Ponieważ ostatnio uczę podstaw rachunku λ, wdrożyłem prosty ewaluator λ w Common Lisp. Kiedy pytam o normalną formę Y fac 3redukcji w normalnym porządku, zajmuje to 619 kroków, co wydawało się trochę za dużo.
Oczywiście, za każdym razem, gdy robiłem podobne redukcje na papierze, nigdy nie korzystałem z nietypowego rachunku λ, ale dodawałem na nich liczby i funkcje. W takim przypadku fac jest zdefiniowany jako taki:
fac = λfac.λn.if (= n 0) 1 (* n (fac (- n 1)))
W tym przypadku, biorąc pod uwagę =, *a -jak currying funkcje, to zajmie tylko około 50 kroków, aby dostać się Y fac 3do swojej normalnej postaci 6.
Ale w moim ewaluatorze zastosowałem:
true = λx.λy.x
false = λx.λy.y
⌜0⌝ = λf.λx.x
succ = λn.λf.λx.f n f x
⌜n+1⌝ = succ ⌜n⌝
zero? = λn.n (λx.false) true
mult = λm.λn.λf.m (n f)
pred = λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
fac = λfac.λn.(zero? n) ⌜1⌝ (* n (fac (pred n)))
Y = λf.(λf.λx.f (x x)) f ((λf.λx.f (x x)) f)
W 619 krokach przechodzę Y fac ⌜3⌝do normalnej postaci ⌜6⌝, mianowicie λf.λx.f (f (f (f (f (f x))))).
Po szybkim przejrzeniu wielu kroków, wydaje mi się, że jest to definicja, predktóra gwarantuje tak długą redukcję, ale wciąż zastanawiam się, czy to może być duży, paskudny błąd w mojej implementacji ...
EDYCJA: Początkowo poprosiłem o tysiąc kroków, z których niektóre rzeczywiście spowodowały nieprawidłową implementację normalnej kolejności, więc zszedłem do 2/3 początkowej liczby kroków. Jak skomentowałem poniżej, przy mojej obecnej implementacji przejście z arytmetyki Peano na Kościół faktycznie zwiększa liczbę kroków…