Dane wejściowe i wyjściowe jako liczby kościelne .
00000000 01011111 01100101 11101101 0
W rachunku lambda jest to λ m . λ n . λ f . λ x . m f ( n f x ).
Indeks De Bruijna : λ λ λ λ 4 2 (3 2 1)
Rachunek lambda to zwięzły sposób opisu odwzorowania (funkcji).
Na przykład to zadanie można zapisać jako λ x . λ y . x + y
Należy zauważyć, że nie jest to lambda (funkcja), która przyjmuje dwa argumenty. To właściwie zagnieżdżona lambda. Zachowuje się jednak jak lambda, która przyjmuje dwa argumenty, więc można go nieformalnie opisać jako taki. Każda lambda formalnie bierze tylko jeden argument.
Na przykład, jeśli zastosujemy tę lambda do 3 i 4:
(λ x . λ y . x + y ) 3 4 ≡ (λ y . 3 + y ) 4 ≡ 3 + 4 = 7
Tak więc pierwsza lambda faktycznie zwraca inną lambda.
Cyfry kościelne to sposób na pozbycie się dodatkowych znaków, pozostawiając tylko symbole i zmienne lambda.
Każda liczba w systemie kościelnym jest w rzeczywistości lambda, która określa, ile razy funkcja jest stosowana do elementu.
Niech funkcją będzie f, a elementem będzie x .
Tak więc liczba 1 odpowiada λ f . λ x . f x , co oznacza zastosowanie f do x dokładnie raz.
Na przykład liczba 3 to λ f . λ x . f ( f ( f x )), co oznacza zastosowanie f do x dokładnie trzy razy.
W związku z tym, dodanie dwóch cyfr Church (powiedzmy, m i n ) ze sobą, to jest takie same jak zastosowania F do x , m + n razy.
Możemy zauważyć, że jest to to samo, co najpierw zastosowanie f do x , n razy, a następnie zastosowanie f do uzyskanego elementu m razy.
Na przykład 2 oznaczałoby, f(f(x))
a 3 oznaczałoby f(f(f(x)))
, więc 2 + 3 byłoby f(f(f(f(f(x)))))
.
Aby zastosować f do x , n razy, mamy n f x .
Można zobaczyć m i n jako funkcje biorąc dwa argumenty, nieformalnie.
Następnie ponownie stosujemy f do tego wynikowego elementu, m razy: m f ( n f x ).
Następnie dodajemy z powrotem płytę kotła, aby uzyskać λ m . λ n . λ f . λ x . m f ( n f x ).
Teraz musimy przekonwertować go na indeks De Bruijn .
Po pierwsze, liczymy „względną odległość” między każdą zmienną do deklaracji lambda. Na przykład m miałoby odległość 4, ponieważ zadeklarowano 4 jagnięta „temu”. Podobnie, n miałoby odległość 3, f miałoby odległość 2, a x miałby odległość 1.
Piszemy to jako następującą formę pośrednią: λ m . λ n . λ f . λ x . 4 2 (3 2 1)
Następnie usuwamy deklaracje zmiennych, pozostawiając nam: λ λ λ λ 4 2 (3 2 1)
Teraz konwertujemy go na binarny rachunek lambda .
Reguły są następujące:
- λ staje się
00
.
- m n (grupowanie) staje się
01 m n
.
- liczby i stają się
1
i razy + 0
, na przykład 4 staje się 11110
.
λ λ λ λ 4 2 (3 2 1)
≡ λ λ λ λ 11110
110
( 1110
110
10
)
≡ λ λ λ λ 11110
110
0101 111011010
≡ λ λ λ λ 0101
111101100101111011010
≡ 00
00
00
00
0101
111101100101 111011010
≡ 000000000101111101100101111011010