## Seeing It as a Relationship: <-> beta-reduction

Posted in kerneltrap.org on January 30, 2010 – 4:36am

Last week I got a question that asks me to show that the following statement about Y combinator in LaTeX is correct: $Y z \leftrightarrow^{*}_{\beta} z (Y z)$ where $\leftrightarrow_{\beta}$ is defined as $\rightarrow_{\beta} \bigcup \leftarrow_{\beta}$

The statement about the union originally made me thought in the following way: $Y z$ $\rightarrow_{\beta}$ $r1$ $\rightarrow_{\beta}$ $r2$ $\rightarrow_{\beta}$ $\dots$ $\rightarrow_{\beta}$ $z (Y z)$

or $Y z$ $\leftarrow_{\beta}$ $r1$ $\leftarrow_{\beta}$ $r2$ $\leftarrow_{\beta}$ $\dots$ $\leftarrow_{\beta}$ $z (Y z)$

both of which are not possible (the one showed in the Wikipedia article shows a syntactic equality not a zero or more beta reduction steps).

I erred in seeing $\leftrightarrow^{*}_{\beta}$ as two separate operations instead of a single relation with the given semantic. Once viewed as a relationship with the given semantic (i.e., $\rightarrow_{\beta} \bigcup \leftarrow_{\beta}$) that means that the relationship holds iff either the left-hand side can beta reduce to the right-hand side or the right-hand side can beta reduce to the left hand side, I can easily understand that the statement is correct as shown below:

Step 1: $(\lambda f \cdot (\lambda x \cdot f (x x)) (\lambda x \cdot f (x x))) z = Y z$ $\leftrightarrow_{\beta} (\lambda x \cdot z (x x)) (\lambda x \cdot z (x x)) = r1$ $\leftrightarrow_{\beta} z ((\lambda x \cdot z (x x)) (\lambda x \cdot z (x x))) = r2$

Step 2: $z ((\lambda f \cdot (\lambda x \cdot f (x x)) (\lambda x \cdot f (x x))) z) = z (Y z)$ $\leftrightarrow_{\beta} z ((\lambda x \cdot z (x x)) (\lambda x \cdot z (x x))) = r2$

In other words, $Y z \leftrightarrow_{\beta} r1 \leftrightarrow_{\beta} r2 \leftrightarrow_{\beta} z (Y z)$ because $Y z \leftrightarrow_{\beta} r1$ holds due the given semantic of $\leftrightarrow_{\beta}$ since Y z can beta reduce to r1 but r1 cannot beta reduce to Y z, and $r1 \leftrightarrow_{\beta} r2$ holds due to the same reason since r1 can beta reduce to r2 but r2 cannot beta reduce to r1, and $r2 \leftrightarrow_{\beta} z (Y z)$ holds due to the same reason since z (Y z) can beta reduce to r2 but r2 cannot beta reduce to z (Y z).

This entry was posted in Lambda Calculus, Learning Experience, Mathematics and tagged . Bookmark the permalink.