John Harrison - Введение в функциональное программирование (1108517), страница 9
Текст из файла (страница 9)
е. выполнять роль интерпретатора. Подробнее это будет рассмотрено в курсе Computation Theory.26Глава 3. Лямбда-исчисление как язык3.1. программированияПредставление данных в лямбда-исчислениисобственно, и происходит его название ML, Meta Language) системы доказательстватеорем Edinburgh LCF (Gordon, Milner, and Wadsworth 1979). Это значит,что язык был предназначен для реализации алгоритмов логического выводав формальном дедуктивном исчислении. Определение языка обнаруживаетсущественное влияние ISWIM, но в отличие от последнего, ML был расширентакими возможностями, как новаторская полиморфная типизация, включающаяабстрактные типы данных, либо система обработки ошибок на основе исключений.Эти черты языка были введены, исходя из реальных практических потребностей,что в итоге привело к целостному и точному дизайну.
Подобная узкаяспециализация характерна для успешных языков (язык C может служить ещё однимхорошим примером) и резко их отличает от провальных попыток коллективногопроектирования, таких как Algol 60, который оказался скорее источником важныхидей, нежели практичным инструментом. Дальнейшее знакомство с ML состоитсяпозже, а в данный момент мы рассмотрим, как в роли языка программированияможет быть использовано чистое лямбда-исчисление.3.1Представление данных в λ-исчисленииПрограммы для своей работы требуют входных данных, поэтому мы начнём сфиксации определенного способа представления данных в виде выражений лямбдаисчисления.
Далее введём некоторые базовые операции над этим представлением.Во многих случаях оказывается, что выражение s, представленное в форме, удобнойдля восприятия человеком, может напрямую отображаться в лямбда-выражение s0 .Этот процесс получил жаргонное название «синтаксическая глазировка» («syntactic sugaring»), поскольку делает горькую пилюлю чистой лямбда-нотации болееудобоваримой. Введём следующее обозначение:4s = s0 .Будем говорить, что «s = s0 по определению»; другая общепринятая формазаписи этого отношения — s =def s0 . При желании, мы можем всегда считать,что вводим некоторое константное выражение, определяющее семантику операции,которая затем применяется к своим аргументам в обычном стиле лямбда-исчисления,абстрагируясь тем самым от конкретных обозначений.
Например, выражениеif E then E1 else E2 возможно трактовать как COND E E1 E2 , где COND — некотораяконстанта. В подобном случае все переменные в левой части определения должныбыть связаны операцией абстракции, т. е. вместо4fst p = p true(см. ниже) мы можем написать4fst = λp. p true.3.1.1Логические значения и условияДля представления логических значений true («истина») и false («ложь»)годятся любые два различных лямбда-выражения, но наиболее удобно использовать273.1.
Представление данныхГлавав лямбда-исчислении3. Лямбда-исчисление как язык программированияследующие:4true = λx y. x4false = λx y. yИспользуя эти определения, легко ввести понятие условного выражения,соответствующего конструкции ? : языка C. Отметим, что это условное выражение,а не оператор (который не имеет смысла в данном контексте), поэтому наличиеальтернативы обязательно.4if 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 = false E1 E2= (λx y.
y) E1 E2= E2Определив условное выражение, на его базе легко построить весь традиционныйнабор логических операций:4not p = if p then false else true4p and q = if p then q else false4p or q = if p then true else q3.1.2Пары и кортежиОпределим представление упорядоченных пар следующим образом:4(E1 , E2 ) = λf. f E1 E2Использование скобок не обязательно, хотя мы часто будем использовать ихдля удобства восприятия либо подчеркивания ассоциативности. На самом деле, мыможем трактовать запятую как инфиксную операцию наподобие +. Определив пару,как указано выше, зададим соответствующие операции извлечения компонент парыкак:4fst p = p true4snd p = p false28Глава 3.
Лямбда-исчисление как язык3.1. программированияПредставление данных в лямбда-исчисленииЛегко убедиться, что эти определения работают, как требуется:fst (p, q) =====(p, q) true(λf. f p q) truetrue p q(λx y. x) p qpsnd (p, q) =====(p, q) false(λf. f p q) falsefalse p q(λx y. y) p qqиПостроение троек, четвёрок, пятёрок и так далее вплоть до кортежейпроизвольной длины n производится композицией пар:(E1 , E2 , . . .
, En ) = (E1 , (E2 , . . . En ))Всё, что нам при этом потребуется — определение, что инфиксный операторзапятая правоассоциативен. Дальнейшее понятно без введения дополнительныхсоглашений. Например:(p, q, r, s) =====(p, (q, (r, s)))λf. f p (q, (r, s))λf. f p (λf.
f q (r, s))λf. f p (λf. f q (λf. f r s))λf. f p (λg. g q (λh. h r s))В последнем выражении для удобства восприятия было произведено альфапреобразование. Несмотря на то, что кортежи представляют собой «плоскую»структуру данных, путём последовательной их композиции возможно представитьпроизвольную конечную древовидную структуру. Наконец, если кто-то предпочитаеттрадиционные функции, заданные на декартовом произведении, нашимкаррированным функциям, преобразовать их друг в друга нетрудно:4CURRY f = λx y. f (x, y)4UNCURRY g = λp. g (fst p) (snd p)Эти специальные операции над парами нетрудно обобщить на случай кортежейпроизвольной длины n.
Например, мы можем задать функцию-селектор выборки i-гокомпонента из кортежа p. Обозначим эту операцию (p)i , и определим её как (p)1 =fst p, (p)i = fst (sndi−1 p). Аналогичным образом возможно обобщение CURRYи UNCURRY:4CURRYn f = λx1 · · · xn . f (x1 , . . . , xn )4UNCURRYn g = λp. g (p)1 · · · (p)n293.1. Представление данныхГлавав лямбда-исчислении3.
Лямбда-исчисление как язык программированияВоспользуемся обозначением λ(x1 , . . . , xn ). t как сокращённой формой записи дляUNCURRYn (λx1 · · · xn . t),обеспечив тем самым естественную нотацию для функций над декартовымипроизведениями.3.1.3Натуральные числаПредставим натуральное число n в виде34n = λf x.
f n x,то есть, 0 = λf x. x, 1 = λf x. f x, 2 = λf x. f (f x) и т. д. Такое представлениеполучило название нумералов Чёрча, хотя его базовая идея была опубликована ранеев работе Wittgenstein (1922).4 Это представление не слишком эффективно, так какфактически представляет собой запись чисел в системе счисления по основанию 1: 1,11, 111, 1111, 11111, 111111, .
. .. С точки зрения эффективности можно разработатьгораздо лучшие формы представления, к примеру, кортеж логических значений,который интерпретируется как двоичная запись числа. Впрочем, в данный моментнас интересует лишь принципиальная вычислимость, а нумералы Чёрча имеютразличные удобные формальные свойства. Например, легко привести лямбдавыражения такой общеизвестной арифметической операции, как получение числа,следующего в натуральном ряду за данным, то есть, прибавление единицы каргументу операции:4SUC = λ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 xn+1Аналогично, легко реализуется проверка числа на равенство нулю:4ISZERO n = n (λx. false) trueпосколькуISZERO 0 = (λf x. x)(λx. false) true = trueиISZERO (n + 1) ====(λf x. f n+1 x)(λx. false)true(λx. false)n+1 true(λx. false)((λx. false)n true)false3Запись выражения f n x с параметром n применяется исключительно для удобства записи, а нев силу его цикличности.4См. «6.021 A number is the exponent of an operation».30Глава 3. Лямбда-исчисление как язык3.1. программированияПредставление данных в лямбда-исчисленииСумма и произведение двух нумералов Чёрча:4m + n = λf x. m f (n f x)4m ∗ n = λf x.
m (n f ) xВ справедливости этих определений легко убедиться: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 ) xx. (λf x. f m x) (n f ) xx. (λx. (n f )m x) xx. (n f )m xx. ((λf x. f n x) f )m xx. ((λx. f n x)m xx. (f n )m xx.
f mn xНесмотря на то, что эти операции на натуральных числах были определеныдостаточно легко, вычисление числа, предшествующего данному, гораздо сложнее.Нам требуется выражение P RE такое, что P RE 0 = 0 и P RE (n + 1) = n. Решениеэтой задачи было предложено Клини в работе Kleene (1935). Клини применил такойприём: для заданного λf x.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
