Lambda calcul et confusion des chiffres d'église
-
20-08-2019 - |
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 n ) 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 = 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?
La solution
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