McMaster University — Fall 2009
Assignment 1
Untyped λ-Calculus
- Provide a datatype for representing terms of the Untyped
λ-calculus
- Implement functions at least for the following tasks:
- constructing Church numerals
- Church numeral arithmetic and other combinators
- given a λ-term, return its free variables
- given a λ-term and a variable name
x,
return the variable names in scope
at free occurrences of x.
(These are the names of variables that would be captured by
naïively substituting for x.
- replacing free occurrences of a variable with another variable
- substitution
- β-reduction of top-level redexes
- η-reduction of top-level redexes
- reduction of the leftmost-outermost β-redex
- reduction of the leftmost-innermost β-redex
- performing sequences of reductions in both strategies.
Simply Typed λ-Calculus
- Provide a datatype for representing types of a simply
typed λ-calculus
- Provide a datatype for representing terms of a explicitly
typed variant of the simply typed λ-calculus,
i.e., where abstraction has the shape
``&lambda var : type . term''.
- Write a type checking function that,
given a context (of type assignments to variables)
and a term, determines whether
that term has any type errors, and if not, returns its type.
- Implement β-reduction and normalisation