Exercise 2: Untyped Lambda Calculus
Hand in: October 18 (in 2 weeks).
In this exercise, we reuse the combinator parsing library introduced in exercise 1.
The provided framework is selfcontained and can be downloaded as zip.
Assignment
The goal of this exercise is to familiarize yourself with the λcalculus; your work consists of implementing a parser and a reducer for untyped λterms.
We use the following syntax to express λterms:
t ::= x variable  "\" x "." t abstraction  t t application (left associative)  "(" t ")"
REMINDER The bodies of abstractions are taken to extend
as far to the right as possible, so that, for example,
λx. λy. x y x
stands for the same tree as
λx. (λy. ((x y) x))
(cf. TAPL, p.54).
The evaluation rules for full betareduction are defined as follows:
t_{1} → t_{1}' t_{1} t_{2} → t_{1}' t_{2}
t_{2} → t_{2}' t_{1} t_{2} → t_{1} t_{2}'
t_{1} → t_{1}' λx. t_{1} → λx. t_{1}'
(λx. t_{1}) t_{2} → [x ↦ t_{2}] t_{1}
The last rule uses substitution, whose definition we reproduce here (presented on page 71 of the TAPL book):
[x → s]x = s [x → s]y = y if y ≠ x [x → s](λy. t_{1}) = λy . t_{1} if y = x λy . [x → s]t_{1} if y ≠ x and y ∉ FV(s) (*) [x → s](t_{1} t_{2}) = ([x → s]t_{1} [x → s]t_{2})
The part marked with an (*)
doesn't handle the case where y ∈ FV(s).
So what shall we do then ? We first use of alphaconversion
for consistently renaming a bound variable in a term  actually a
lambda abstraction  and then continue to apply the substitution rules.
To rename a bound variable in a lambda abstraction
λx.t_{1}
, one chooses a fresh name
x_{1}
for bound variable x
, and
consistently renames all free occurences of x
in
the body t_{1}
.
We use the following rules to test if a variable is free in some term:
FV(x) = {x} FV(λx.t_{1}) = FV(t_{1}) \ {x} FV(t_{1} t_{2}) = FV(t_{1}) ∪ FV(t_{2})
Evaluation strategy
Pages 56ff of the TAPL book present several evaluation strategies for the λcalculus:

Under full betareduction any redex may be reduced at any time. This is the strategy described by the evaluation rules listed above, but this is too unrestricted in practice: we need a deterministic way to choose a certain redex, when more than one is available.
 Under normal order strategy, the leftmost, outermost redex is always reduced first. This strategy allows to reduce inside unapplied lambda terms.

The callbyname strategy is yet more restrictive, allowing no reductions inside lambda abstractions. Arguments are not reduced before being substituted in the body of lambda terms when applied.
Haskell uses an optimized version known as callbyneed that, instead of reevaluating an argument each time it is used, overwrites all occurrences of the argument with its value the first time it is evaluated, avoiding the need for subsequent reevaluation.

Most languages use a callbyvalue strategy, in which only outermost redexes are reduced and where a redex is reduced only when its righthand side has already been reduced to a value (a function).
The callbyvalue strategy is strict, in the sense that the arguments to functions are always evaluated, whether or not they are used by the body of the function. In contrast, lazy strategies such a callbyname and callbyneed evaluate only the arguments that are actually used.
REMINDER: Except for the full betareduction strategy the
evaluation relation is a partial function: each term t evaluates in one step
to at most one term t'
.
Implementation
The following steps should help you to complete the two
source files located in directory src/fos/
:

Complete the parser productions with the start symbol
Term
; you also need to define some delimiters and subclasses of classTerm
. 
Implement a reducer that uses the normalorder strategy, which applies alphaconversion and term substitution following the above reduction rules.
def alpha(t: Term): Term = //.. def subst(t: Term, x: String, s: Term): Term = //.. def reduceNormalOrder(t: Term): Term = //..

Implement another reducer which uses the callbyvalue evaluation strategy. For that you need to define a new set of evaluation rules, similar to the ones given above. Since we speak about values, we need to define what a value is. We can follow the book in saying that the only values are lambda abstractions. Does it simplify the substitution operation? What would happen if we add variables to the set of values (do not implement, these are selfcheck questions) ? Compare the output of the two reducers, and try to understand why it is different.
def reduceWithCallByValue(t: Term): Term = //..
The method path
invoked
in the main function returns a stream of terms representing the big
reduction step which consists of all single steps computed by
reduceNormalOrder
or reduceWithCallByValue
.
def path(t: Term, reduce: Term => Term): Stream[Term] = //..
Input/Output
Your program should read a string from standard input until endoffile is encountered, which represents the input program. If the program is syntactically correct, it should print each step of the smallstep reduction, starting with the input term, until it gets stuck. It should do so using both reduction strategies. The provided framework already implements this behavior. You should use it asis.
Hints
 As in the previous exercise, the project is supplied with a
build.xml
file for ant, sources for the combinator parsing library, and a starting point for your project. You can use"ant docs.combinator1"
to build the HTML documentation of the combinator parsing library. 
Don't forget to override the method
toString()
in the subclasses of classTerm
in order to get a clean output! 
Streams
are a form of lazy lists, and they are a perfect match for evaluations
that may not terminate. Since the tail of a stream is not
evaluated unless needed, you can construct a sequence of terms
almost as with a list:
 if the term can be reduced further to
t1
, you useStream.cons(t1, path(t1))
to construct a new element,  otherwise you return an empty stream, using
Stream.empty
 if the term can be reduced further to