Lambda calcul et confusion des chiffres d'église

Question

J'essaie de comprendre les bases du calcul lambda et des chiffres de l'Église. J'ai beaucoup lu et pratiqué, mais il me semble que je n'arrive pas à essayer de voir comment certaines fonctions fonctionnent.

L'exemple sur lequel je suis coincé est le suivant. Peut-être que quelqu'un peut expliquer où je me suis trompé.

Le chiffre d'église pour 1 peut être représenté par:

λf. λx. f x

La fonction d’exposition sur les chiffres de l’Eglise (m ⁿ ) peut être définie comme suit:

λm. λn. n m

Tout ce que je veux faire, c'est montrer qu'en appliquant la fonction d'exponentiation à 1 et 1, je récupère 1, puisque 1 ¹ = 1. Je le fais, alors je comprends mieux comment les fonctions fonctionnent. Mon travail est comme suit et je suis coincé à chaque fois:

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

Et là je suis coincé. J'ai perdu les deux f, il ne reste plus que des x et je n'ai pas récupéré 1. Où vais-je mal?

Answer 1

  

Où vais-je mal?

Nulle part! Vous avez terminé. Rappelez-vous, les noms de variables ne sont pas importants; c'est la structure qui est importante. Les noms f ou x2 ne sont pas significatifs. Il importe seulement de savoir comment ils sont utilisés. Le chiffre de l'église pour 1 est

λf. λx. f x

et vous avez

λx2. (λx1. x2 x1)

Renommez x1 en x et <=> en <=> et voil & # 224 ;! Vous avez

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