Beta reducción de la expresión

Question

Se me presenta la siguiente donde:

TRUE = λxy.x
FALSE = λxy.y

IF = λbtf. b t f
OR = λxy. IF x TRUE y

y estoy tratando de evaluar:

OR FALSE TRUE 

el uso de Beta reducción. Desde la beta es la reducción de la izquierda asociativa, comencé desde la izquierda, pero estoy teniendo dificultades con la O, donde no contiene en SI y la VERDAD en la expresión. Así que he intentado:

OR FALSE TRUE
(λxy. IF x TRUE y) (λxy.y) (λxy.x)
(λxy. (λbtf. b t f) x (λxy.x) y) (λxy.y) (λxy.x) #i substituted btf with x here but I'm not fully sure if it's valid
(λxy. x (λxy.x) y) (λxy.y) (λxy.x)
(λxy. x x) (λxy.y) (λxy.x)
(λxy.y) (λxy.y) (λxy.x)
(y) (λxy.x)

Pero estoy bastante seguro de que he metido la pata en alguna parte a lo largo de la manera como la evaluación de la O fue bastante confuso. No estoy seguro de si me la beta reducido correctamente así que agradecería un poco de ayuda en esto.

Me dio otra oportunidad así que aquí está lo que hice:

OR FALSE TRUE
(λxy. IF x TRUE y) FALSE TRUE
IF FALSE TRUE FALSE TRUE
(λbtf. btf) FALSE TRUE FALSE TRUE
FALSE TRUE FALSE TRUE
(λxy.y) TRUE FALSE TRUE
(λx.TRUE) FALSE TRUE
TRUE TRUE
(λxy.x) TRUE
λy.TRUE

De nuevo estoy todavía no se sabe si es correcta esta forma. Un poco de ayuda necesaria.

Answer 1

De hecho, $\text{OR} \ \text{FALSE} \ \text{TRUE}$ $\beta$-se reduce a $\text{TRUE}$, como se esperaba. Nos deja ver que en un paso-por-paso $\beta$-reducción.

\begin{align} \text{OR} \ \text{FALSE} \ \text{TRUE} &= (\lambda xy. \text{IF} \ x \ \text{TRUE} \ y) \ \text{FALSE} \ \text{TRUE} \\ &\to_\beta (\lambda y. \text{IF} \ \text{FALSE} \ \text{TRUE} \ y) \ \text{TRUE} \\ &\to_\beta \text{IF} \ \text{FALSE} \ \text{TRUE} \ \text{TRUE} \\ &= (\lambda btf. \, b\,t\,f) \ \text{FALSE} \ \text{TRUE} \ \text{TRUE} \\ &\to_\beta (\lambda tf. \text{FALSE} \ t\,f) \ \text{TRUE} \ \text{TRUE} \\ &\to_\beta (\lambda f. \text{FALSE} \ \text{TRUE} \ f) \ \text{TRUE} \\ &\to_\beta \text{FALSE} \ \text{TRUE} \ \text{TRUE} \\ &= (\lambda x y. y) \ \text{TRUE} \ \text{TRUE} \\ &\to_\beta (\lambda y. y) \ \text{TRUE} \\ &\to_\beta \text{TRUE} \end{align}

Su error en la primera reducción que escribió en el paso siguiente: \begin{equation} (\lambda xy. x (\lambda xy.x) y) (\lambda xy.y) (\lambda xy.x) \to_\beta (\lambda xy. x x) (\lambda xy.y) (\lambda xy.x) \end{equation} lo cual no es correcto. De hecho, no se puede reducir la $(\lambda xy.x) y$ dentro $\lambda xy. x (\lambda xy.x) y$ porque, como usted dijo, la aplicación es de izquierda asociativa, por lo tanto $\lambda xy. x (\lambda xy.x) y = \lambda xy. (x (\lambda xy.x)) y$. El paso correcto es: \begin{align} (\lambda xy. x (\lambda xy.x) y) (\lambda xy.y) (\lambda xy.x) &\to_\beta (\lambda y. (\lambda xy.y) (\lambda xy.x) y) (\lambda xy.x) \to_\beta \dots \end{align}