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

В терминах нашего конкретного синтаксиса мы всегда редуцируемредекс, чей символ λ находится левее всего.Следующая теорема, известная как теорема Черча–Россера, утверждает, что если мы начнем с терма T и проведем две произвольныеконечные последовательности редукций, всегда будут существовать ещедве последовательности редукций, которые приведут нас к одному и тому же терму (хотя он может и не находиться в нормальной форме).Теорема 2.

Если t → s1 и t → s2 , то существует терм u, такой, чтоs1 → u и s2 → u.Эта теорема имеет несколько важных следствий.Следствие 1. Если t1 = t2 , то существует терм u такой, что t1 → uи t2 → u.Следствие 2. Если t = t1 и t = t2 , где t1 и t2 находятся в нормальнойформе, то t1 ≡α t2 , т.е. t1 и t2 равны с точностью до переименованияпеременных.Следовательно, нормальная форма, если она существует, единственнас точностью до до α-конверсии.С вычислительной точки зрения это означает следующее.

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

Такой терм является замкнутым; он имеетфиксированный смысл независимо от значения любых переменных.В теории комбинаторов установлено, что с помощью несколько базовых комбинаторов и переменных можно выразить любой терм без применения операции лямбда-абстракции. В частности, замкнутый терм можновыразить только через эти базовые комбинаторы. Определим эти комбинаторы следующим образом:I = λx.xK = λx y.xS = λf g x.f x (g x)I является функцией идентичности, которая оставляет свой аргументнеизменным. K служит для создания постоянных (константных) функций: применив его к аргументу a, получим функцию λx.a, которая возвращает a независимо от переданного ей аргумента.

Комбинатор S является «разделяющим»: он берет две функции и аргумент и «разделяет»аргумент между функциями.Теорема 3. Для любого лямбда-терма t существует терм t0 , не содержащий лямбда-абстракций и составленный из комбинаторов S,K, I и переменных, такой что F V (t0 ) = F V (t) и t0 = t.Эту теорему можно усилить, поскольку комбинатор I может бытьвыражен в терминах S и K. Действительно, для любого A выполняется:S K A x = K x (A x)= (λy.x) (A x)= xПрименяя η-конверсию, получаем, что I = S K A для любого A. Попричинам, которые станут ясны в дальнейшем, мы будем использоватьA = K.

Таким образом, I = S K K, и в дальнейшем символ I можноисключать из выражений, составленных из комбинаторов.Хотя мы представили комбинаторы как некоторые лямбда-термы, можно разработать теорию, в которой они являются базовым понятием. Также, как и в лямбда-исчислении, можно начать с формального синтаксиса,14вместо лямбда-абстракций содержащего комбинаторы. Вместо правил α,β и η-конверсии, можно ввести правила конверсии для выражений, содержащих комбинаторы, например K x y → x.

Как независимая теория,теория комбинаторов обладает многими аналогиями с лямбда-исчислением, в частности, для нее выполняется теорема Черча–Россера. Однакоэта теория менее интуитивно понятно, поскольку выражения с комбинаторами могут быстро становиться сложными и запутанными.Комбинаторы имеют не только теоретический интерес. Как мы ужеговорили, и как станет ясно из последующих глав, лямбда-исчислениеможет рассматриваться как простой функциональный язык программирования, составляющий ядро настоящих языков, таких как ML илиHaskell.

Тогда можно сказать, что приведенная выше теорема показывает, что лямбда-исчисление может быть в некотором смысле «скомпилировано» в «машинный код» комбинаторов. Комбинаторы действительноиспользуются как метод реализации функциональных языков не толькона уровне программного, но и на уровне аппаратного обеспечения.5Лямбда-исчисление как язык программирования5.1Введение5.2Представление данных в лямбда-исчисленииПрограммы предназначены для обработки данных, поэтому необходимо начать с того, чтобы зафиксировать лямбда-выражения, представляющие данные. Затем мы определим базовые операции на этих данных.Часто будет возможно показать, как строка s, представляющая некоторое описание в читаемом человеком формате может быть закодирована ввиде лямбда-выражения s0 . Эта процедура известна как «синтаксическийсахар».

Будем записывать такую процедуру какs , s0Эту запись следует читать как «s = s0 по определению». Можно трактовать ее как определение некоторой константы s, обозначающей операцию, которую затем можно использовать в стиле, принятом в лямбдаисчислении.155.2.1Булевские значения и условияДля кодирования значений true и false можно использовать любыенеравные лямбда-термы, но лучше всего определить их следующим образом:true , λx y.xfalse , λx y.yИспользуя эти определения, можно легко определить условное выражение (напоминающее конструкцию ?:) языка Си.

Заметьте, что это —условное выражение, а не условная команда (в нашем контексте этопонятие не имеет смысла), следовательно, else-часть обязательна:if E then E1 else E2 , E E1 E2 .Действительно:if true then E1 else E2 , true E1 E2, (λx y.x) E1 E2, E1иif false then E1 else E2 , true E1 E2, (λx y.y) E1 E2, E2Теперь легко определить все обычные логические операторы:not p , if p then false else truep and q , if p then q else falsep or q , if p then true else q5.2.2Пары и кортежиУпорядоченную пару можно представить следующим образом:(E1 , E2 ) , λf.f E1 E2Скобки здесь необязательны, но мы будем использовать их для того,чтобы вызывать аналогии с соответствующей записью для обозначения16векторов или комплексных чисел в математике. В действительности запятую можно рассматривать просто как некоторый инфиксный оператор,как + или −.

С учетом данного определения, функции для извлечениякомпонентов пары можно записать так:fst p , p truesnd p , p falseНетрудно убедиться, что эти определения удовлетворяют требованиям:fst(p, q) =====(p, q) true =(λf.f p q) true =true p q =(λx y.x) p q =psnd(p, q) =====(p, q) false =(λf.f p q) false =false p q =(λx y.y) p q =qиТройки, четверки и вообще, произвольные n-кортежи можно построить с помощью пар:(E1 , E2 , . . . , En ) = (E1 , (E2 , . . . , En )).Следует только ввести соглашения, что оператор «запятая» ассоциативенвправо.Функции fst и snd можно расширить на случай n-кортежей. Определим функцию селектора, которая получает i-й компонент кортежа p.Будем записывать ее как (p)i .

Тогда (p)1 = fst p и (p)i = fst(sndi−1 p).5.2.3Натуральные числаНатуральное число n будем представлять в следующем виде:n , λf x.f n x17т.е. 0 = λf x.x, 1 = λf x.f x, 2 = λf x.f (f x) и т.д. Таким образом, числа вводятся индуктивным образом, и употребление символа nв определении сделано просто для удобства. Введенное представлениеназывается «цифрами по Черчу». Это не очень эффективное представление; можно было бы использовать, например, двоичное представлениечисел в виде кортежей, состоящих из значений true и false.

Однако сейчас нас интересует понятие вычислимости «в принципе», и цифры поЧерчу обладают рядом удобных формальных свойств.Например, легко можно ввести операцию следования (увеличенияна 1):SUC , λn f x.n f (f x)Действительно:SUC n ======(λn f x.n f (f x)) (λf x.f n x) =λf x.(λf x.f n x) f (f x) =λf x.(λx.f n x) (f x) =λf x.f n (f x) =λf x.f n+1 x =n+1Также легко ввести функцию проверки числа на 0:ISZERO n , n (λx.false) trueпосколькуISZERO 0 = (λf x.x) (λx.false)true = trueиISZERO n + 1 ====(λf x.f n x)(λx.false)true =(λx.false)n+1 true =(λx.false)((λx.false)n true) =falseСледующие определения вводят сложение и умножение:m + n , λf x.m f (n f x)m ∗ n , λf x.m (n f ) x18Действительно:m+n ========λfλfλfλfλfλfλfλfx.m f (n f x) =x.(λf x.f m x) f (n f x) =x.(λx.f m x) (n f x) =x.f m (n f x) =x.f m ((λf x.f n x) f x) =x.f m ((λx.f n x) x) =x.f m (f n x) =x.f m+n xиm∗n ========λfλfλfλfλfλfλfλfx.m (n f ) x =x.(λf x.f m x) (n f ) x =x.(λx.(n f )m x) x =x.(n f )m x =x.((λf x.f n x) f )m x =x.(λx.f n x)m x =x.(f n )m x =x.f mn xЭти операции на натуральных числах довольно легко представляются в лямбда-исчислении, однако выразить функцию «предшествования»(вычитание 1) оказывается гораздо труднее.

Требуется найти лямбдавыражение PRE, такое, что PRE 0 = 0 и PRE n + 1 = n. Эту задачурешил Клини в 1935 году. Идея заключается в том, чтобы отбросить одно применение f в выражении λf x.f n x. Определим функцию PREFN,удовлетворяющую следующим условиям:PREFN f (true, x) = (false, x)иPREFN f (false, x) = (false, f x)Тогда можно заметить, что (PREFN f )n+1 (true, x) = (false, f n x) ифункцию предшествования можно определить без особых трудностей.Функцию PREFN можно определить, например, так:PREFN , λf p.(false, if fst p then snd p else f (snd p))Тогда:PRE n , λf x.

snd(n (PREFN f ) (true, x))195.3Рекурсивные функцииВозможность определять рекурсивные функции — характерная особенность функционального программирования. На первый взгляд, кажется, что в лямбда-исчислении нет способа сделать это. Действительно,важной частью рекурсивного определения является именование функции, иначе как мы обратимся к ней в правой части определения? Однаков действительности мы сможем обойтись без этого, хотя, как и в случаес функцией предшествования, этот факт далеко не очевиден.Ключевым моментом является существование так называемых комбинаторов неподвижной точки.

Замкнутый лямбда-терм Y называется комбинатором неподвижной точки, если для любого лямбда-терма fвыполняется: f (Y f ) = Y f . Таким образом, комбинатор неподвижнойточки по заданному терму f возвращает неподвижную точку f , т.е. термx, такой что f (x) = x. Первый такой комбинатор, найденный Карри,обычно обозначается как Y .