В умножении чисел m и n мы будем m раз складывать число n:
M ul = λm n s z. m ( Add n) Zero
Лямбда исчисление без типов | 221
Конструктивная математика
В конструктивной математике существование объекта может быть доказано только описанием алгорит-
ма, с помощью которого можно построить объект. Например доказательство методом “от противного” от-
вергается.
Лямбда исчисление строит конструктивное описание функции. По лямбда-терму мы можем не только
вычислять значения функции, но и понять как она была построена. В классической теории, функция это
множество пар ( x, f( x)) аргумент-значение, которое обладает свойством:
x = y ⇒ f ( x) = f ( y)
По этому определению мы ничего не можем сказать о внутренней структуре функции. Мы можем со-
бирать из одних функций другие с помощью подстановки значений, но мы никак не сможем понять, что
находится внутри функции. Лямбда исчисление решает эту проблему.
Расширение лямбда исчисления
Предположим, что мы решили написать язык программирования на основе лямбда-исчисления. Было бы
очень неэффективно представлять числа с помощью чисел Пеано. Ведь у нас есть процессор и мы можем
спросить у него чему равно значение и получить ответ очень быстро.
В этом случае пользуются расширенным лямбда исчислением. В нём два типа примитивов это перемен-
ные и константы. Для констант мы можем определять специальные правила редукции. Например мы можем
дополнить исчисление константами:
+ , ∗, 0 , 1 , 2 , ...
И ввести для них правила редукции, которые запрашивают ответ у процессора:
a + b
=
AddW ithCP U ( a, b)
a ∗ b = M ulW ithCP U ( a, b)
Так же мы можем определить и константы для логических значений:
T rue, F alse, If, N ot, And, Or
И определить правила редукции:
If T rue a b
=
a
If F alse a b
=
b
N ot T rue
=
F alse
N ot F alse
=
T rue
Add F alse a
=
F alse
Add T rue b
=
b
. . .