In order to pass this assignment you have to get at least three points.
(1p) Define what a χ-computable function on the natural numbers is.
(2p) Prove that the following function is not χ-computable (where Exp is the abstract syntax of χ):
f ∈ { p ∈ Exp | p is closed } → Bool
f p = if p terminates with the value Zero() then true else false
You should prove this by reducing the "intensional" halting problem (see the lecture slides) to this function.
(2p) Implement χ substitution as a χ program. You should construct a χ expression, let us call it subst, that given the representation of a variable x, a closed expression e, and an expression e′, produces the representation of the expression obtained by substituting e for every free occurrence of x in e′:
subst ⌜x⌝ ⌜e⌝ ⌜e′⌝ ⇓ ⌜e′ [ x ← e ]⌝.
You do not need to prove formally that this property is satisfied, but please test your code. You can for instance test that this implementation of substitution matches the one from the last assignment. The wrapper module (documentation) contains some testing procedures, as well as routines for representing natural numbers and χ abstract syntax as constructor trees.
(2p) Implement a χ self-interpreter. You should construct a χ expression, let us call it eval, that satisfies the following properties:
For any closed expressions e and v, if e ⇓ v then eval ⌜e⌝ ⇓ ⌜v⌝.
For any closed expressions e and v, if eval ⌜e⌝ ⇓ v, then there should be some v′ such that e ⇓ v′ and v = ⌜v′⌝.
You do not need to prove formally that these properties are satisfied, but please test your code. For full credit your implementation must evaluate addition of natural numbers correctly, i.e. eval ⌜add ⌜m⌝ ⌜n⌝⌝ must terminate with the value ⌜m + n⌝, for arbitrary (small) m, n ∈ ℕ (where add is an implementation of addition). The wrapper module contains some testing procedures that you can use.
Please provide your source code in a form which is easy to test, not, say, a PDF file.