Реализуем λ-исчисление в матпакетах!

[arseniiv]

Вот пытался построить $\lambda$-исчисление в Mathematica, но выходит не очень. (Знаю-знаю, что там есть "безымянные функции" вида $f[\# ]\&$, которые равноценны $\lambda x.f[x]$, но решил "заново".) Сначала я написал коротко и ясно:

λ /: λ[x_, f_]∘y_ := ReplaceAll[f, x -> y]

(Были ещё дополнительные правила, чтобы не возиться с выражениями, например, для возможности ввода λ[x, y, z, sth], они тут ни при чём.) Но при составлении комбинатора Y, естественно, получалась бесконечная рекурсия — сразу срабатывало правило для $\beta$-редукции, а ни к чему хорошему оно тут не приводит. Хотя с "простыми" выражениями всё работало, что тоже естественно. Тогда я сделал функцию β, которая бы упрощала то, что у неё внутри, пока результат не совпал с каким-нибудь из предыдущих. Тогда она его и оставляла. Всё стало хорошо, но пришлось дописывать куски этой функции, чтобы она работала с любыми выражениями, а не только теми, которые в аксиоме (шаблоны должны быть прописаны явно). Худо-бедно что-то составил, но теперь у меня не редуцируется выражение $\lambda x.\lambda y.(x^2+y^2)$. Уже даже не понимаю, почему.
В общем, у кого есть Mathematica (моя версия 5.0) и кто хочет поиграть с ней в лямбда-исчисление, напишите сюда, что у вас получится! Вдруг есть какие-нибудь довольно простые решения. Я мог легко что-нибудь упустить.
Могу привести свой почти страшный код и некоторые результаты его работы. Кажется, я всё-таки там что-то упустил.
Интересно просто посмотреть, если кто-нибудь делал такую реализацию в других пакетах.

[arseniiv]

Приведу свой последний код.

О, я его сейчас подправил, и он заработал! Тогда точно приведу:

β1[λ[x_, f_]∘y_] := ReplaceAll[f, x -> y]
β1[otherexpr_] := otherexpr

$\beta$-редукция один раз

β[expr_] := Module[
    {results = {}, e = expr},
    While[! OccurQ[e, results],
        AppendTo[results, e = β1[e]]
    ];
    e
]
OccurQ[elem_, list_] := If[ (* MemberQ здесь непригодно *)
    Do[
        If[list[[i]] == elem, Break[True]],
        {i, Length[list]}
    ] === Null,
    False, True
]
β[λexpr_∘y1_∘y2_] := β[β1[λexpr∘y1]∘y2]
β[y1_?(Head[#] =!= λ &)∘y2_] := y1∘β[y2]

$\beta$-редукция до повторения

λ[L_List, f_] := λ[First[L], λ[Rest[L], f]]
λ[{L1_}, f_] := λ[L1, f]
λ[L1_, L2__, f_] := λ[{L1, L2}, f]
SmallCircle[a_, b_, c__] := SmallCircle[SmallCircle[a, b], c]
SmallCircle /: (a∘c) == (b∘c) := a == b
SmallCircle /: (c∘a) == (c∘b) := a == b
λ /: λ[x_, f_] == λ[y_, g_] := β[λ[x, f]∘a$0001] == β[λ[y, f]∘a$0001]

дополнительные правила: для упрощённой записи и для сравнений

Вот пример использования этой писанины:

In :   λ[a, b, a^2 + b^2]∘t∘b // β
Out:   b^2 + t^2

Примеры записи (комбинаторы):

λI  = λ[x, x]
λK  = λ[x, y, x]
λKs = λ[x, y, y]
λS  = λ[x, y, z, x∘z∘(y∘z)]
λY2 = λ[x, f∘(x∘x)] (* Всего лишь кусок из Y *)
λY  = λ[f, λY2∘λY2]

Используя пакет Utilities`Notations`, можно ещё и вывод сделать в "традиционной форме".

[nestoklon]

arseniiv, а того что вы пытаетесь делать нет ли сразу в каком-нибудь хаскеле? У меня есть знакомый фанат этого языка, он что-то похожее грузил.
Просто есть подозрение, что матпакеты не очень хорошо подходят для вашей задачи.

[arseniiv]

Я знаю. Я собрался себе мини-язык составить для этой цели. (Между делом думаю, как лучше оформить конечным автоматом.) А хаскель загружать не хочу... (Кстати, Mathematica, можно сказать, функциональный интерпретатор с большой примесью императивности и математических и других функций. Поэтому там есть встроенные выражения, как я написал выше, но управлять их вычислением не выйдет, да и композиция там правоассоциативна, а мне нужна левая.) А ещё meduza мне предложила мне посмотреть один язык; интересно, но конвертировать исходники его лень в удобоваримый вид (вроде он на Python).

Но хотя бы я ещё раз убедился, что могу вертеть Mathematic'ой как хочу.

-- Чт янв 07, 2010 21:28:45 --

Кстати, в обычной нотации Mathematica $\lambda x.\lambda y.(x^2+y^2)$ можно записать двояко, в отличие от $\lambda$-исчисления:

f = #1^2 + #2^2 &
f[a, b]

f = With[{t = #}, t^2 + #^2 &] &
f[a][b]

В lisp этому соответствовали бы вызовы

(f a b)

((f a) b)