Exercises for the third tutorial

1. Explain what can go wrong if we substitute an open expression for every free occurrence of some variable in a term, using the definition of substitution given for χ.

   Hint: Consider substituting x for the free occurrences of y in λx.y.

2. [BN] Explain the standard representation of booleans in χ. How are true and false represented?

3. [BN] Implement if-then-else as a χ function that takes three arguments.

4. [BN] Implement a χ program that does not terminate.

5. [BN] Explain the standard representation of natural numbers in χ.

6. Implement a function (in, say, Agda or Haskell) that converts a natural number into its standard representation in χ. The function could have the following type, where Exp is the (Agda or Haskell) representation of the inductively defined set defining the abstract syntax of χ:

     Natural -> Exp

   (You can use the type Exp provided by the BNFC specification of χ that comes with the third assignment.)

7. Implement a function (in, say, Agda or Haskell) that tries to convert a χ value representing a natural number into a natural number. The function could have the following type:

     Exp -> Maybe Natural

8. Implement a function (in, say, Agda or Haskell) that converts a list of natural numbers into its standard representation in χ. The function could have the following type:

     [Natural] -> Exp

9. Implement the append function for lists, represented in the standard way, in χ.

10. Explain what the following χ program does:

      rec foo = λxs. case xs of
        { Nil()       -> Nil()
        ; Cons(x, xs) -> append (foo xs) Cons(x, Nil())
        }
      [ append ← the full code of the append function ]

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