patternMinor
Lambda Calculus beta reduction
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.
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
$$
$$
(((\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.