Лекция 3.

λ-исчисление как язык программирования

Введение в Функциональное программирование

Джон Харрисон

Университет Кембриджа

10 сентября 2008 г.

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Темы

Вычислимость и полнота по Тьюрингу

λ-исчисление как язык программирования
Представление основных типов данных
Рекурсивные функции и комбинаторы неподвижной точки
Let-выражения
Шаги к декларативному языку программирования

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Вычислимость; Полнота по Тьюрингу

До того как появились компьютеры, проблема разрешимости

(Entscheidungsproblem) стимулировала создание множества
равноценных определений «вычислимости».
Машины Тьюринга
Регистровые машины
µ-рекурсивные функции
Алгоритмы Маркова
λ-исчисление
Многие из них соответствуют методам программирования, несмотря
даже на то, что они появились раньше компьютеров! Например,
алгоритмы Маркова относятся к SNOBOL, а λ-исчисление к
функциональному программированию.

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Влияние λ-исчисления

LISP вобрал некоторые идеи из λ-исчисления, но не был основан на

нём. В действительности же λ-исчисление начало оказывать влияние
благодаря Ландину.
Ландин показал как можно использовать λ-исчисление, чтобы
объяснить возможности некоторых существующих языков
программирования, например, область видимости переменных в
Algol 60.
Он предложил простой функциональных язык ISWIM («If you See
What I Mean»), основанный на λ-исчислении. Многие современные
функциональные языки, включая ML, произошли от ISWIM.
ML начал жить как метаязык для средства доказательства теорем
Edinburgh LCF. ML добавил в ISWIM новейшую систему типов и
исключения. Минималистичный замысел породил добротный язык.
Начнём с λ-исчисления. За работу!

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Булевы значения (1)

Мы можем определить булевы значения следующим образом:

4
true = λx y . x
4
false = λx y . y

Условные выражения сродни конструкции «?:» языка C:

4
if E then E1 else E2 = E E1 E2
Например:

if true then E1 else E2 = true E1 E2

= (λx y . x) E1 E2
= E1

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Булевы значения (2)

и

if false then E1 else E2 = false E1 E2

= (λx y . y ) E1 E2
= E2

Теперь, когда у нас есть условное выражение, нам будет легко

определить все логические операции:

4
not p = if p then false else true
4
p and q = if p then q else false
4
p or q = if p then true else q

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Пары
Мы можем представить упорядоченные пары следующим образом:
4
(E1 , E2 ) = λf . f E1 E2
Для такого представления соответствующие деструкторы пар будут
выглядеть как:

4
fst p = p true
4
snd p = p false
Они работают как полагается
fst (p, q) = (p, q) true
= (λf . f p q) true
= true p q
= (λx y . x) p q
= p

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Кортежи

Мы получаем кортежи, повторяя операцию создания пары:

(E1 , E2 , . . . , En ) = (E1 , (E2 , . . . En ))

Затем мы можем определить основные «отображения»:

(p)1 = fst p

и для i > 1:

(p)i = fst (sndi−1 p)

Мы получаем (E1 , E2 , . . . , En )i = Ei для i ≤ n.

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Декаррированные функции

Теперь мы определим не-каррированные функции от многих

аргументов. Вот функции для перевода функций в каррированный и
декаррированный вид:

4
CURRYn f = λx1 · · · xn . f (x1 , . . . , xn )
4
UNCURRYn g = λp. g (p)1 · · · (p)n

Можно писать λ(x1 , . . . , xn ). t вместо:

UNCURRYn (λx1 · · · xn . t)
И мы получаем обобщённую β-конверсию:

(λ(x1 , . . . , xn ). t[x1 , . . . , xn ])(t1 , . . . , tn ) = t[t1 , . . . , tn ]

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Натуральные числа

Мы можем кодировать числа множеством способов. Похоже, что

самый простой – это нумералы Чёрча:
4
n = λf x. f n x

Это выражение означает, что:

0 = λf x. x
1 = λf x. f x
2 = λf x. f (f x)
3 = λf x. f (f (f x))
4 = λf x. f (f (f (f x)))

и так далее.

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Инкремент
Следующая операция прибавляет единицу к нумералу Чёрча:
4
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

Также можно проверить является ли нумерал Чёрча нулём с

помощью:
4
ISZERO n = n (λx. false) true

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Сложение
Сложение нумералов Чёрча определяется как
4
m + n = λf x. m f (n f x)

В самом деле:

m+n = λf x. m f (n f x)
= λf x. (λf x. f m x) f (n f x)
= λf x. (λx. f m x) (n f x)
= λf x. f m (n f x)
= λf x. f m ((λf x. f n x) f x)
= λf x. f m ((λx. f n x) x)
= λf x. f m (f n x)
= λf x. f m+n x

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Умножение
Умножение определяется как
4
m ∗ n = λf x. m (n f ) x

В самом деле:

m∗n = λf x. m (n f ) x
= λf x. (λf x. f m x) (n f ) x
= λf x. (λx. (n f )m x) x
= λf x. (n f )m x
= λf x. ((λf x. f n x) f )m x
= λf x. (λx. f n x)m x
= λf x. (f n )m x
= λf x. f mn x

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Декремент

Это уже намного сложнее. Сначала нам надо определить

вспомогательную функцию для работы с парами:
4
PREFN = λf p. ( false,
if fst p then snd p else f (snd p))
Мы получаем:

PREFN f (true, x) = (false, x)

PREFN f (false, x) = (false, f x)

Мы можем использовать эту функцию для того, чтобы

«отбросить» одно из применений f в f n x. Эта выдумка
принадлежит Клини. Теперь определим:
4
PRE n = λf x. snd(n (PREFN f ) (true, x))

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Рекурсивные функции (1)

Кажется, что сложно определить рекурсивную функцию не задав ей

имени. Однако, мы можем это сделать, используя комбинаторы
неподвижной точки.
Говорят, что Y – комбинатор неподвижной точки, если, применив
его к функции f , мы получим неподвижную точку x для f , то есть
такое x, что f (x) = x. Для всех f имеем:

f (Y f ) = Y f

Мы сможем понять как составить такой комбинатор, вспомнив

парадокс Рассела. Мы определяли R = λx. ¬(x x) и приходили к
тому, что R R = ¬(R R). Всё, что нам потребуется, это заменить ¬
на функцию f . Таким образом:
4
Y = λf . (λx. f (x x))(λx. f (x x))

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Рекурсивные функции (2)

Достаточно просто показать, что Y работает как положено:

Yf = (λ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 )

Как альтернативу Y , можно задать выражение:

4
T = (λx y . y (x x y )) (λx y . y (x x y ))

Оно имеет более сильное свойство: T f −→ f (T f ).

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Рекурсивные функции (3)

Как нам использовать комбинатор неподвижной точки для
определения рекурсивных функций? Рассмотрим функцию
факториала. Хотелось бы определить 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)

Таким образом, если мы определим:

4
F = λf n. if ISZERO n then 1 else n ∗ f (PRE n)

то мы обнаружим, что fact есть неподвижная точка функции F , т.е.

fact = F fact. Поэтому мы определим:

fact = Y F

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Let-выражения
Зачастую, удобно привязать выражение к некоторому имени, чтобы
избежать множества повторов одного и того же выражения. Введём
следующий вариант синтаксического сахара XXX:
4
let x = s in t = (λx. t) s

Введём также запись для множества совместных привязок:

let x1 = s1 and · · · and xn = sn in t

которая является синтаксическим сахаром для:

(λ(x1 , . . . , xn ). t) (s1 , . . . , sn )

Ещё мы можем использовать запись let f x1 · · · xn = t, которая

является синтаксическим сахаром для:

let f = λx1 · · · xn . t

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Рекурсивные let-выражения

Обычно let интерпретируется не рекурсивно. Когда мы хотим задать

выражение рекурсивно, то добавляем слово rec. Например:

let rec fact(n) = if ISZERO n then 1

else n ∗ fact(PRE n)

равнозначно

let fact = Y F

где, как и раньше:

F = λf n. if ISZERO n then 1 else n ∗ f (PRE n)

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Функциональные программы

Мы уже говорили, что функциональная программа это просто

выражение.
Однако, мы обычно выделяем некоторые общие и интересные
выражения в let конструкции; таким образом, программа
приобретает форму: серия определений подвыражений и основное
выражение, например

let rec fact(n) = if ISZERO n then 1

else n ∗ fact(PRE n) in
···
fact(6)

Таким образом, программа может быть прочитана «декларативно»,

как множество математических уравнений, определяющих свойства
значимых понятий. Вся информация о вычислении задана неявно.

Джон Харрисон Введение в Функциональное программирование

 Лекция 3. λ-исчисление как язык программирования

Способ вычисления

Тем не менее, способ вычисления всё же существует.

Грубо говоря, все уравнения читаются слева направо, и все имена
заменяются на соответствующие выражения. Затем, мы постоянно
выполняем β-конверсии.
Основной вопрос состоит в том, как выполнить серию β-конверсий.
Мы знаем, что от этого зависит завершится вычисление или нет.
Как мы увидим, различные функциональные языки выбирают
разные подходы.
Однако сейчас время подумать о типах.

Джон Харрисон Введение в Функциональное программирование