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

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

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s