Assignment 3

In order to pass this assignment you have to get at least three points.

This time you can make use of a BNFC specification of a variant¹ of the concrete syntax of χ. Use bnfc --haskell Chi.cf followed by alex LexChi.x and happy ParChi.y to generate Haskell code from the BNFC specification. There is also a Haskell wrapper module that exports the generated abstract syntax and some definitions that may be useful for testing your code (documentation). If you use the wrapper module, make sure that you have a sufficiently recent version of GHC.² (Do not submit the wrapper module or the generated code.)

1. (1p) Explain what the following χ program does:

     rec foo = λm. λn. case m of
       { Zero() -> case n of
         { Zero()  -> True()
         ; Succ(n) -> False()
         }
       ; Succ(m) -> case n of
         { Zero()  -> False()
         ; Succ(n) -> foo m n
         }
       }

2. (2p) [BN] Implement substitution for χ. The function should take three arguments, a variable, a closed term, and another term, and substitute the first term for every free occurrence of the variable in the second term.

   If you use the BNFC specification above and Haskell, then the substitution function should have the following type:

     Variable -> Exp -> Exp -> Exp

   Test your implementation. Here are some test cases that must work:

   Variable	Substituted term	Term	Result
   x	Z()	rec x = x	rec x = x
   y	λx.x	λx.(x y)	λx.(x (λx.x))
   z	C(λz.z)	case z of { C(z) -> z }	case C(λz.z) of { C(z) -> z }

3. (1p) Implement multiplication of natural numbers in χ, using the representation of natural numbers given in the χ specification.

   Hint: If you want to make use of addition in the implementation of multiplication, then you can define multiplication using a free variable add, and use the substitution operation from the previous exercise to substitute a complete (closed) implementation of addition for this variable.

4. (2p) [BN] Implement an interpreter for χ. The interpreter should be a partial function from closed terms to values, and should implement the operational semantics of χ.

   If you use the BNFC specification above and Haskell, then the interpreter should have the following type:

     Exp -> Exp

   Test your implementation, for instance by testing that addition (defined in the wrapper module) works for some inputs. If addition doesn't work when we test your code, then your solution will not be accepted.

   (Implementing a call-by-value semantics properly in a language like Haskell, which is by default non-strict, can be tricky. However, you will not fail if the only problem with your implementation is that some programs that should fail to terminate instead terminate with a "reasonable" result.)

Please provide your source code in a form which is easy to test, not, say, a PDF file.

(Exercises marked with [BN] are based on exercises from a previous version of this course, given by Bengt Nordström.)