Reducción de la expresión lambda

Question

No puedo resolver la siguiente expresión de lambda usando ambos orden normales (llamado por nombre) y la reducción de orden de solicitud (llamada por valor).Sigo obteniendo diferentes respuestas para ambas.Esta es la expresión de lambda que debe reducirse utilizando ambas técnicas:

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

Answer 1

Sigo obteniendo diferentes respuestas para ambos.

Debe obtener el mismo resultado para ambos pedidos. Muestre su trabajo para que la comunidad pueda ayudarlo a encontrar su error.

Mi conjetura es que ha sustituido erróneamente $ f $ en lugar de $ x $ hacia el final, Cuando $ f $ es de hecho libre.

El procedimiento de reducción correcto se muestra a continuación.

---

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

No hay diferencia entre el orden normal y el orden aplicativo en el primer paso.

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

---

En este paso hay una diferencia, debido a que se está aplicando el valor, $ ((\ lambda f \ x \ ldotp f \ (f \ x)) \ f) $ no está en la forma normal beta. Vamos a ignorarlo y usar el orden normal primero.

Orden normal

$ ((\ 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)) \ f) \ x)) $ < / p>

$ F \ (F \ (F \ (F \ X)) $

---

Volvamos al primer paso.

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

---

Esta vez usemos el orden aplicativo

Orden aplicativa

$ (\ 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)) $

---

Con orden normal, redujimos la expresión a:

$ F \ (F \ (F \ (F \ X)) $

con orden aplicativo reducimos la expresión a:

$ F \ (F \ (F \ (F \ X)) $

Los resultados son los mismos.