$\lambda$-Calculus Evaluator

This homework assignment aims to implement an evaluator of $\lambda$-expressions in Haskell, reducing a given $\lambda$-expression into its normal form following the normal order evaluation strategy. As a side effect, this homework assignment will also help you consolidate your knowledge of $\lambda$-calculus. The $\lambda$-expressions will be represented as instances of a suitably defined Haskell data type. So you will practice how to work with such types, in particular how to make it an instance of the Show class and how to use pattern matching with them.

The interpreter should be implemented as a Haskell module called Hw3. Note the capital H. The module names in Haskell have to start with capital letters. As the file containing the module code must be of the same name as the module name, all your code is required to be in a single file called Hw3.hs. Your file Hw3.hs has to start with the following lines:

module Hw3 where

type Symbol = String
data Expr = Var Symbol
          | App Expr Expr
          | Lambda Symbol Expr deriving Eq

The first line defines a module of the name Hw3. The names of variables in $\lambda$-terms are represented by instances of String. The second line just introduces a new name Symbol for the type String to distinguish visually when we deal with the variable names. The last line defines the data type representing $\lambda$-expressions. There are three data constructors: one for a variable, one for an application and one for $\lambda$-abstraction. The clause deriving Eq makes the data type instance of the Eq class so that it is possible to check whether two $\lambda$-expressions are equal or not.

Evaluator specification

First, make the data type Expr an instance of the Show class so that ghci can display $\lambda$-expressions. So you need to define the show function converting $\lambda$-expressions into a string. Once you type into the ghci prompt the following expressions, it should behave as follows:

λ> Var "x"
x

λ> App (Var "x") (Var "y")
(x y)

λ> Lambda "x" (Var "x")
(\x.x)

λ> App (Lambda "x" (Var "x")) (Var "y")
((\x.x) y)

λ> Lambda "s" (Lambda "z" (App (Var "s") (App (Var "s") (Var "z"))))
(\s.(\z.(s (s z))))

So the symbol $\lambda$ is displayed as \. Variables are displayed as their names. Applications are displayed as (e1 e2) with a space separating expressions e1,e2 and $\lambda$-abstractions as (\x.e).

As a next step, your task is to implement a function eval :: Expr -> Expr. This function for a given input $\lambda$-expression returns its normal form if it exists. Moreover, it has to follow the normal order evaluation strategy. So to make a single step $\beta$-reduction, you have to identify the leftmost outermost redex and reduce it. Then you repeat this process until there is no redex.

To reduce a redex, you have to implement the substitution mechanism allowing you to substitute a $\lambda$-expression for all the free occurrences of a variable in another $\lambda$-expression. This mechanism has to deal with name conflicts, as you know from the lecture on $\lambda$-calculus. One possibility how to safely do that is the following recursive definition:

$$\begin{array}{rl}x[x:=e]& =e\\ y[x:=e]& =y\text{if }y\ne x\\ (e_1{e}_2)[x:=e]& =(e_1[x:=e]e_2[x:=e])\\ (\lambda x.e^{\prime })[x:=e]& =(\lambda x.e^{\prime })\\ (\lambda y.e^{\prime })[x:=e]& =(\lambda y.e^{\prime }[x:=e])\text{if }y\ne x\text{ and }y\text{ is not free in }e\\ (\lambda y.e^{\prime })[x:=e]& =(\lambda z.e^{\prime }[y:=z][x:=e])\text{if }y\ne x\text{ and }y\text{ is free in }e\text{; }z\text{ is a fresh variable}\end{array}$$

The last case deals with the name conflicts, i.e., it uses $\alpha$-conversion. As $y$ is free in $e$ in this case, it could become bound after the substitution in $e^{\prime }$. Thus we rename $y$ in $\lambda y.e^{\prime }$ to a new fresh variable $z$, i.e., we compute $e^{\prime }[y:=z]$ and then replace the variable in the $\lambda$-abstraction to $\lambda z.e^{\prime }[y:=z]$. Then we can continue and recursively substitute $e$ for $x$ in $e^{\prime }[y:=z]$. So follow the above recursive definition in your code.

Your code has to generate fresh symbols when needed. The fresh symbols can be denoted, e.g., "a0","a1","a2",.... To generate a fresh symbol, it suffices to increment the number of the last used symbol. This number is a state of your computation. As Haskell is a purely functional language, you cannot have a state and update it when necessary. Instead, you need to include the index into signatures of your functions similarly, as we did in the exercise from Lab 9 where we implemented a function indexing nodes of a binary tree.

Test cases

Below you find several public test cases. If the $\lambda$-expression is already in its normal form, the eval function just returns its input.

λ> eval (App (Var "x") (Var "y"))
(x y)
λ> eval (Lambda "x" (Var "x"))
(\x.x)

If it is reducible, it returns its normal form. For instance $(\lambda x.x)y$ is reduced to $y$:

λ> eval (App (Lambda "x" (Var "x")) (Var "y"))
y

Consider the expression $(\lambda x.(\lambda y.(xy))y$. The reduction gives $(\lambda y.(xy))[x:=y]$. By the definition of substitution, we have to rename $y$ to $a0$ and then substitute $y$ for the free occurrences of $x$, i.e.,

$$\begin{array}{rl}(\lambda y.(xy))[x:=y]& =(\lambda a0.(xy)[y:=a0][x:=y])\\ & =(\lambda a0.(xa0)[x:=y])\\ & =(\lambda a0.(ya0))\end{array}$$

λ> eval (App (Lambda "x" (Lambda "y" (App (Var "x") (Var "y")))) (Var "y"))
(\a0.(y a0))

Consider the $\lambda$-expression $(\lambda x.(\lambda y.y))y$. The reduction leads to $(\lambda y.y)[x:=y]$. As $y$ is free, we introduce by the definition a fresh variable $a0$ instead of $y$ obtaining $\lambda a0.y[y:=a0]=\lambda a0.a0$. Then we compute $\lambda a0.a0[x:=y]=\lambda a0.a0$.

λ> eval (App (Lambda "x" (Lambda "y" (Var "y"))) (Var "y"))
(\a0.a0)

Consider the $\lambda$-expression $(\lambda x.(\lambda y.(\lambda z.((xy)z))))(yz)$. As $y$ and $z$ are free in $(yz)$ we have to rename them in $\lambda x.(\lambda y.(\lambda z.((xy)z)))$ obtaining $\lambda a0.(\lambda a1.(((yz)a0)a1))$.

ex = App (Lambda "x"
           (Lambda "y"
             (Lambda "z" (App (App (Var "x") (Var "y")) (Var "z")))))
         (App (Var "y") (Var "z"))

λ> eval ex
(\a0.(\a1.(((y z) a0) a1)))

To write more complex test cases, you can define subexpressions and then compose more complex ones. For instance, to test that $S1$ reduces to $2$:

one = Lambda "s" (Lambda "z" (App (Var "s") (Var "z")))
suc = Lambda "w"
       (Lambda "y"
         (Lambda "x"
           (App (Var "y")
                (App (App (Var "w") (Var "y"))
                     (Var "x")))))

λ> eval (App suc one)
(\y.(\x.(y (y x))))

One more test case using the definition $one=\lambda s.(\lambda z.(sz))$. Consider the $\lambda$-expression

$$(\lambda z.one)(sz)=(\lambda z.(\lambda s.(\lambda z.(sz))))(sz).$$

It reduces to $\lambda a0.(\lambda z.(a0z))$. As $s$ is free in $(sz)$, the bound occurrence of $s$ in $one$ is renamed. But $z$ is not renamed because by the defition of substitution we have $\lambda z.(a0z)[z:=(sz)]=\lambda z.(a0z)$.

λ> eval (App (Lambda "z" one) (App (Var "s") (Var "z")))
(\a0.(\z.(a0 z)))