Czy kilkaset kroków redukcji jest zbyt wiele, aby uzyskać normalną postać Y fac ⌜3⌝?

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…

Kodowanie kościoła jest naprawdę złe, jeśli chcesz go używać pred. Radzę ci użyć bardziej wydajnego kodowania w stylu Peano:

// arytmetyka

: p_zero = λs.λz.z
: p_one = λs.λz.s p_zero
: p_succ = λn.λs.λz.sn
: p_null = λn.n (λx. ff) tt
: p_pred = λn.n (λp.p) p_zero
: p_plus = μ! f.λn.λm.n (λp. p_succ (! fpm)) m
: p_subs = μ! f.λn.λm.n (λp. p_pred (! fpm)) m
: p_eq = μ! f.λm.λn. m (λp. n (λq.! fpq) ff) (n (λx.ff) tt)
: p_mult = μ! f.λm.λn. m (λp. p_plus n (! fpn)) p_zero
: p_exp = μ! f.λm.λn. m (λp. p_mult n (! fpn)) p_one
: p_even = μ! f.λm. m (λp. not (! fp)) tt

// liczby

: p_0 = λs.λz.z
: p_1 = λs.λz.s p_0
: p_2 = λs.λz.s p_1
: p_3 = λs.λz.s p_2
...

To jest kod pobrany z jednej z moich starych bibliotek i μ!f. …był to po prostu zoptymalizowana konstrukcja Y (λf. …). (I tt, ff, notsą wartości logiczne).

Nie jestem jednak pewien, czy uzyskałbyś lepsze wyniki fac.

Jeśli zastanowię się, ile rzeczy robi procesor, aby obliczyć silnię 3, powiedzmy w Pythonie, to kilkaset redukcji nie jest wcale wielkim problemem.