Anonimowa rekurencja
Kombinator stałoprzecinkowy jest funkcją wyższego rzędu, fix
która z definicji spełnia równoważność
forall f. fix f = f (fix f)
fix f
przedstawia rozwiązanie x
równania stałego punktu
x = f x
Silnia liczby naturalnej można udowodnić za pomocą
fact 0 = 1
fact n = n * fact (n - 1)
Używanie fix
dowolnych konstruktywnych dowodów na funkcje ogólne / μ-rekurencyjne można uzyskać bez nonimowej autoreferencyjności.
fact n = (fix fact') n
gdzie
fact' rec n = if n == 0
then 1
else n * rec (n - 1)
takie, że
fact 3
= (fix fact') 3
= fact' (fix fact') 3
= if 3 == 0 then 1 else 3 * (fix fact') (3 - 1)
= 3 * (fix fact') 2
= 3 * fact' (fix fact') 2
= 3 * if 2 == 0 then 1 else 2 * (fix fact') (2 - 1)
= 3 * 2 * (fix fact') 1
= 3 * 2 * fact' (fix fact') 1
= 3 * 2 * if 1 == 0 then 1 else 1 * (fix fact') (1 - 1)
= 3 * 2 * 1 * (fix fact') 0
= 3 * 2 * 1 * fact' (fix fact') 0
= 3 * 2 * 1 * if 0 == 0 then 1 else 0 * (fix fact') (0 - 1)
= 3 * 2 * 1 * 1
= 6
Ten formalny dowód na to
fact 3 = 6
metodycznie używa równoważnika kombinatora stałoprzecinkowego do przepisywania
fix fact' -> fact' (fix fact')
Rachunek Lambda
Bez typu rachunek lambda formalizm polega na gramatyki bezkontekstowych
E ::= v Variable
| λ v. E Abstraction
| E E Application
gdzie v
rozciąga się na zmienne, wraz z regułami redukcji beta i eta
(λ x. B) E -> B[x := E] Beta
λ x. E x -> E if x doesn’t occur free in E Eta
Redukcja beta zastępuje wszystkie wolne wystąpienia zmiennej x
w ciele abstrakcji („funkcja”) B
wyrażeniem („argument”) E
. Redukcja Eta eliminuje zbędną abstrakcję. Czasem jest to pomijane w formalizmie. Irreducible wypowiedzi, do których ma zastosowanie reguła nie redukcja, jest w normalnym lub postaci kanonicznej .
λ x y. E
jest skrótem od
λ x. λ y. E
(różnorodność abstrakcyjna),
E F G
jest skrótem od
(E F) G
(lewe skojarzenie aplikacji),
λ x. x
i
λ y. y
są równoważne alfa .
Abstrakcja i zastosowanie to dwa jedyne „prymitywy językowe” rachunku lambda, ale umożliwiają kodowanie dowolnie złożonych danych i operacji.
Cyfry kościelne są kodowaniem liczb naturalnych podobnych do Peano-aksomatycznych naturałów.
0 = λ f x. x No application
1 = λ f x. f x One application
2 = λ f x. f (f x) Twofold
3 = λ f x. f (f (f x)) Threefold
. . .
SUCC = λ n f x. f (n f x) Successor
ADD = λ n m f x. n f (m f x) Addition
MULT = λ n m f x. n (m f) x Multiplication
. . .
Formalny dowód na to
1 + 2 = 3
używając reguły przepisywania redukcji wersji beta:
ADD 1 2
= (λ n m f x. n f (m f x)) (λ g y. g y) (λ h z. h (h z))
= (λ m f x. (λ g y. g y) f (m f x)) (λ h z. h (h z))
= (λ m f x. (λ y. f y) (m f x)) (λ h z. h (h z))
= (λ m f x. f (m f x)) (λ h z. h (h z))
= λ f x. f ((λ h z. h (h z)) f x)
= λ f x. f ((λ z. f (f z)) x)
= λ f x. f (f (f x)) Normal form
= 3
Kombinatory
W rachunku lambda kombinatory są abstrakcjami, które nie zawierają wolnych zmiennych. Najprościej: I
kombinator tożsamości
λ x. x
izomorficzny do funkcji tożsamości
id x = x
Takie kombinatory są prymitywnymi operatorami rachunku kombinatorycznego, takimi jak system SKI.
S = λ x y z. x z (y z)
K = λ x y. x
I = λ x. x
Redukcja beta nie jest silnie normalizująca ; nie wszystkie redukowalne wyrażenia, „redeksy”, zbiegają się do normalnej formy przy redukcji beta. Prostym przykładem jest rozbieżne zastosowanie ω
kombinatora omega
λ x. x x
Do siebie:
(λ x. x x) (λ y. y y)
= (λ y. y y) (λ y. y y)
. . .
= _|_ Bottom
Priorytetem jest redukcja skrajnych lewych podwyrażeń („głów”). Kolejność stosowania normalizuje argumenty przed podstawieniem, normalna kolejność nie. Dwie strategie są analogiczne do chętnej oceny, np. C, i leniwej oceny, np. Haskell.
K (I a) (ω ω)
= (λ k l. k) ((λ i. i) a) ((λ x. x x) (λ y. y y))
rozbiega się pod niecierpliwą redukcją wersji beta zamówień
= (λ k l. k) a ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ y. y y) (λ y. y y))
. . .
= _|_
ponieważ w ścisłej semantyce
forall f. f _|_ = _|_
ale zbiega się pod leniwą redukcją beta normalnego rzędu
= (λ l. ((λ i. i) a)) ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ x. x x) (λ y. y y))
= a
Jeśli wyrażenie ma normalną formę, odnajdzie ją redukcja beta normalnego rzędu.
Y
Zasadnicza właściwość Y
kombinatora stałoprzecinkowego
λ f. (λ x. f (x x)) (λ x. f (x x))
jest dany przez
Y g
= (λ f. (λ x. f (x x)) (λ x. f (x x))) g
= (λ x. g (x x)) (λ x. g (x x)) = Y g
= g ((λ x. g (x x)) (λ x. g (x x))) = g (Y g)
= g (g ((λ x. g (x x)) (λ x. g (x x)))) = g (g (Y g))
. . . . . .
Równoważność
Y g = g (Y g)
jest izomorficzny
fix f = f (fix f)
Rachunek lambda bez typu może kodować arbitralne konstruktywne dowody nad funkcjami ogólnymi / μ-rekurencyjnymi.
FACT = λ n. Y FACT' n
FACT' = λ rec n. if n == 0 then 1 else n * rec (n - 1)
FACT 3
= (λ n. Y FACT' n) 3
= Y FACT' 3
= FACT' (Y FACT') 3
= if 3 == 0 then 1 else 3 * (Y FACT') (3 - 1)
= 3 * (Y FACT') (3 - 1)
= 3 * FACT' (Y FACT') 2
= 3 * if 2 == 0 then 1 else 2 * (Y FACT') (2 - 1)
= 3 * 2 * (Y FACT') 1
= 3 * 2 * FACT' (Y FACT') 1
= 3 * 2 * if 1 == 0 then 1 else 1 * (Y FACT') (1 - 1)
= 3 * 2 * 1 * (Y FACT') 0
= 3 * 2 * 1 * FACT' (Y FACT') 0
= 3 * 2 * 1 * if 0 == 0 then 1 else 0 * (Y FACT') (0 - 1)
= 3 * 2 * 1 * 1
= 6
(Mnożenie opóźnione, konfluencja)
W przypadku kościelnego rachunku lambda bez typu wykazano, że istnieje poza tym rekurencyjnie wyliczalna nieskończoność kombinatorów stałoprzecinkowych Y
.
X = λ f. (λ x. x x) (λ x. f (x x))
Y' = (λ x y. x y x) (λ y x. y (x y x))
Z = λ f. (λ x. f (λ v. x x v)) (λ x. f (λ v. x x v))
Θ = (λ x y. y (x x y)) (λ x y. y (x x y))
. . .
Redukcja beta w normalnym rzędzie sprawia, że nierozwinięty niepoprawny rachunek lambda jest kompletnym systemem przepisywania Turinga.
W Haskell kombinator stałoprzecinkowy można elegancko zaimplementować
fix :: forall t. (t -> t) -> t
fix f = f (fix f)
Leniwość Haskella normalizuje się do skończoności, zanim wszystkie podwyrażenia zostaną ocenione.
primes :: Integral t => [t]
primes = sieve [2 ..]
where
sieve = fix (\ rec (p : ns) ->
p : rec [n | n <- ns
, n `rem` p /= 0])