Lambda Calculus Reduction / evaluating expressions

1
votes

I was reading these notes on lambda calculus, and I am having some trouble reducing / evaluating one of the expressions at the start.

In particular the function (λf.λx.f(f(x)))(λy.y^2)(5).

How exactly do I begin this? He says the answer comes out to be 625. My mathematical intuition says that we proceed like so: (λf.λx.f(f(x)))(5^2) and he said previously that f(x) is the map

x |-> x^2

so f(f(x)) is the composition which would be f o f = (f)^2 = x^4

So further reducing our lambda expression we get

(λf.λx.x^4))(5^2)

But then we would plug 25 into x^4 which gives us 25*25*25*25 = 390,625.

(λf.(390,625))

then when we get here, I have absolutely no idea what this expression represents?

What part of the Lambda Calculus have I misunderstood? Is the way I am reducing expressions correct?

2
lambdalambda-calculus

2 Answers

1
votes

I don't know anything about lambda calculus, so feel free to downvote me into oblivion if I'm wrong :) Plus my terminology will be off, so hopefully someone experienced will answer the question. This should probably be posted to math.stackexchange.com anyways.

The

enter image description here

was given earlier as an example and was not meant to carry over to subsequent problems.

First of all, it looks as if you didn't copy the expression correctly. According to the PDF, it is:

enter image description here

Now the order of operations matters (brackets first!).

We start with:

enter image description here

We are providing the lambda term on the left enter image description here with the argument enter image description here. This means that f is replaced by the squared function.

So now we have:

enter image description here

Edit:

The reason why enter image description here is given as an argument to enter image description here is that we could write the whole expression as:

enter image description here

If we look at the first part, it's easier to see that enter image description here applies to the first argument:

enter image description here

1
votes

Correct normal-order (leftmost first) beta-reduction to normal form:

   (λ f. (λ x. f (f x))) (λ y. y ^ 2) 5
=  (λ x. (λ y. y ^ 2) ((λ y. y ^ 2) x)) 5
=  (λ x. ((λ y. y ^ 2) x) ^ 2) 5
=  (λ x. (x ^ 2) ^ 2) 5
=  (5 ^ 2) ^ 2
=  25 ^ 2
=  625

Numerical primitives like 2, 5, and ^, though encodable, are not part of the grammar. Intuitive conventional algebraic reduction rules like exponent multiplication don't apply; only beta- and possibly eta-reduction.