Lambda réduction Calcul

Question

Tous,

Ci-dessous l'expression lambda que je me rends compte difficile à réduire dire que je ne suis pas en mesure de comprendre comment s'y prendre ce problème.

(Xm lambda N Àa Xb m (nab) b.) (Λ f x x.) (Λ f x fx.)

C'est ce que j'ai essayé, mais je suis coincé:

Considérant l'expression ci-dessus: (. λf x x) (λm.E) m équivaut à
E = (. lambda N Xa Xb m (nab) b)
m = (. λ f x fx)

= > (λn λa λb. (λ f x. x) (λ f x. fx) (nab) b)

C Considérant l'expression ci-dessus comme (λn. E) M est égal à
E = (λa λb. (Λ f x. X) (λ f x. F x) (n a b) b)
M = ??

.. et je suis perdu !!

Quelqu'un peut-il s'il vous plaît m'aider à comprendre que, pour toute expression de lambda-calcul, quelles devraient être les étapes pour effectuer une réduction?

Answer 1

Vous pouvez suivre les étapes suivantes pour réduire les expressions lambda:

1. Entièrement entre parenthèses l'expression pour éviter les erreurs et rendre plus évident l'endroit où l'application de la fonction a lieu.
2. Recherchez une application de fonction, c'est-à-dire que vous trouvez une occurrence du modèle (λX. e1) e2 où X peut être un identificateur valide et e1 et e2 peuvent être des expressions valides.
3. appliquer la fonction par le remplacement (λx. e1) e2 avec e1' où e1' est le résultat du remplacement de chaque occurrence libre de x en e1 avec e2.
4. Répétez les étapes 2 et 3 jusqu'à ce que le motif ne se reproduise plus. Notez que cela peut conduire à une boucle infinie pour les expressions non-normalisation, de sorte que vous devriez arrêter après 1000 itérations ou alors ;-)

Donc, pour votre exemple, nous commencer par l'expression

((λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))) (λf. (λx. (f x))) 

ici la sous-expression (λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x)) correspond à notre modèle avec X = m, e1 = (λn. (λa. (λb. (m ((n a) b)) b)))) et e2 = (λf. (λx. x)). Ainsi, après substitution, nous obtenons (λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))), ce qui rend notre expression entière:

(λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))) (λf. (λx. (f x))) 

Maintenant, nous pouvons appliquer le modèle à l'ensemble de l'expression avec X = n, e1 = (λa. (λb. ((λf. (λx. x)) ((n a) b)) b)) et e2 = (λf. (λx. (f x))). Donc, après avoir remplacé nous obtenons:

(λa. (λb. ((λf. (λx. x)) (((λf. (λx. (f x))) a) b)) b)) 

maintenant ((λf. (λx. (f x))) a) correspond à notre modèle et devient (λx. (a x)), ce qui conduit à:

(λa. (λb. ((λf. (λx. x)) ((λx. (a x)) b)) b)) 

Cette fois, nous pouvons appliquer le modèle à ((λx. (a x)) b), ce qui réduit à (a b), conduisant à :

(λa. (λb. ((λf. (λx. x)) (a b)) b)) 

maintenant, appliquez le modèle à ((λf. (λx. x)) (a b)), ce qui réduit à (λx. x) et obtenez:

(λa. (λb. b)) 

Maintenant nous avons terminé.

Answer 2

où vous allez mal est que dans la première étape, vous ne pouvez pas avoir

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

parce que l'expression originale ne comprend pas cette expression d'application. Pour que cela soit clair, vous pouvez mettre dans les parenthèses implicites qui suit la règle selon laquelle l'application est laissée associative (en utilisant [et] pour les nouveaux parens et de mettre dans certains disparus s « »):

[ (λm . λn . λa . λb . m (n a b) b) (λ f x. x) ] (λ f x. f x) 

De là, , trouver une expression de la forme (λv.E) M certains où à l'intérieur et le réduire en remplaçant v par M en E. Attention, c'est vraiment une application de la fonction à M: ce n'est pas si vous avez quelque chose comme N (λv.E) M, puisque N est appliqué à la fonction et M comme deux arguments. Si vous êtes toujours bloqué, essayez de mettre dans les parens pour chaque lambda aussi - fondamentalement un nouveau "(" après chaque ".", Et un "" correspondant) qui va aussi loin que possible vers la droite tout en restant appariement. le nouveau « (» A titre d'exemple, je l'ai fait un ici (en utilisant [et] pour les faire sortir):

((λm . λn . λa . [λb . m (n a b) b]) (λ f x. x)) (λ f x. f x)