Próbuję zrozumieć podstawy rachunku lambda i liczebników Kościoła. Dużo czytałem i ćwiczyłem, ale wydaje mi się, że utknąłem, próbując zobaczyć, jak działają niektóre funkcje.Lambda calculus i zamieszanie w liczbach kościelnych
Przykłąd, na którym utknąłem, jest następujący. Być może ktoś może wyjaśnić, gdzie popełniłem błąd.
Kościół liczbowy dla 1 może być przedstawione jako:
λf. λx. f x
Funkcja potęgowanie na cyframi Church (m n) można otrzymać jako:
λm. λn. n m
Wszystko co chce zrobić jest pokazane, że przez zastosowanie funkcji potęgowania do 1 i 1, wracam 1, ponieważ 1 = 1. Robię to, więc lepiej rozumiem, jak działają te funkcje. Moja praca jest następująca i utknęłam za każdym razem:
// Exp (1 1)
(λm. λn. n m) (λf1. λx1. f1 x1) (λf2. λx2. f2 x2)
// Substitute for m
(λn. n (λf1. λx1. f1 x1)) (λf2. λx2. f2 x2)
// Substitute for n
(λf2. λx2. f2 x2) (λf1. λx1. f1 x1)
// Substitute for f2
(λx2. (λf1. λx1. f1 x1) x2)
// Substitute for f1
λx2. (λx1. x2 x1)
I tam utknąłem. Zgubiłem oba numery: f
, pozostałe po x
i nie otrzymałem 1 kopii. Gdzie się mylę?
Dziękuję bardzo. Nie masz pojęcia, ile arkuszy złomu papieru wypełniłem (i przeklinałem) próbując zrobić to i podobne problemy "pracy" zanim miałem twój wgląd! – nodmonkey