Функциональное программирование. Основы (Файлы для подготовки к экзамену), страница 4

Часто его называют «парадоксальным комбинатором». Он определяется следующим образом:Y , λf.(λx.f (x x)) (λx.f (x x))Нетрудно убедиться, что данное выражение действительно определяеткомбинатор неподвижной точки:Y f ====(λf.(λx.f (x x)) (λx.f (x x))) f =(λx.f (x x)) (λx.f (x x)) =f ((λx.f (x x)) (λx.f (x x))) =f (Y f )Хотя с математической точки зрения наши рассуждения верны, с вычислительной стороны такое определение вызывает трудности, посколькувышеприведенное рассуждение использует лямбда-равенство, а не редукции (в последнем переходе мы использовали обратную β-конверсию).По этой причине можно предпочесть следующее определение комбинатора неподвижной точки, принадлежащее Тьюрингу:T , (λx y.y (x x y)) (λx y.y (x x y))(Доказательство того, что T f → f (T f ) оставляем в качестве упражнения.)Несмотря на сделанное выше замечание, будем обозначать комбинатор неподвижной точки по-прежнему как Y .

Покажем, как он можетпомочь в определении рекурсивных функций. Рассмотрим в качестве20примера функцию факториала. Мы хотим определить функцию fact, такую, что:fact(n) = if ISZERO n then 1 else n ∗ fact(PRE n)Сперва преобразуем это к следующему эквивалентному виду:fact = λn.if ISZERO n then 1 else n ∗ fact(PRE n)Это выражение, в свою очередь, эквивалентноfact = (λf n.if ISZERO n then 1 else n ∗ f (PRE n)) factОтсюда можно заключить, что fact является неподвижной точкой некоторой функции F следующего вида:F = λf n.if ISZERO n then 1 else n ∗ f (PRE n)Таким образом, fact = Y F .Похожая техника используется для определения взаимно рекурсивных функций, т.е. набора функций, определения которых взаимно зависят друг от друга.

Определение видаf1f2...fn====F1 f1 . . . fnF2 f1 . . . fn...Fn f1 . . . fnможно преобразовать, используя кортежи, к одному равенству:(f1 , f2 , . . . , fn ) = (F1 f1 . . . fn , F2 f1 . . . fn , . . . , Fn f1 . . . fn )Теперь, если мы запишем t = (f1 , f2 , . . . , fn ), то каждая из функций fiв правой части равенства может быть представлена через соответствующий селектор: fi = (t)i .

Таким образом, уравнение можно записать вканоническом виде t = F t, что дает решение t = Y F . Отсюда, снова спомощью селекторов, можно получить отдельные компоненты кортежа t.5.4Именованные выраженияРанее мы представляли возможность записывать безымянные функции как одно из преимуществ лямбда-исчисления. Было показано, чторекурсивные функции можно определить, не вводя каких-либо имен. Тем21не менее возможность давать имена выражениям часто бывает полезна, поскольку позволяет избежать долгих и утомительных повторений.Простая форма именования может быть введена как еще одна форма«синтаксического сахара» над чистым лямбда-исчисление:let x = S in T , (λx.T ) SНапример:(let z = 2 + 3 in z + z) = (λz.z + z) (2 + 3) = (2 + 3) + (2 + 3)Можно связать несколько выражений с переменными в последовательном или параллельном стиле.

В первом случае мы просто вкладываем let-конструкции друг в друга. Во втором мы записываем связывания,ограничив их символами ‘{’ и ‘}’ и разделяя символом ‘;’:let {x1 = S1 ; x2 = S2 ; . . . ; xn = Sn } in TЭто выражение можно рассматривать как «синтаксический сахар» для:(λ(x1 , . .

. , xn ).T ) (S1 , . . . , Sn )Вместо префиксной формы с let можно ввести постфиксный вариант,который иногда более читаем:T where x = SНапример, можно записать ‘y < y 2 where y = 1 + x’.Далее, с помощью let-нотации можно определять функции, введя соглашение, чтоlet f x1 x2 . . . xn = S in Tозначаетlet f = λx1 x2 . . . xn .S in TДля определения рекурсивных функций можно ввести соглашение поиспользованию комбинатора неподвижной точки, т.е.let fact n = if ISZERO n then 1 else n ∗ fact(PRE n) in Sозначает let fact = Y F in S.225.5На пути к реальному языку программированияРазработанная нами система «синтаксического сахара» позволяет поддерживать понимаемый человеком синтаксис для чистого лямбда-исчисления, и с ее помощью можно писать программы на языке, очень напоминающем настоящий язык программирования, такой как Haskell илиML.Программа представляет собой единственное выражение.

Однако, имеяв распоряжении механизм let для связывания подвыражений с именами, более естественно рассматривать программу как набор определенийвспомогательных функций, за которыми следует само выражение, например:let { fact n = if ISZERO n then 1 else n ∗ fact(PRE n);...} in fact 6(Заметьте, что это уже напоминает реальную программу на языке Haskell,за тем исключением, что, помимо правил выравнивания, позволяющимобойтись без символов ‘{’, ‘}’ и ‘;’,в Haskell введено соглашение опускатьконструкцию let в определениях верхнего уровня.)Эти определения вспомогательных функций можно интерпретироватькак систему уравнений в обычном математическом смысле. Они не задают нам нам явных указаний, каким именно образом вычислять выражения.

По этой причине функциональное программирование часто объединяют с логическим в класс декларативных методов программирования.Программа определяет ряд желаемых свойств результата и оставляетмашине найти способ его вычисления.Тем не менее программа все же должна быть выполнена каким-либообразом. В действительности выражение-программа вычисляется с помощью «развертывания» всех конструкций до уровня чистого лямбдаисчисления и последующего применения β-конверсий. Таким образом,хотя в самой программе нет никакой информации по ее выполнению,при ее составлении все же подразумевается некоторая стратегия исполнения.

В некотором смысле понятие декларативности является отражением только человеческой психологии.Более того, необходимо ввести некоторое определенное соглашениепо используемым редукционным стратегиям, поскольку известно, чтовыбор различных β-редексов может привести к различному поведениюпрограммы в смысле ее завершаемости. Следовательно, нам нужно определить эту стратегию, чтобы получить реальный язык программирования.

В последующих разделах мы увидим, как различаются по этому23критерию различные функциональные языки программирования. Однако сперва нам нужно ввести понятие типа.6ТипыТипы предоставляют возможность различать отдельные виды данных,такие как булевские значения, натуральные числа и функции. Учет типовможет дать то преимущество, что, например, функция не может бытьприменена к аргументам, имеющим «неправильный» тип. Почему у насможет возникнуть желание ввести типы в лямбда-исчисление и в языкипрограммирования, основанные на нем? Мотивы этого могут возникнутькак со стороны логики, так и со стороны программирования.Изначально лямбда-исчисление задумывалось как способ формализации всего языка математики. Черч надеялся также включить в лямбдаисчисление теорию множеств.

По заданному множеству S можно определить его характеристическую функцию χS , такую что:(true, x ∈ SχS (x) =false, x ∈/SИ наоборот, имея унарный предикат P , можно определить множествотаких x, что P (x) = true. Кажется, естественно определить предикаты(и, следовательно, множества) в виде произвольных лямбда-выражений.Однако это приводит к противоречиям.Рассмотрим знаменитый парадокс Рассела. Определим множество Rкак множество тех множеств, которые не содержат сами себя в качествеэлемента:R = {x|x ∈/ x}Тогда мы получаем, что R ∈ R ⇔ R ∈/ R, что является, несомненно, противоречием.

В терминах лямбда-исчисления, мы полагаем R = λx.¬(x x)и обнаруживаем, что R R = ¬(R R). Выражение R R является неподвижной точкой оператора отрицания.Парадокс Рассела возникает из-за того, что мы делаем странную даже с точки зрения здравого смысла вещь: мы применяем функцию саму к себе. Конечно, само по себе применение функции к самой себене обязательно приводит к парадоксу: например, функция идентичности λx.x или константная функция λx.y вполне безобидны.

Однако, мы,безусловно, имели бы более ясное представление о функциях, обозначаемых лямбда-термом, если бы мы точно знали области их определенияи значений и применяли бы их только к аргументам, принадлежащим24их областям определения. Таковы были причины, по которым Расселизначально предложил ввести понятие типа.Типы также возникли, вероятно, вначале без всякой связи с приведенными выше рассуждениями, в языках программирования, и посколькумы рассматриваем лямбда-исчисление как язык программирования, такая точка зрения не может нас не интересовать.

Даже в первых версияхФортрана различались целые и вещественные числа. Одной из этого была эффективность: зная о типе переменной, можно генерировать болееэффективный код и более эффективно использовать память.Помимо эффективности, по мере развития программирования, типыстали цениться за то, что они предоставляют ограниченную форму статической проверки программ. Многие ошибки программирования, от простых опечаток до более существенных концептуальных ошибок, влекутза собой несоответствие типов, и, следовательно, могут быть обнаружены до запуска программы, на этапе ее компиляции.

Более того, типычасто предоставляют полезную информацию для людей, читающих программы. Наконец, типы можно использовать для того, чтобы достичьбольшей модульности и скрытия данных: они позволяют «искусственно»отделить некоторые данные от их внутреннего представления.Вместе с тем некоторые программисты недолюбливают типы. Существуют безтиповые языки, как императивные, так и функциональные.Другие языки (к ним относится и Си) являются слабо типизированными: компилятор допускает некоторое несоответствие в типах и самделает необходимые преобразования.

Также существуют языки (например, LISP), которые выполняют проверку типов динамически, во времявыполнения программы, а не во время компиляции.Найти систему типов, которая не позволяет выполнять полезные статические проверки и в то же время не накладывает на программистачересчур жестких ограничений — непростая задача, до конца еще нерешенная.