Парсването се извършва чрез индиректна рекурсия на няколко функции и две помощни:
(upper-split "TheQ.uickBro.wnFox(Ju.mps(Ove.r)).(The)LazyDog" #\.) =>
("TheQ" "uickBro" "wnFox" "(Ju.mps(Ove.r))" "(The)LazyDog")
Тази функция се използва с разделители #\. и #\λ и се използва, за да се запазят правилата на скобите
(tokenize "pe(sh)o(g(osho))a")=>
("p" "e" "(sh)" "o" "(g(osho))" "a")
Правейки същото съображение като upper-split, тази се използва за парсване на ниво апликация:
λxyz.xz(yz)
1) На израза и всеки негов директен подизраз съпоставяме буква за тип:
TERM: λfx.f(fx) λf.λx.(f(fx)): ζ λx.(f(fx)): ε (f(fx)): δ (fx): γ x: β f: α
2) Типовете от предната стъпка и правилата на ламбда смятането ни позволяват да изведем още такива твърдения:
λf.λx.(f(fx)): (α→ε)
λf.λx.(f(fx)): ((β→θ)→ε)
λf.λx.(f(fx)): ((γ→η)→ε)
λf.λx.(f(fx)): (α→(β→δ))
λf.λx.(f(fx)): ((β→θ)→(β→δ))
λf.λx.(f(fx)): ((γ→η)→(β→δ))
λx.(f(fx)): (β→δ)
f: (γ→η)
f: (β→θ)
λf.λx.(f(fx)): ζ
λx.(f(fx)): ε
(f(fx)): δ
(fx): γ
x: β
f: α
3) Използвайки изразите и съответните им типове от стъпка 2, можем да построим релация на еквивалентност между типове, които задължително са еднакви:
δ <-> β
γ <-> δ
β <-> η
β <-> θ
η <-> θ
γ <-> β
θ <-> γ
η <-> γ
θ <-> δ
η <-> δ
(β→θ) <-> α
(γ→η) <-> α
(γ→η) <-> (β→θ)
(β→δ) <-> ε
((γ→η)→(β→δ)) <-> ζ
((β→θ)→(β→δ)) <-> ζ
((β→θ)→(β→δ)) <-> ((γ→η)→(β→δ))
(α→(β→δ)) <-> ζ
(α→(β→δ)) <-> ((γ→η)→(β→δ))
(α→(β→δ)) <-> ((β→θ)→(β→δ))
((γ→η)→ε) <-> ζ
((γ→η)→ε) <-> ((γ→η)→(β→δ))
((γ→η)→ε) <-> ((β→θ)→(β→δ))
((γ→η)→ε) <-> (α→(β→δ))
((β→θ)→ε) <-> ζ
((β→θ)→ε) <-> ((γ→η)→(β→δ))
((β→θ)→ε) <-> ((β→θ)→(β→δ))
((β→θ)→ε) <-> (α→(β→δ))
((β→θ)→ε) <-> ((γ→η)→ε)
(α→ε) <-> ζ
(α→ε) <-> ((γ→η)→(β→δ))
(α→ε) <-> ((β→θ)→(β→δ))
(α→ε) <-> (α→(β→δ))
(α→ε) <-> ((γ→η)→ε)
(α→ε) <-> ((β→θ)→ε)
((β→β)→(β→β))
4) Взимаме най-дългия типов израз за нашия ламбда терм от стъпка 2 и чрез еквивалентностите от стъпка 3 заменяме всеки примитивен тип /гръцка буква/ с най-малкия по азбучен ред негов еквивалентен, за да получим възможно най-малко променливи в резултата:
λfx.f(fx) има тип ((β→β)→(β→β)).