confusione di Lambda e numeri di chiesa confusione

Question

Sto cercando di capire le basi del calcolo lambda e dei numeri di Chiesa. Ho fatto molta lettura e pratica, ma mi sembra di rimanere bloccato nel cercare di vedere come funzionano alcune funzioni.

L'esempio su cui sono bloccato è il seguente. Forse qualcuno può spiegare dove ho sbagliato.

La Chiesa cifra per 1 può essere rappresentata come:

λf. λx. f x 

La funzione di elevazione a potenza in cifre della Chiesa (m ⁿ) può essere somministrato come:

λm. λn. n m 

Tutto quello che voglio fare è mostrare che applicando la funzione di esponenziazione a 1 e 1, torno indietro 1, dal 1 = 1. Sto facendo questo, quindi capisco meglio come funzionano queste funzioni. Il mio lavoro è il seguente e mi blocco ogni volta:

// 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) 

E lì sono bloccato. Ho perso entrambi f, lasciato solo con x, e non ne ho ricevuto 1. Dove sto andando male?

Answer 1

Dove sto andando male?

Da nessuna parte! Hai finito. Ricorda, i nomi delle variabili non sono importanti; è la struttura che è importante. I nomi f o x2 non sono significativi. Importa solo come vengono utilizzati. La cifra Chiesa per 1 è

λf. λx. f x 

e si dispone

λx2. (λx1. x2 x1) 

Rinominare x2-f e x1-x e voilà! Hai

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