Lambda Calculus

Lambda Calculus is the simplest general purpose programming language. It is composed of

general function abstractions known as lambda abstractions, variables, and function applica-

tions. A lambda term may look as follows: (x:x) y. Computation is done with what is known

as -reduction. In this case the y variable gets substituted in for x in the term inside of the

parentheses wherever it occurs, in this case the one place, so we get the following (x:x) y y.

If x occured multiple times in the lambda abstraction inside of the parenthesis we would get

something di erent. For example (x:x x) y y y. To illuminate what is going on with this

-reduction let us take a look at what is known as the parse trees for these expressions. We will

use for lambda abstractions, A for applications, and the variables characters for the variables.

(x:x x) y

A

L y

A

x x

x

The reduction takes the y variable on the right part of top application (A), and substitutes

it in for the variable x on wherever it occurs in the sub tree to the right of the L, so it would

then output the following tree:

A

y y

1

2 Assignment

For this assignment, I want you to take in two lambda expressions from command line using

the following syntax:

! n

(space applications) ! @

variables ! characters from [a-z]

parens ! parens

So for some examples:

x:x x ! nx . x @ x

(x:x x) y ! (nx . x @ x) @ y

(x:(y:y))z ! (nx . (ny . y)) @ z

It will then parse them into trees as seen on the rst page.

If the rst lambda expression given has a L, I want you to peform a reduction as if the second

term is being applied to it, it will then output the lambda expressionto the command line:

Input:

\x . x @ x

y

Output:

y @ y

Input:

(\x . x @ (\y . y))

\z . z

Output:

(\z . z) @ (\y . y)

2