Cálculo lambda y números de la iglesia confusión

Question

Estoy tratando de entender los conceptos básicos del cálculo lambda y los números de la Iglesia. He estado leyendo y practicando mucho, pero parece que sigo atascado tratando de ver cómo funcionan algunas funciones.

El ejemplo en el que estoy atascado es el siguiente. Quizás alguien pueda explicar dónde me he equivocado.

La Iglesia numeral de 1 puede ser representada como:

λf. λx. f x 

La función de exponenciación en números Iglesia (m ⁿ) se puede dar como:

λm. λn. n m 

Todo lo que quieren hacer es mostrar que al aplicar la función de exponenciación a 1 y 1, obtengo 1, ya que 1 = 1. Estoy haciendo esto, así que entiendo mejor cómo funcionan estas funciones. Mi trabajo es el siguiente y me quedo atascado cada vez:

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

Y allí estoy atascado. Perdí los f, me quedé solo con x, y no tengo 1 de vuelta. ¿Dónde estoy equivocado?

Answer 1

¿Dónde me estoy equivocando?

Nowhere! Ya terminaste Recuerde, los nombres de las variables no son importantes; es la estructura lo que es importante. Los nombres f o x2 no son significativos. Solo importa cómo se usan. El número 1 es para la Iglesia

λf. λx. f x 

y tiene

λx2. (λx1. x2 x1) 

Renombrar x2-f y x1-x y listo! Usted tiene

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