Computeability/3/assig.org

Assignment 3

Supporting files

This time you can make use of a BNFC specification (Chi.cf) of a variant of the concrete syntax of $\chi$. This grammar gives specific rules for variable and constructor names, and differs from the concrete syntax presented in the lectures in some ways:

• Variables and constructors are sequences of letters (a to z and A to Z), digits (0 to 9), underscores (_), dashes (-) and primes ('), and variables have to start with lower-case letters or underscores, whereas constructors have to start with upper-case letters.
• Lambdas are written using backslash characters (\) and arrows are written using the string ->.
• End-of-line comments of the form -- ... are allowed, as are (non-nested) comments of the form {- ... -}.
• There can be a final comma after a non-empty list of constructor arguments, and there can be a final semicolon after a non-empty list of branches.
• Parentheses are treated differently. Superfluous parentheses are allowed around expressions. Some parentheses can be omitted; application is treated as a left-associative operation. Note that some grammatically correct expressions actually parse differently with this variant of the grammar, for instance (rec x = x y) which is interpreted as rec x = (x y) rather than (rec x = x) y (which was previously grammatically incorrect). See the grammar for details.

If you want to use Haskell then there is also a wrapper module (Chi.cf) that exports the generated abstract syntax and some definitions that may be useful for testing your code (documentation). The wrapper module comes with a Cabal file (chi.cabal) and a cabal.project file that might make installation a little easier. Here is one way to (hopefully) get started:

• Install all dependencies properly, including suitable versions of GHC and cabal-install (installation instructions), as well as BNFC.
• Put Chi.cf, Chi.hs, chi.cabal and cabal.project in an otherwise empty directory.

• Run bnfc --haskell Chi.cf in that directory.

  • Now it is hopefully possible to use standard cabal commands. You could for instance try the following (still in the same directory):
  • First use cabal repl to start GHCi.
  • Then issue the following commands at the GHCi command prompt:

  import Chi
  import Prelude
  pretty <$> (runDecode (decode =<<
                      asDecoder (code =<< code (parse "\\x. x"))))

Exercises

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

Please provide your source code in a form which is easy to test, not, say, a PDF file. Do not submit the files provided on this page or the generated code, only the code that you write.

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

(1p)

Consider the following $\chi$ program:

rec foo = \m. \n. case m of
  { Zero() → case n of
    { Zero() → True()
    ; Suc(n) → False()
    }
  ; Suc(m) → case n of
    { Zero() → False()
    ; Suc(n) → foo m n
    }
  }

Give a high-level explanation of the mathematical function in $\mathbb{N} \rightarrow \mathbb{N} \rightarrow \text{Bool}$ that is implemented by this code.

Answer

The function will check for equality of the two natural numbers. If they are both $Zero()$, then it returns true, and if both are the successor of a some values, it checks if they are equal. In the other cases, it returns false.

(2p)

Consider the $\chi$ term t with concrete syntax $C (\lambda z.z)$:

• Give the abstract syntax corresponding to t. Use the abstract syntax presented in the lectures. The answer should be a value in the set Exp.
• Give the concrete syntax of the (standard) $\chi$ representation of t.
• Give the abstract syntax of the (standard) $\chi$ representation of t.

In the abstract syntax the constructor C should be represented by $\underline{C} \in \text{Const}$, and the variable z by $\underline{z} \in \text{Var}$. When giving the $\chi$ representation of the term you should use (the representation of) the number 0 to represent $\underline{C}$, and 1 to represent $\underline{z}$.

Answer

The abstract syntax is the following: \[ \text{const}\ \underline{C}\ (\text{cons}\ (\text{lambda}\ \underline{z}\ (\text{var}\ \underline{z}))\ \text{nil}) \]

The concrete syntax of the standard representation is the following: \[ \text{Const}(\ulcorner \underline{C} \urcorner, \text{Cons}(\text{Lambda}(\ulcorner \underline{z} \urcorner, \text{Cons} (\text{Var}(\ulcorner \underline{z} \urcorner), \text{Nil}())), \text{Nil}())) \]

The abstract syntax of the standard representation, given that $\underline{z}$ and $\underline{C}$ corresponds to zero: \[ \text{Const}(\text{Zero}(), \text{Cons}(\text{Lambda}(\text{Zero}(), \text{Cons} (\text{Var}(\text{Zero}()), \text{Nil}())), \text{Nil}())) \]

(2p) [BN]

Implement substitution for $\chi$. 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	$\lambda x.x$	$\lambda x. (x y)$	$\lambda x . (x (\lambda x . x))$
z	$C(\lambda z . z)$	$\text{case}\ z\ \text{of}\ \{ C(z) \rightarrow z \}$	$\text{case}\ C(\lambda z. z) \ \text{of}\ \{ C(z) \rightarrow z \}$

Answer

See Assignment.hs

(1p)

Implement multiplication of natural numbers in $\chi$, using the representation of natural numbers given in the $\chi$ 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.

Answer

\m. rec mult = \n. case n of
  { Zero() -> Zero()
  ; Succ(n) -> add m (mult n)
  }

where we substitute add for the following:

\m. rec add = \n. case n of
  { Zero() -> m
  ; Succ(n) -> Suc(add n)
  }

(2p) [BN]

Implement an interpreter for $\chi$. The interpreter should be a partial function from closed terms to values, and should implement the operational semantics of $\chi$.

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 your code is tested, then your solution will not be accepted. Also make sure that the following examples are implemented correctly:

• The following programs should fail to terminate:

  • $C() C()$
  • $case \lambda x.x of {}$
  • $case C() of { C(x) \rightarrow C() }$
  • $case C(C()) of { C() \rightarrow C() }$
  • $case C(C()) of { C() \rightarrow C(); C(x) \rightarrow x }$
  • $case C() of { D() \rightarrow D() }$
  • $(\lambda x.\lambda y.x) (rec x = x)$

• The following programs should terminate with specific results:

  • The program $case C(D(),E()) of { C(x, x) \rightarrow x }$ should terminate with the value $E()$.
  • The program $case C(\lambda x.x, Zero()) of { C(f, x) \rightarrow f x }$ should terminate with the value $Zero()$.
  • The program $case (\lambda x.x) C() of { C() \rightarrow C() }$ should terminate with the value $C()$.
  • The program $((\lambda x.x)(\lambda x.x))(\lambda x.x)$ should terminate with the value $\lambda x.x$.

Note that 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.

Answer