Question

Lambda calculus normalization

Answer 1

I'm trying to understand how this should be normalized:
(λx. λy. x y y) (λx. λy. x + y) 5

Where I'm getting stuck is the "x y y" part. Are both of the y's bound? Is one unbound?

Answer 2

Great Scott, more satanic math.
Have this.
5 y^2 (x λ) . (y λ) . x (y + (x λ) . (y λ) . x)

Answer 3

What is that?

Answer 4

That is the result.

Answer 5

That's not any kind of format that makes sense to me. In lambda calculus, you can't have λ without a variable after it.

Answer 6

I'm getting this but I'm not sure if it's right:
(λ x. λ y. x y y) (λ x. λ y. x + y) 5 --> (λ x. λ y. x y y) (λ y. 5 + y) -->
(λ x. λ z. x z z) (λ y. 5 + y) --> (λ z. (λ y. 5 + y) z z) --> (λ z. 5 + z z)