Упорядоченная пара и алгебраический тип. Вычитание 1. Бета-эквивалентность (WTF?). Y-комбинатор. Реализация вычисления факториала через Y-комбинатор. Упорядоченной парой термов A и B называется терм \s.s A B. Таким образом, нетрудно придумать функции для работы с подобными конструкциями:
Code
pair = \a.\b.\s.s a b
fst = \p.p True
snd = \p.p False
В дальнейшем для удобства упорядоченные пары будут обозначаться как <A, B>. Рассмотрим представление следующего алгебраического типа в лямбда-исчислении:
Code
type ('a, 'b) x = L of 'a | R of 'b;;
Такой тип позволяет функции возвращать значения двух разных типов =)
Итак, представление в лямбде:
Code
inL = \a.<True, a>
inR = \b.<False, b>
case = \p.\fa.\fb.((fst p) fa fb) (snd p)
Сравните это со следующими записями:
Code
fun a -> L a
fun b -> L b
fun p la lb -> match p with (True, a) -> fa a | (False, b) -> fb b
Нетрудно заметить, что ML-ный синтаксис здесь практически эквивалентен лямбде. Вычитание единицы - весьма нетривиальный трюк. Говорят, он пришёл в голову другу Чёрча, когда тот сидел в кабинете у стоматолога, поэтому называется он "трюком зуба мудрости".
Заметим, что вычитание единицы из n - это то же самое, что прибавление к 0 (n - 1) единицы. Попробуем реализовать программу, выполняющую подобную операцию, на OCaml.
Code
let dec n =
let rec dec acc c =
if c < n then if (fst acc) then dec (true, (snd acc) + 1) (c + 1) else dec (true, snd acc) (c + 1) else snd acc in
dec (false, 0) 0;;
Что-то вроде этого...
Получилось неплохо за одним исключением: сравнение c и n - это нехорошо. К счастью, в лямбде можно избавиться не только от сравнения, но и от второго аргумента функции, так как там числа устроены по-другому:
Code
Dec = \n.\f.\x.snd (n (\p.(fst p)?<True, f (snd p)>:<True, x>) <False, x>)
Штукенберг также давал ещё одну реализацию того же; я в ней не разобрался, но выглядит она... минималистически?
Code
Dec = \n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)
UPD: разобрался 
http://en.wikipedia.org/wiki/Lambda_calculus
Приблизительно посередине статьи, раздел "Arithmetic in lambda calculus", подпункт "Predecessor".
Quote
The predecessor function defined by PRED n = n - 1 for a positive integer n and PRED 0 = 0 is considerably more difficult. The formula
PRED := λnfx.n (λgh.h (g f)) (λu.x) (λu.u)
can be validated by showing inductively that if T denotes (λgh.h (g f)), then T^(n)(λu.x) = (λh.h(f^(n-1)(x))) for n > 0.
Quote
Функция вычитания единицы, определённая как PRED n = n - 1 для натурального n и PRED 0 = 0 является намного более сложной. Формула
PRED := λnfx.n (λgh.h (g f)) (λu.x) (λu.u)
может быть проверена индукцией, если показать, что если T = (λgh.h (g f)), тогда T^(n) (λu.x) = (λh.h (f^(n-1) (x))) при n > 0.
И ещё одна реализация декремента:
Code
Φ := λx.pair (snd x) (Inc (snd x))
PRED := λn.fst (n Φ (pair 0 0))
Бета-эквивалентностью называется транзитивное, рефлексивное и симметричное замыкание
бета-редукции, либо симметричное замыкание бета-редуцируемости.
Y-комбинатором называется следующий терм:
Code
Y = \f.(\x.f (x x)) (\x.f (x x))
У него есть замечательное свойство: (Y F) -b> F (Y F)... Попробуем применить Y-комбинатор для реализации факториала. (На самом деле, конечно, это можно сделать гораздо проще без него.) Сначала заметим, что Y - это почти что цикл while. В самом деле, рассмотрим следующий пример:
Code
T = \f.\x.(IsZero x) 1 (Mul x (f (Dec x)))
fact = Y T -b> ?
Это очень напоминает программу на ML:
Code
let rec fact x =
if x = 0 then 1 else x * (fact (n - 1));;
Как нетрудно заметить, всё довольно просто...
