# Lambda Calculus simplification

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem.

$$(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)(\lambda sz.sz)$$

I am lost with this.

if anyone could lead me in the right direction that would be much appreciated

Lambda terms are simplified by the β-reduction rule: $$(\lambda x.M)N\,\rightarrow_\beta\,M[x:=N]$$

It means, if you have a subterm that looks like $(\lambda x.M)N$ (called redex) you can replace it by $M[x:=N]$, which is $M$ with $N$ substituted for $x$. The replacement $M[x:=N]$ is often called contractum. (Capital letters likes $M$ and $N$ are used to denote terms.)

In your case, the first reduction would be:

$$(\underbrace{(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)}_{\mbox{redex}})(\lambda sz.sz) \rightarrow_\beta \underbrace{(\lambda n.(\lambda sz.(\lambda sz.sz)s(nsz)))}_{\mbox{contractum}}(\lambda sz.sz)$$ where we replaced $m$ with $\lambda sz.sz$. Note that we now have $\lambda sz$ inside $\lambda sz$ which isn't very convenient (yet allowed). It is better to rename bound variables ($\alpha$-conversion) to be distinct, for example to:

$$(\lambda n.(\lambda uv.(\lambda sz.sz)u(nuv)))(\lambda sz.sz)$$

Some notes:

• Substitution applies only to free variables. Bound variables stay always intact.
• Sometimes substitution is not directly possible. For example, you cannot substitute $x:=y$ into $\lambda y.xy$ because $y$ is bound under $\lambda$. You'd get $\lambda y.yy$ which would change the meaning of the term. So first, you have to rename the bound variable first, for example to $\lambda z.xz$ and then you can safely substitute $x:=y$ to get $\lambda z.yz$. The Wikipedia article gives formal definition of substitution and shows when it's necessary to rename bound variables.
• Lambda associates to the right, so $\lambda sz.sz$ is $\lambda s.(\lambda z.sz)$.
• Application associates to the left, so $xyz$ is $(xy)z$.

An alternative way of expressing a lambda abstraction and reduction. Indexes are used instead of lettered terms based on the order of input. Abstractions are surrounded by []'s

(λmn.(λsz.ms(nsz)))(λsz.sz)(λsz.sz)
m -> 1, n -> 2, s -> 3, z -> 4
(λmn.(λsz.ms(nsz))) = [1 3 (2 3 4)]
(λsz.sz) = [1 2]
[1 3 (2 3 4)][1 2][1 2]
[[1 2] 2 (1 2 3)][1 2]   ;1 was replaced with [1 2], remaining terms decremented
[[1 2] 1 ([1 2] 1 2)]    ;1 was replaced with [1 2], remaining terms decremented
[1 ([1 2] 1 2)]          ;1 2 was replaced by 1 ([1 2] 1 2)]
[1 (1 2)]                ;1 2 was replaced by 1 2
(λmn.m(mn))


The notation above is just a more compact and unambiguous way of expressing lambda abstractions. Compound abstractions reduce to a single normal form automatically, alpha reduction is not needed.

Single positive indexes are used for bound terms. Negative indexes are used for kill terms. Negative indexes are placed last in order of decreasing magnitude.

I = λx.x = 
K = λxy.x = [1 -2]
KI = λyx.x = [2 -1]
S = λxyz.xz(yz) = [1 3 (2 3)]


Applying S to K:

[1 3 (2 3)][1 -2]
[[1 -2] 2 (1 2)]  ;1 was replaced with [1 -2], remaining terms decremented
[[.2 -1] (1 2)]   ;reducing: 1 replaced by .2*, -2 decremented (in magnitude)
[2 -2 -1]         ;(1 2) bound terms become kill terms due to -1.
[2 -1] = KI       ;-2 kill term is void due to surviving 2 term

* the . notation signifies the bound term is from the outer abstraction
and must be used to prevent decrementing and double replacement of the
term until the substitution of all terms in the abstraction is complete.

[2 -1][anything] ;applying KI to anything
 = I          ;yeilds I, therefor SK[anything] =  = I


Applying K to K:

[1 -2][1 -2]
[[1 -2] -1]  ;kill terms are absorbed and also increase the magnitude of bound terms
[2 -3 -1]    ;applying this result to anything yields K.
[2 -3 -1][anything]
[2 -1]

• Please add a bit of commentary/motivation. Jan 24 '13 at 9:53
• Your answer lacks any description and thus looks like some sort of Soduko puzzle. What is your representation? What are the reduction rules? Jan 24 '13 at 18:02
• Then do it in the answer; you can edit by clickin on, well, "edit".
– Raphael
Jan 25 '13 at 11:31
• Here is a web based version of an interpreter console for this notation. It does not show the reduction steps but does evaluate correctly for everything that I have been able to throw at it. I am interested in getting feedback on it. Mar 21 '13 at 21:22