Ayudar a entender la beta de reducción de ejemplo

Question

Actualmente estoy leyendo un libro de texto en sistemas de computación distribuida que incluye una breve introducción a $\lambda$-cálculo. Hay un ejemplo de la evaluación de la secuencia de $(((if \space \space true) \space \space 4) \space \space 5)$ que está escrito a continuación.

1. $\space\space(((\lambda b.\lambda t.\lambda e.((b \space t) \space e) \space \lambda x.\lambda y.x) \space 4) \space 5)$

2. $\space\space((\lambda t.\lambda e ((\lambda x.\lambda y.x \space \space t) \space e) \space 4) \space 5)$

3. $\space\space(\lambda e ((\lambda x.\lambda y.x \space \space 4) \space \space e) \space \space 5)$

4. $\space\space((\lambda x.\lambda y.x \space \space 4) \space \space 5)$

5. $\space\space(\lambda y.4 \space \space 5)$

6. $\space\space 4$

El autor ha utilizado $\beta$de reducción en cada línea y puedo seguir hasta la segunda a la última reducción. Podría alguien explicar cómo los obtenemos a partir de la línea 4 a la línea 6?

Answer 1

Cuando se va de la línea 4 a la línea 5, se sustituye $x=4$ a $\lambda y. x$, debido a que el interior argumento está vinculado a la $\lambda x$. El 5 se pasa a continuación el resultado y vinculadas a la $\lambda y$, por lo que sustituimos $y=5$ a $\lambda y. 4$. Desde $y$ no aparece libre en $4$, esto no altera la expresión, así que terminamos con $4$.

Answer 2

En la línea 4. hay un $\beta$-redex $(\lambda x \lambda y. x \ 4)$, donde $\lambda x \lambda y. x$ se aplica a $4$. Esto significa que $(\lambda x \lambda y. x \ 4)$ reescribe$-$a través de una $\beta$paso$-$a $(\lambda y. x)\{4 / x\}$ (que es $(\lambda y. x)$ donde la libre aparición de $x$ es reemplazado por $4$), es decir, $\lambda y. 4$.

Desde la $\beta$-redex $(\lambda x \lambda y. x \ 4)$ está dentro de un contexto (es decir, es un sub-término de un mayor plazo), a continuación de la línea 4., si ponemos el sub-plazo $(\lambda x \lambda y. x \ 4)$ en su contexto, tenemos: $$\begin{align} ((\lambda x \lambda y. x \ 4) \ 5) &\to_\beta (\lambda y. x \ 5)\{4 / x\} = (\lambda y. 4 \ 5) \\ &\to_\beta 4\ \{5/y\} = 5 \end{align}$$ donde, de nuevo, $(\lambda y. 4 \ 5)$ es $\beta$-redex y, a continuación, vuelve a escribir$-$a través de una $\beta$paso$-$a $4\ \{5/y\}$ (que es $4$ donde las apariciones libres de $y$ son reemplazados por $5$), es decir, $4$ porque no hay apariciones libres de $y$ en $4$.