Last week I got a question that asks me to show that the following statement about Y combinator (http://en.wikipedia.org/wiki/Fixed_point_combinator#Y_combinator) in LaTeX is correct:

Y z \leftrightarrow^{*}_{\beta} z (Y z)

where \leftrightarrow{\beta} = \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

IOW:

Y z \leftrightarrow_{\beta} r1 \leftrightarrow_{\beta} r2 \leftrightarrow_{\beta} z (Y z)

because of the following reason:

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