Lambda calculus i zamieszanie w liczbach kościelnych

Question

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.

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 ⁿ) 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ę?

Answer 1

Gdzie się mylę?

Nigdzie! Jesteś skończony. Pamiętaj, że nazwy zmiennych nie są ważne; ważna jest struktura. Nazwy f lub x2 nie są znaczące. Ma znaczenie tylko, w jaki sposób są używane. Cyfra 1 jest Kościół dla

λf. λx. f x 

i masz

λx2. (λx1. x2 x1) 

Rename x2 do f i x1 do x i voila! Masz

λf. (λx. f x) 
= λf. λx. f x