Réduction d'expression Lambda

Question

Je suis incapable de résoudre l'expression Lambda suivante en utilisant la réduction de commande normale (appel d'appel) et d'ordre applicatif (appel d'appel).Je continue à obtenir des réponses différentes pour les deux.C'est l'expression de la Lambda qui doit être réduite à l'aide des deux techniques:

$ (\ lambda f \ x \ ldotp f \ (f \ x)) \ (\ lambda f \ x \ ldotp f \ (f \ x)) \ fx $

Answer 1

Je continue à obtenir des réponses différentes pour les deux.

Vous devriez obtenir le même résultat pour les deux commandes. S'il vous plaît montrer votre travail pour que la communauté puisse vous aider à trouver votre erreur.

Je suppose que vous avez une hypothèse substituée par erreur $ f $ au lieu de $ x $ vers la fin, Quand $ f $ est en fait libre.

La procédure de réduction correcte est indiquée ci-dessous.

---

$ (\ lambda f \ x \ ldotp f \ (f \ x)) \ (\ lambda f \ x \ ldotp f \ (f \ x)) \ f x $

Il n'y a pas de différence entre l'ordre normal et l'ordre applicatif à la première étape.

$ (\ lambda f \ x \ ldotp f \ (f \ x) \ ((\ lambda f \ x \ ldotp f \ (f \ x)) \ f ) \ x $

---

À cette étape, il y a une différence, car la valeur étant appliquée à, $ ((\ lambda f \ x \ ldotp f \ (f \ x)) \ f) $ n'est pas sous la forme bêta normale. Ignorons-le et utilisons la commande normale en premier.

Commande normale

$ ((\ lambda f \ x \ ldotp f \ (f \ x)) \ f) \ (((((\ lambda f \ x \ ldotp f \ (f \ x)) \ f) \ x) $

$ (\ lambda x \ ldotp \ f \ (f \ x)) \ ((((\ lambda f \ x \ ldotp f \ (f \ x)) \ f ) \ x) $

$ f \ (f \ ((((\ lambda f \ x \ ldotp f \ (f \ x)) \ x)) $ < / p>

$ f \ (f \ (f \ (f \ x)) $

---

Revenons à la première étape.

$ (\ lambda f \ x \ ldotp f \ (f \ x) \ ((\ lambda f \ x \ ldotp f \ (f \ x)) \ f ) \ x $

---

Cette fois utilisez l'ordre applicatif

Ordre d'application

$ (\ lambda f \ x \ ldotp f \ (f \ x)) \ (\ lambda x \ ldotp f \ (f \ x)) \ x

$ (\ lambda x \ ldotp f \ (f \ x)) \ ((\ lambda x \ ldotp f \ (f \ x)) \ x) $

$ (\ lambda x \ ldotp f \ (f \ x)) \ (f \ (f \ x) $) $

$ f \ (f \ (f \ (f \ x)) $

---

avec ordre normal, nous avons réduit l'expression à:

$ f \ (f \ (f \ (f \ x)) $

avec commande applicative, nous avons réduit l'expression à:

$ f \ (f \ (f \ (f \ x)) $

Les résultats sont les mêmes.