Exercise 2: Untyped Lambda Calculus
Hand in: November 22 (in 2 weeks). NEW The assignement has been augmented with a call-by-value reducer. See below.
In this exercise, we reuse the combinator parsing library introduced in exercise 1.
The provided framework is self-contained and can be downloaded as zip or tar.gz archive.
The API documentation for this exercise is available online.
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 are defined as follows:
t1 → t1' t1 t2 → t1' t2
t2 → t2' t1 t2 → t1 t2'
t1 → t1' λx. t1 → λx. t1'
(λx. t1) t2 → [x ↦ t2] t1
We reproduce here the substitution rules presented on page 71 of the TAPL book:
[x → s]x = s [x → s]y = y if y ≠ x [x → s](λy. t1) = λy . t1 if y = x λy . [x → s]t1 if y ≠ x and y ∉ FV(s) (*) [x → s](t1 t2) = ([x → s]t1 [x → s]t2)
The part marked with an (*) doesn't handle the case where y ∈ FV(s). So what shall we do then ?! We first use of alpha-conversion for consistently renaming a bound variable in a term - actually a lambda abstraction - and then continue to apply the substitution rules.
The renaming of a bound variable occurs by traversing a term and
generating fresh names (eg. based on the rule 'x'
becomes
'x1'
, and so on) for free variables; we use the following
rules to test if a variable is member of the FV set:
FV(x) = {x} FV(λx.t1) = FV(t1) \ {x} FV(t1 t2) = FV(t1) ∪ FV(t2)
Evaluation strategy
Pages 56ff of the TAPL book present several evaluation strategies for the λ-calculus:
-
Under full beta-reduction any redex may be reduced at any time. This is the strategy described by the evaluation rules listed above.
- Under normal order strategy, the leftmost, outermost redex is always reduced first.
-
The call-by-name strategy is yet more restrictvive, allowing no reductions inside abstractions.
Haskell uses an optimized version known as call-by-need that, instead of re-evaluating 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 re-evaluation.
-
Most languages use a call-by-value strategy, in which only outermost redexes are reduced and where a redex is reduced only when its right-hand side has already been reduced to a value.
The call-by-value 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 call-by-name and call-by-need evaluate only the arguments that are actually used.
REMINDER: Except for the full beta-reduction 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/tapl2/
:
-
Complete the parser productions with the start symbol
Term
; you also need to define some delimiters and subclasses of classTerm
. -
Implement the method
build
for representing terms as ASTs. -
Implement a simple reducer which applies alpha-conversion and term substitution following the above reduction rules (full beta reduction).
def alpha(t: Term): Term = //.. def subst(t: Term, x: String, s: Term): Term = //.. def reduce(t: Term): Term = //..
-
NEW Implement another reducer which uses the call-by-value 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, just answer with one or two phrases!) ? Compare the output of the two reducers, and try to understand why is it different.
def reduceWithCallByValue(t: Term): Term = //..
NEW 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
reduce
or reduceWithCallByValue
.
def path(t: Term, reduce: Term => Term): Stream[Term] = //..
Hints
-
Don't forget to override the method
toString()
in the subclasses of classTerm
in order to get a clean output! -
To get nice error messages you may modify the method
parse
as follows:def parse(in: String): Option[Output] = { val res = run(Term, in) res match { case Success(_, _) => output(res) case Failure(_, _) => Console.println(res); None } }
-
NEW
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