Бестиповое λ-исчисление

λ-исчисление разработано в 1930-х годах Алонзо Чёрчем, и изначально использовалось для исследования оснований математики. В 1936 году Чёрч выделил подмножество λ-исчисления, называемое сейчас бестиповым λ-исчислением, относящееся к проблеме вычислимости. В 1940 году он ввёл простое типизированное λ-исчисление, более слабое, чем бестиповое, но зато логически непротиворечивое.

В середине 1960-х годов, Питер Ландин показал, что любой произвольно сложный язык программирования можно свести к простому базовому исчислению, которое затем можно дополнить набором производных форм, выраженных через базовое исчисление. В качестве базового исчисления он использовал λ-исчисление.

Джон МакКарти использовал лямбда-исчисление для формального описания и исследования языка Lisp. Впоследствии, λ-исчисление стало широко использоваться для спецификации конструкций языков программирования, в разработке языков, и при исследовании систем типов.

Важность λ-исчисления в том, что это, с одной стороны, своего рода язык программирования, на котором можно описывать поведение программ, а с другой стороны – математический объект, о котором можно доказывать строгие утверждения.

Основы λ-исчисления

В математике и программировании, базовой абстракцией является функция (или процедура). Действительно, вместо того, чтобы повторять одно и то же выражение много раз, удобно параметризовать его, и далее использовать сокращённое название.

Введём два термина.

Функциональная абстракция
это определение параметризованного выражения. Например, выражение \(f(x) = x^2-x+1\) является функциональной абстракцией арифметического выражения.
Применение функции
это использование функциональной абстракции в рамках другого выражения, с указанием значений параметров. Например, выражение \(f(2)\) – это применение функции \(f\) к числу \(2\).

Лямбда-исчисление является наиболее простым исчислением, реализующим эту концепцию. В лямбда-исчислении существуют только две операции – функциональная абстракция и применение, а все значения сами являются либо функциональными абстракциями, либо переменными.

Определим синтаксис для записи выражений лямбда-исчисления. Любой терм t лямбда-исчисления является одним из:

  1. Переменная. Переменные будем обозначать маленькими латинскими буквами, напр. x.
  2. Лямбда-абстракция. Анонимная (т.е. не имеющая имени) функциональная абстракция. Обозначается символом λ, после которого следует переменная-параметр, затем точка, затем “тело”, являющееся произвольным термом, напр. λx. x
  3. Применение. Два терма, разделённых пробелом, означают применение левого терма к правому терму. Напр. (λx. x) y. Правый терм будем называть аргументом.

В случае неоднозначности, будем использовать скобки для разделения термов.

Переменные в теле лямбда-абстракции, являющиеся параметрами, называются связанными переменными. Прочие – свободными.

Терм без свободных переменных называется замкнутым; замкнутые термы называют также комбинаторами.

α-эквивалентность

Название связанных переменных лямбда-абстракции не несёт смысловой нагрузки, оно может быть произвольным. Как следствие, два лямбда-терма, одинаковые с точностью до переименования связанных переменных, называются α-эквивалентными. Например, следующие лямбда-абстракции эквивалентны:

  • λx. x
  • λy. y
  • λz. z

Но следующие нет:

  • λx. y
  • λy. x

β-редукция

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

Формально это можно записать следующим образом:

(λx. t₁) t₂ -> [x -> t₂] t₁

Здесь t₁, t₂ – произвольные лямбда-термы, а выражение в квадратных скобках означает замену в следующем терме.

Терм, к которому применима β-редукция, будем называть редексом (redex, reducible expression).

Например, терм вида

(λx. x) (λy. y)

может быть редуцирован к

  [x -> (λy. y)]x
= (λy. y)

Стратегии вычисления

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

Будем называть термы, к которым нельзя в соответствии со стратегией применить β-редукцию термами в нормальной форме.

Рассмотрим типовые стратегии на примере терма

(λx. x) ((λy. y) (λz. (λw. w) z))

или для простоты

id (id (λz. id z))

где id обозначает комбинатор идентичности, id = λx. x.

Полная β-редукция

При полной β-редукции, любой редекс может сработать в любой момент.

   (λx. x) ((λy. y) (λz. (λw. w) z))
-> (λx. x) ((λy. y) (λz. [w -> z]w))
 = (λx. x) ((λy. y) (λz. z))
-> [x -> ((λy. y) (λz. z))]x
 = (λy. y) (λz. z)
-> [y -> (λz. z)]y
 = λz. z

Нормальный порядок вычислений

При нормальном порядке вычислений, сначала обрабатывается самый левый, самый внешний редекс.

  (λx. x) ((λy. y) (λz. (λw. w) z))
-> [x -> ((λy. y) (λz. (λw. w) z))]x
 = (λy. y) (λz. (λw. w) z)
-> [y -> (λz. (λw. w) z)] y
 = λz. (λw. w) z
-> λz. [w -> z]w
 = λz. z

Вызов по имени

Стратегия вызова по имени использует нормальный порядок вычислений, и дополнительно запрещает проводить редукцию внутри абстракций. Соответствует модели “ленивых” вычислений.

  (λx. x) ((λy. y) (λz. (λw. w) z))
-> [x -> ((λy. y) (λz. (λw. w) z))]x
 = (λy. y) (λz. (λw. w) z)
-> [y -> (λz. (λw. w) z)]y
 = λz. (λw. w) z

Вызов по имени используется, в частности, в ALGOL и Haskell. Строго говоря, в Haskell используется оптимизированная версия, известная как “вызов по необходимости”, когда аргумент вычисляется единожды при необходимости (как правило, после применения!), а прочие его вхождения используют уже вычисленное значение.

Вызов по значению

Используется в большинстве языков программирования. Соответствует модели “нетерпеливых” (строгих) вычислений.

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

  (λx. x) ((λy. y) (λz. (λw. w) z))
-> (λx. x) ([y -> (λz. (λw. w) z)]y)
 = (λx. x) (λz. (λw. w) z)
-> [x -> (λz. (λw. w) z)]x
 = (λz. (λw. w) z)

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

Рассмотрим некоторые типовые конструкции λ-исчисления, чтобы почувствовать, насколько это мощная система.

Функции нескольких аргументов

Можно заметить, что в наше определение λ-исчисления не “встроено” способа определить λ-абстракцию с несколькими переменными. Это не недосмотр – абстракции нескольких переменных легко выражаются через вложенные абстракции одной переменной. Такое представление называется каррированием (в честь Хаскелла Карри).

Действительно, рассмотрим вложенную абстракцию вида

λx. λy. λz. (x y) (x z)

При последовательном применении,

(((λx. λy. λz. (x y) (x z)) u) v) w

получим

(u v) (u w)

что семантически эквивалентно применению функции 3 аргументов к 3 аргументам.

Для удобства, введём сокращённое обозначение:

λx y …. t ≡ λx. λy. … t

Так же, для удобства, условимся, что оператор применения лево-ассоциативен, т.е.

t₁ t₂ … tₙ ≡ ((t₁ t₂) …) tₙ

Булевские константы Чёрча

Ещё одна конструкция, легко кодируемая в λ-исчислении – булевские выражения и условный оператор.

Определим следующие выражения:

tru = λx y. x
fls = λx y. y

Пусть tru кодирует значение “истина”, а fls значение “ложь”. Тогда мы можем определить комбинатор

ifThenElse = λc t f. c t f

являющейся функцией 3 аргументов, и переходящей во второй аргумент, если первый аргумент равен tru и в третий, если fls (аналогично тренарному оператору в C-подобных языках).

Комбинатор ifThenElse на самом деле почти ничего не делает – это и не требуется, поскольку его поведение по сути закодировано в tru и fls.

Не составляет труда так же определить логические функции, нампример, конъюнкция

and = λx y. x y fls

Упражнение вывести выражения для or, not, xor.

Пары

При помощи булевских констант, можно закодировать пары значений в виде термов. Введём определения

pair = λf s. λb. b f s
fst = λp. p tru
snd = λp. p fls

Определение pair может показаться несколько странным. Оно записано в таком виде, чтобы подчеркнуть, что применение pair к двум аргументам возвращает функцию, которая, в свою очередь, будучи применена к tru вернёт первый аргумент pair, а к fls – второй.

Например,

fst (pair u v)
(λp. p tru) ((λf s. λb. b f s) u v)
(λp. p tru) (λb. b u v)
(λb. b u v) tru
tru u v
(λx y. x) u v
u

Числа Чёрча

После ввода булевской арифметики, разумным выглядит ввести натуральные числа. Стандартная конструкция – числа Чёрча – выглядит следующим образом:

c₀ ≡ λs z. z
c₁ ≡ λs z. s z
c₂ ≡ λs z. s (s z)
c₃ ≡ λs z. s (s (s z))
...

Число n кодируется комбинатором двух аргументов cₙ, который принимает “функцию следования” s и “ноль” z и n раз применяет s к z.

Таким образом, в кодировании Чёрча, число n – это функция, которая что-то делает n раз.

Определим функцию следования, которая, принимая число Чёрча, возвращает следующее число Чёрча:

succ = λn. λs z. s (n s z)

Упражнение предложить другое определение для succ.

Аналогично можно определить сложение

plus = λm n. λs z. m s (n s z)

и умножение

times = λm n. λs z. m (n s) z

Также возможны определения plus и times через succ и plus соответственно:

plus' = λm n. m succ n
times' = λm n. m (plus n) c₀

Упражнение выведите терм для возведения в степень.

Для проверки на равенство 0, нужно передать числу Чёрча в качестве s и z такие функции ss и zz, что применение ss к zz один или более раз даст fls, тогда как zz сам по себе даст tru. Понятно, что в качестве zz можно взять просто tru, а в качестве ss – функцию, всегда возвращающую fls:

iszero = λn. n (λx. fls) tru

Возможно несколько неожиданно, определить функцию вычитания на числах Чёрча оказывается достаточно нетривиально. Для этого используется достаточно “хитрая” функция предшествования, использующая пары чисел, такие, что на каждом шаге применения функции следования, предыдущее число сохраняется как элемент пары:

zz = pair c₀ c₀
ss = λnn. pair (snd nn) (succ (snd nn))
pred = λn. fst (n ss zz)

Стоит отметить, что при таком определении, pred c₀ = c₀. Вообще говоря, это определяется только первым членом пары zz, поэтому несложно изменить эту функцию для поддержки, например, целых чисел (т.е. включая отрицательные).

Упражнение определите функцию вычитания чисел Чёрча используя функцию pred Упражнение определите функцию проверки чисел Чёрча на равенство.

Рекурсия

Интересно отметить, что для некоторых термов, нормальной формы может не существовать. Самый простой пример такого терма – расходящийся комбинатор

omega = (λx. x x) (λx. x x)

Этот комбинатор содержит только один редекс, но один шаг β-редукции снова приводит нас к omega:

  (λx. x x) (λx. x x)
-> [x -> (λx. x x)](x x)
-> (λx. x x) (λx. x x)

Про термы, не имеющие нормальной формы, говорят, что они расходятся.

Комбинатор omega можно обобщить до более полезного комбинатора – комбинатора неподвижной точки, который позволяет использовать рекурсию:

fix = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

У этого комбинатора достаточно сложная структура с повторами, и, возможно, сразу представляется несколько затруднительным понять, как он работает. Смысл его, однако, достаточно прост: мы хотим ввести рекурсию, то есть возможность пользоваться конструкциями вида

f = <тело, содержащее f>

Для этого собственно и используется комбинатор fix:

f = fix (λf. <тело, содержащее f>)

Допустим, мы хотим определить функцию факториала. Используя введённые ранее определения чисел Чёрча, можно записать одну итерацию как

fact1 = λf. λn. ifThenElse (iszero n) c₁ (times n (f (pred n)))

где f – рекурсивный вызов.

Используя комбинатор fix, можем переписать в виде

fact = fix fact1

Рассмотрим, как будет происходить редукция, скажем, выражения fact c₂:

   fact c₂
 = fix fact1 c₂
 = (λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))) fact1 c₂
-> (λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) c₂
-> fact1 (λy. (λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) y) c₂
 = fact1 (λz. (λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) z) c₂
-> ...
-> times c₂ ((λz. (λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) z) c₁)
-> times c₂ ((λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) c₁)
-> ...
-> times c₂ (times c₁ ((λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) c₀))
-> ...
-> times c₂ (times c₁ c₁)
-> ...
-> c₂