In order to pass this assignment you have to get at least two points.
(2p) Implement a Turing machine interpreter using χ.
The interpreter should be a closed χ expression. If we denote this expression by run, then it should satisfy the following property (but you do not have to prove that it does):
For every Turing machine tm and input string xs ∈ List {0, 1} the following equation should hold:
⌜⟦ tm ⟧ xs⌝ = ⟦ Apply(Apply(run, ⌜tm⌝), ⌜xs⌝) ⟧
(The ⟦_⟧ brackets to the left stand for the Turing machine semantics, and the ⟦_⟧ brackets to the right stand for the χ semantics.)
Turing machines should be represented in the following way:
States are represented as natural numbers, represented in the usual way.
The set of states is not represented explicitly, but defined implicitly by the states that are mentioned in the definition.
The input alphabet is {0, 1}, with 0 represented by Zero() and 1 by Succ(Zero()).
The tape alphabet is not represented explicitly, but contains the blank character (Blank()), 0, 1 and a finite number of other natural numbers (represented in the usual way).
The transition function is specified by a list of rules (using the usual list constructors). Each rule has the following form: Rule(s₁, x₁, s₂, x₂, d). The value of the transition function for a given state s and symbol x is determined by finding the first rule in the list of rules for which s = s₁ and x = x₁. If there is no matching rule, then the transition function is undefined for the given input. If there is a matching rule Rule(s₁, x₁, s₂, x₂, d), then the new state is s₂, the symbol written is x₂, and the head is moved in the direction d.
Finally a Turing machine is represented by TM(s₀, δ), where s₀ is the initial state and δ is the transition function.
The input and output strings should be represented as lists of symbols.
Please test that addition, implemented as in Tutorial 5, Exercise 6, works as it should when run on your Turing machine interpreter. A testing procedure that you can use has been added to the wrapper module (documentation).
(2p) Prove that every Turing-computable partial function in ℕ ⇀ ℕ is also χ-computable. You can assume that the definition of "Turing-computable" uses Turing machines of the kind used in the previous exercise.
Hint: Use the interpreter from the previous exercise. Do not forget to convert the input and output to the right formats.