## 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).