lambda calculus

Homework due Monday 12, 11 PM

reduce the following λexpressions. If there is a normal form find it. If not, see if you can find two different reductions.

(λx.xy)λt.tz

(λx.xy)λx.xz(λxyz.xy(yz) xyz)

We talked about a special term

Y ≡ λf.(λx.f(xx))(λx.f(xx))

This is a specialized term that creates the so called fixed points. if F is a term then X is a fixed point if FX → X or vice versa. You can loosely use equality to express this X = FX. So far we only have defined equality as an alternative for →. That is why I say loosely.

Is succ = Y succ? If so, is that okay? Should something be equal to its successor? succ is the successor function defined for integers.

How about fact = Y fact? fact is the term we defined in class. It describes the facto- rial function. In both cases all you need to do is to write the terms as described and check the reductions. That’s it.

Given I ≡ λx.x, K ≡ λxy.x, and S ≡ λxyz.xz(yz), decide if SKK → I? Either show that it does or argue it does not.

Finally, create a term that has an infinite reduction. A term I have not shown in class and please do it yourself. I do know what famous self reducing terms are out there. So spend a little time and come up with your own. Show that the reduction does not stop. A term X that has X → X is of course never going to stop reducing. But maybe you could find something like X → Y , Y → Z and Z → X for instance. Or maybe you can find something rather than the term I gave in class. That is, λx.xx λx.xx