Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Consider $(\;(\lambda f.\lambda x. f(f(f(x))))\;(\lambda g.\lambda y.g(g(y))) \;)$.

Lets take the first lambda function, now

$(\lambda f.\lambda x. f(f(f(x))))\;(\lambda x.x+1)(0) = 3 $ right?

And for the second one,

$(\lambda g.\lambda y.g(g(y)))\;(\lambda x.x+1)(0) = 2$

I verified with some code too.

If I try to evaluate

$(\;(\lambda f.\lambda x. f(f(f(x))))\;(\lambda g.\lambda y.g(g(y))) \;)\;(\lambda x.x+1)(0)$

by hand, I got answer 6. I wrote the code for it and answer is 8. I'm not able to convince myself about it. Isn't the following simplification correct?

$(\;(\lambda f.\lambda x. f(f(f(x))))\;(\lambda g.\lambda y.g(g(y))) \;) = (\;(\lambda f.\lambda x.f(f(\;\; f(f(\;\; f(f(x))))))))$

In general how does one evaluate such long lambda expressions?

share|improve this question

1 Answer 1

up vote 3 down vote accepted

You're working with Church numerals, which represent natural numbers by repeated function composition. For a Church numeral n, n succ zero gives you the number it represents, which is what your first tests verify.

The mistake you make after that is easy and subtle, especially when writing out all the lambdas in full. Writing the Church numerals as numbers for clarity, the correct answer (3 2) succ 0 gives $2^3$, but what you're doing when evaluating by hand is 3 (2 succ) 0, which gives $3 \times 2$.

In the latter case you're taking a function f, computing a function "apply f twice", then applying that function three times to get "apply (apply f twice) thrice".

In the former case, you have a function 2 which applies a function twice, and you apply 2 itself three times, so that when you then apply the result to a function f you have "apply (apply (apply f twice) twice) twice".

The actual reduction goes like this:

$(\lambda n \ f. n (n (n \ f))) (\lambda g \ x. g (g \ x))$

$(\lambda f. (\lambda g_1 \ x_1. g_1 (g_1 \ x_1)) ((\lambda g_2 \ x_2. g_2 (g_2 \ x_2)) ((\lambda g_3 \ x_3. g_3 (g_3 \ x_3)) f))) $

$(\lambda f. (\lambda g_1 \ x_1. g_1 (g_1 \ x_1)) ((\lambda g_2 \ x_2. g_2 (g_2 \ x_2)) (\lambda x_3. f (f \ x_3)) )) $

$(\lambda f. (\lambda g_1 \ x_1. g_1 (g_1 \ x_1)) ((\lambda x_2. (\lambda x_{32} . f (f \ x_{32})) ((\lambda x_{31}. f (f \ x_{31})) x_2)) )) $

$(\lambda f. (\lambda g_1 \ x_1. g_1 (g_1 \ x_1)) ((\lambda x_2. (\lambda x_{32}. f (f \ x_{32})) (f (f \ x_2)) )) ) $

$(\lambda f. (\lambda g_1 \ x_1. g_1 (g_1 \ x_1)) (\lambda x_2. (f (f (f (f \ x_2))))) ) $

$(\lambda f. (\lambda x_1. (\lambda x_{22}. (f (f (f (f \ x_{22}))))) ((\lambda x_{21}. (f (f (f (f \ x_{21}))))) x_1)) ) $

$(\lambda f. (\lambda x_1. (\lambda x_{22}. (f (f (f (f \ x_{22}))))) (f (f (f (f \ x_1)))) ) ) $

$(\lambda f. (\lambda x_1. f (f (f (f (f (f (f (f \ x_1))))))) ) ) $

Pardon the subscripts, they seemed tidier than the usual style of alpha conversion--reusing variable names makes it too easy to mix things up.

So at the end we're left with $(\lambda f \ x. f (f (f (f (f (f (f (f \ x)))))))) $ which is indeed the Church numeral 8.

In general how does one evaluate such long lambda expressions?

The biggest headache is the avalanche of parentheses, and you may notice I've used a few syntactic shortcuts (merging the "heads" of immediately nested lambdas, writing application as juxtaposition) that help somewhat. More important is that I did the reduction above in a code editor that highlights matching parentheses, which helps quite a bit.

That said, the best way to evaluate non-trivial lambda expressions is to let a computer do it for you. I've used a Scheme interpreter in the past, which works nicely. These days I'd use GHCi instead, though that only helps if you can work within a typed lambda calculus, and requires compiler-specific extensions if you want simple Church encoding to work.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.