Exercise 2: Untyped Lambda Calculus

Hand in: October 20 (in 2 weeks).

In this exercise, we reuse the combinator parsing library introduced in exercise 1.

The provided framework is self-contained and can be downloaded as src.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 beta-reduction 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

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. 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. To rename a bound variable in a lambda abstraction λx.t1, one chooses a fresh name x1 for bound variable x, and consistently renames all free occurences of x in the body t1.

We use the following rules to test if a variable is free in some term:

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:

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/fos/:

  1. Complete the parser productions with the start symbol Term; you also need to define some delimiters and subclasses of class Term.
  2. Implement a reducer that uses the normal--order strategy, which applies alpha-conversion 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 = //..
  3. 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, these are self-check 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 end-of-file is encountered, which represents the input program. If the program is syntactically correct, it should print each step of the small-step 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 as-is.

Hints