HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Lambda Calculus beta reduction

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
betareductionlambdacalculus

Problem

I am trying to learn Lambda calculus from here

and while trying to solve some problems, I got stuck. I was trying to solve the following problem (page 14, excercise 2.6 part (i):

Simplify $M \equiv (\lambda xyz.zyx) aa (\lambda pq. q)$.

My evaluation using the beta rule reduces it to $(\lambda z. z)$ as follows:
First I replace occurences of $x$ in $M$ by $aa (\lambda pq. q)$, and then since there are no occurences of $y$ in the resulting $\lambda$ term, the expression simply evaluates to $(\lambda z. z)$.

Is my reasoning correct? (Since there were no solutions to these notes, I want to ensure my understanding is correct. Any corrections, will be much appreciated! Thanks in advance.

Solution

No, your reduction is wrong. The function $(\lambda x y z. z y x)$ is applied to three arguments: $a$, $a$ and $(\lambda p q. q)$. It is not, as you wrote, a the function $(\lambda x y z. z y x)$ applied to the term $a a (\lambda p q. q)$; that second term does not appear in $M$. Strictly speaking, functions in the lambda-calculus take three arguments, they are effectively curried, so if you add optional parentheses $M$ can be written
$$
(((\lambda x. (\lambda y. (\lambda z. (z y) x))) a) a) (\lambda p. (\lambda q. q))
$$
This reduces by substituting $a$ for $x$ in $(\lambda y. (\lambda z. (z y) x)))$, then $a$ for $y$ in the result of this:
$$
M \to (\lambda y z. z y a) a (\lambda p q.q) \to (\lambda z. z a a) (\lambda p q. q)
$$
then substitute $(\lambda p q. q)$ for $z$, after which a new redex appears:
$$
\ldots \to (\lambda p. (\lambda q. q)) a a \to (\lambda q. q) a \to a
$$

Context

StackExchange Computer Science Q#1434, answer score: 8

Revisions (0)

No revisions yet.