Theory of Types and Programming Languages

Staff

Documents

Assignments

Project 1 - The NB Language

Project 2 - Untyped Lambda Calculus

Project 3 - Simply Typed Lambda Calculus

Project 4 - STLC Extensions

Project 5 - STLC with Type Reconstruction

Project 2: Untyped Lambda Calculus

Hand in: 18 Mar 2022, 23:59 (Hongkong)

Project template: 2-untyped.zip

In this exercise, you’ll be studying untyped λ-calculus. This classic language is defined in Chapter 5 of the TAPL book.

t ::= ident              terms
    | "\" ident "." t
    | t t
    | "(" t ")"

v ::= "\" ident "." t    values

We use standard syntax to express λ-terms, with lambdas replaced by backslashes. As a reminder, note that 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)) (see TAPL, p54).

Evaluation rules

The evaluation rules for full beta-reduction are 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 (see TAPL, p71):

Input Output Condition
[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 occurrences of x in the body t1. Note: you will need to define a function that “freshens” variable names. You can rely on variable names in the input term containing only characters, never any numbers.

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

Input Output
FV(x) {x}
FV(λx. t1) FV(t1) \ {x}
FV(t1 t2) FV(t1) ∪ FV(t2)

Evaluation strategies

TAPL p56 presents several evaluation strategies for the λ-calculus:

What you have to do

  1. Implement the reduceNormalOrder method that uses the normal-order strategy, which applies alpha-conversion and term substitution following the above reduction rules. If none of the rules apply it should throw a NoReductionPossible exception containing the corresponding irreducible term.

  2. Implement the reduceCallByValue method that 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. Again, if none of the rules apply it should throw NoReductionPossible exception containing the corresponding irreducible term.

    Since we reason about values, we need to define what a value is. We will follow the book in saying that the only values are lambda abstractions. Does it simplify the substitution operation? What would happen if we added 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.

Development & debugging

We provide a simple parser and runner for your application which let you quickly debug your current implementation. When you implement reduceNormalOrder and reduceCallByValue, it should produce results like:

input:

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

output:

normal order:
Abs(y,App(Abs(x,Var(x)),Var(y)))
Abs(y,Var(y))
call-by-value:
Abs(y,App(Abs(x,Var(x)),Var(y)))