Вы можете использовать любой нетипизированный язык с лямбда-абстракциями. Например, Python или JavaScript. Есть два основных недостатка:
- Эти языки не имеют ленивой оценки. Это означает, что не все лямбда-члены будут сходиться, даже если они имеют нормальную форму. Вы должны принять это во внимание и соответственно изменить задачу.
- Вы не увидите результат в виде лямбда-термина в нормальной форме. Вы должны знать, чего ожидать от результата, и использовать язык для его оценки, чтобы можно было что-то отобразить.
Зная это, давайте сделаем пример на Python:
Сначала мы создаем вспомогательные функции для преобразования между числами и церковными цифрами:
# Construct Church numeral from an integer
def int2church(n):
def repeat(f, m, x):
if (m == 0): return x
else: return f(repeat(f, m-1, x))
return lambda f: (lambda x: repeat(f, n, x))
def church2int(l):
return l(lambda x: x + 1)(0)
теперь мы можем определить стандартные операции над числами:
zero = int2church(0)
one = int2church(1)
pred = lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f)))(lambda u: x)(lambda u: u)
mul = lambda m: lambda n: (lambda f: m(n(f)))
expn = lambda n: lambda m: m(n)
tetra = lambda n: lambda m: m(expn(n))(one)
и вычислите, например, 4 3 :
expn = lambda n: (lambda m: m(n))
a = int2church(4)
b = int2church(3)
print church2int(expn(a)(b))
или тетрация :
a = int2church(5)
b = int2church(2)
print church2int(tetra(a)(b))
Чтобы выразить еще более интересные вещи, мы можем определить Y комбинатор:
y = lambda f: (lambda x: f(lambda v: x(x)(v))) (lambda x: f(lambda v: x(x)(v)))
и вычислить, например, факториалы:
true = lambda x: (lambda y: x)
false = lambda x: (lambda y: y)
iszero = lambda n: n(lambda x: false)(true)
fact = y(lambda r: lambda n: iszero(n)(one)(mul(n)(lambda x: r(pred(n))(x))))
print church2int(fact(int2church(6)))
Обратите внимание, что комбинатор Y пришлось адаптировать для строгой оценки, используя η-расширение , а также функцию факториала, чтобы избежать бесконечной рекурсии из-за строгой оценки.