Calcolo lambda e confusione di numeri di chiesa

Question

Sto cercando di capire le basi del calcolo lambda e dei numeri della Chiesa. Ho letto e praticato molto, ma mi sembra di rimanere bloccato nel tentativo di vedere come funzionano alcune funzioni.

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

Il numero della Chiesa per 1 può essere rappresentato come:

λf. λx. f x

La funzione di esponenziale sui numeri della Chiesa (m ⁿ ) può essere data come:

λm. λn. n m

Tutto quello che voglio fare è mostrare che applicando la funzione di esponenziale a 1 e 1, torno indietro di 1, poiché 1 ¹ = 1. Lo sto facendo, quindi capisco meglio come questi funzioni funzionano. Il mio lavoro è il seguente e rimango bloccato 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)

Ed eccomi bloccato. Ho perso entrambi f, rimasto solo con x e non ne ho 1 indietro. Dove sto sbagliando?

Answer 1

  

Dove sbaglio?

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. Il numero della Chiesa per 1 è

λf. λx. f x

e tu hai

λx2. (λx1. x2 x1)

Rinomina x1 in x e <=> in <=> e voil & # 224 ;! Hai

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