Hand ins

Hm?

Huh?

3or4/Interpreter/Self.hs

@@ -1,58 +0,0 @@
-{-# Language LambdaCase, Strict #-}
-
-module Interpreter.Self where
-
-import Chi
-import Interpreter.Haskell
-
-mapExp :: Exp
-mapExp = parse
-  "\\f. rec map = \\xs. case xs of \
-  \ { Nil() -> Nil() \
-  \ ; Cons(x,xs) -> Cons(f x, map xs)\
-  \ }"
-
-ifExp :: Exp
-ifExp = parse
-  "\\b. \\t. \\f. case b of \
-  \ { True() -> t \
-  \ ; False() -> f \
-  \ }"
-
-equalExp :: Exp
-equalExp = parse
-  "rec equal = \\m. \\n. case m of \
-  \ { Zero() -> case n of { Zero() -> True(); Suc(n) -> False() } \
-  \ ; Suc(m) -> case n of { Zero() -> False(); Suc(n) -> equal m n }\
-  \ }"
-
-elemExp :: Exp
-elemExp =
-  subst (Variable "equal") equalExp .
-  subst (Variable "if") ifExp $ parse
-  "\\x. rec elem = \\l. case l of \
-  \ { Nil() -> False() \
-  \ ; Cons(v,vs) -> if (equal x v) True() (elem vs)\ 
-  \ }"
-
-substBrExp :: Exp
-substBrExp =
-  subst (Variable "elem") elemExp $ parse
-  "\\subst. \\var. \\b. case b of \
-  \ { Branch(c,vs,e') -> if (elem var vs) Branch(c,vs,e') Branch(c,vs, subst e') \
-  \ }"
-
-substExp :: Exp
-substExp =
-  subst (Variable "if") ifExp .
-  subst (Variable "equal") equalExp .
-  subst (Variable "substBr") substBrExp .
-  subst (Variable "map") mapExp $ parse
-        "\\var. \\e. rec subst = \\x. case x of\
-        \ { Apply(e1,e2) -> Apply(subst e1, subst e2) \
-        \ ; Lambda(x,y) -> if (equal x var) Lambda(x,y) Lambda(x,subst y) \
-        \ ; Var(x) -> if (equal x var) e Var(x) \
-        \ ; Const(c,es) -> Const(c, map subst es) \
-        \ ; Rec(x, e') -> if (equal x var) Rec(x,e') Rec(x,subst e')\
-        \ ; Case(e',bs) -> Case(subst e', map (substBr subst var) bs) \
-        \ }"

3or4or6/4.org

@@ -21,12 +21,19 @@ Prove that the following functions is not $\chi$ computable (where /Exp/ is the
 You should prove this by reducing the "intensional" halting problem (see the [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/lectures/L4.pdf][lecture slides]]) to this function.
 
 ** Answer
+The halting problem can be reduced to this problem, by the expression:
+\[ \lambda p. f\ ((\lambda \_. Zero()) p) \]
+
+In the case where p terminates, the $(\lambda \_. Zero()) p$ would evaluate to $Zero()$, and therefore $f ((\lambda \_. Zero()) p)$ would evaluate to true.
+In the case where p does not terminate, then $(\lambda \_. Zero()) p$ would not evaluate to $Zero()$ as $p$ would not terminate with a value, therefore $f ((\lambda \_. Zero()) p)$ would evaluate to false.
 
 * (2p)
 Implement $\chi$ substitution as a $\chi$ program. You should construct a $\chi$ expressions, 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 \ulcorner x \urcorner \ulcorner e \urcorner \ulcorner e' \urcorner \Downarrow \ulcorner e' [ x \leftarrow e] \urcorner \]
 
 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 [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][wrapper module]] ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.html][documentation]]) contains some testing procedures, as well as routines for representing natural numbers and $\chi$ abstract syntax as constructor trees.
+** Answer
+See =Self.hs=
 
 * (2p)
 Implement a $\chi$ self-interpreter. You should construct a $\chi$ expression, let us call it /eval/, that satisfies the following properties:
@@ -36,17 +43,19 @@ Implement a $\chi$ self-interpreter. You should construct a $\chi$ expression, l
 You do not need to prove formally that these properties are satisfied, but please test your code. Make sure that the following examples are implemented correctly:
 - The program $\text{eval}\ \ulcorner e \urcorner$ should fail to terminate when e is any of the following programs:
   + $\text{C}()\ \text{C}()$
-  + $\text{case}\ \lambda x.x\ \text{of}\ {}$
-  + $\text{case}\ \text{C}()\ \text{of}\ { \text{C}(x) \rightarrow \text{C}() }$
-  + $\text{case}\ \text{C}(\text{C}())\ \text{of}\ { \text{C}() \rightarrow \text{C}() }$
-  + $\text{case}\ \text{C}(\text{C}())\ \text{of}\ { \text{C}() \rightarrow \text{C}(); \text{C}(x) \rightarrow x }$
-  + $\text{case} \text{C}()\ \text{of}\ { \text{D}() \rightarrow \text{D}() }$
+  + $\text{case}\ \lambda x.x\ \text{of}\ \{\}$
+  + $\text{case}\ \text{C}()\ \text{of}\ \{ \text{C}(x) \rightarrow \text{C}() \}$
+  + $\text{case}\ \text{C}(\text{C}())\ \text{of}\ \{ \text{C}() \rightarrow \text{C}() \}$
+  + $\text{case}\ \text{C}(\text{C}())\ \text{of}\ \{ \text{C}() \rightarrow \text{C}(); \text{C}(x) \rightarrow x \}$
+  + $\text{case}\ \text{C}()\ \text{of}\ \{ \text{D}() \rightarrow \text{D}() \}$
   + $(\lambda x.\lambda y.x) (\text{rec}\ x = x)$
 
 - The following programs should terminate with specific results:
-  + The program $\text{eval}\ \ulcorner case C(D(),E()) of { C(x, x) \rightarrow x } \urcorner$ should terminate with the value $\ulcorner E() \urcorner$.
-  + The program $\text{eval}\ \ulcorner case C(\lambda x.x, Zero()) of { C(f, x) \rightarrow f x } \urcorner$ should terminate with the value $\ulcorner Zero() \urcorner$.
-  + The program $\text{eval}\ \ulcorner case (\lambda x.x) C() of { C() \rightarrow C() } \urcorner$ should terminate with the value $\ulcorner C() \urcorner$.
+  + The program $\text{eval}\ \ulcorner \text{case}\ C(D(),E())\ \text{of}\ \{ C(x, x) \rightarrow x \} \urcorner$ should terminate with the value $\ulcorner E() \urcorner$.
+  + The program $\text{eval}\ \ulcorner \text{case}\ C(\lambda x.x, Zero())\ \text{of}\ \{ C(f, x) \rightarrow f x \} \urcorner$ should terminate with the value $\ulcorner Zero() \urcorner$.
+  + The program $\text{eval}\ \ulcorner \text{case}\ (\lambda x.x) C()\ \text{of}\ \{ C() \rightarrow C() \} \urcorner$ should terminate with the value $\ulcorner C() \urcorner$.
   + The program $\text{eval}\ \ulcorner ((\lambda x.x)(\lambda x.x))(\lambda x.x) \urcorner$ should terminate with the value $\ulcorner \lambda x.x \urcorner$.
 
 For full credit your implementation must evaluate addition of natural numbers correctly, i.e. $\text{eval} \ulcorner \text{add}\ \ulcorner m \urcorner \ \ulcorner n \urcorner  \urcorner$ must terminate with the value $\ulcorner \ulcorner m + n \urcorner  \urcorner$, for arbitrary (small) $m, n \in \mathbb{N}$ (where add is an implementation of addition). The wrapper module contains some testing procedures that you can use.
+** Answer
+See =Self.hs=

3or4or6/6.org

@@ -0,0 +1,69 @@
+#+title: Assignment 6
+#+options: toc:nil
+#+latex_header: \usepackage{parskip}
+#+latex_header: \usepackage{stmaryrd}
+#+latex_header: \usepackage{bussproofs}
+
+In order to pass this assignment you have to get at least two points.
+
+* (2p)
+The following string represents a Turing machine, using the encoding presented in the lectures:
+
+\[ 1001100 1 0 10 10 10 1  1 0 110 10 110 1  1 10 10 0 0 1  1 10 110 0 0 1 0 \]
+
+The following string is an encoding, using the encoding presented in the lectures, of some input to the Turing machine:
+
+\[ 110110111011011100 \]
+
+What Turing machine and what input do the strings represent? And what is the result of running the Turing machine with the given input?
+
+** Answer
+
+The Turing machine is the one described by the following:
+
+- States: $S = \{ s_0, s_1 \}$
+- Initial state: $s_0$
+- Input alphabet: $\{c_1,c_2\}$
+- Tape alphabet: $\{\text{\textvisiblespace},c_1,c_2\}$
+- Transition function:
+  + $\delta (s_0, c_1) = (s_1,c_1,R)$
+  + $\delta (s_0, c_2) = (s_1,c_2,R)$
+  + $\delta (s_1, c_1) = (s_0,\text{\textvisiblespace},R)$
+  + $\delta (s_1, c_2) = (s_0,\text{\textvisiblespace},R)$
+  
+Running the machine on the given input, results in erasing every other character.
+
+* (2p)
+
+Implement a Turing machine interpreter using $\chi$.
+
+The interpreter should be a closed $\chi$ 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 \in \text{List}\ \{0, 1\}$ the following equation should hold:
+  \[ \llbracket \text{apply}\ (\text{apply}\ \text{\textit{run}}\ \ulcorner \text{tm} \urcorner) \ulcorner xs \urcorner \rrbracket = \ulcorner \llbracket \text{tm} \rrbracket\ \text{xs} \urcorner \]
+(The $\llbracket \_ \rrbracket$ brackets to the left stand for the $\chi$ semantics, and the $\llbracket \_ \rrbracket$ brackets to the right stand for the Turing machine 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 $Suc(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 form $Rule(s_1, x_1, s_2, x_2, d)$, where $s_1$ and $s_2$ are states, $x_1$ and $x_2$ are tape alphabet symbols, and $d$ is a direction (left is represented by $L()$ and right by $R()$).
++ For a given state $s_1$ and symbol $x_1$ there must be at most one rule with $s_1$ as the first component and $x_1$ as the second component. Furthermore the list of rules must be sorted lexicographically based on these two components: entries with smaller states must precede entries with larger states, and entries with equal states must be sorted based on the symbols (with blanks sorted before the natural numbers).
++ The value of the transition function for a given state $s$ and symbol $x$ is given by the rule with $s = s_1$ and $x = x_1$, if any: if there is no such rule, then the transition function is undefined for the given input. If there is a matching rule $Rule(s_1, x_1, s_2, x_2, d)$, then the new state is $s_2$, the symbol written is $x_2$, and the head is moved in the direction $d$ (if possible).
++ Finally a Turing machine is represented by $TM(s_0, \delta)$, where $s_0$ is the initial state and $\delta$ is the transition function.
+
+The input and output strings should use the usual representation of lists, with the representation specified above for the input and tape symbols.
+
+Please test that addition, implemented as in Tutorial 5, Exercise 6 (with 0 instead of #), works as it should when run on your Turing machine interpreter. A testing procedure that you can use is included in the wrapper module (documentation).
+
+** Answer
+See =Turing.hs=
+* (2p)
+Prove that every Turing-computable partial function in $\mathbb{N} \rightharpoonup \mathbb{N}$ is also $\chi$ 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.
+** Answer
+We know that we can construct an interpreter for Turing machines, and a translation of $\mathbb{N}$ to the language a Turing machine.
+We also know that one can construct an interpreter in the form of a Turing machine of $\chi$, and the opposite.
+This means that a partial function can be translated from $\chi$ to a Turing machine.
+So, given a partial function, one can translate it to a Turing machine, and translate the input, and run the implemented Turing interpreter from the last task, and then translate the result back into $\chi$.

3or4or6/Interpreter/Self.hs

@@ -0,0 +1,99 @@
+{-# Language LambdaCase, Strict #-}
+
+module Interpreter.Self where
+
+import Chi
+import Interpreter.Haskell
+
+-- Task 3
+
+mapExp :: Exp
+mapExp = parse
+  "\\f. rec map = \\xs. case xs of \
+  \ { Nil() -> Nil() \
+  \ ; Cons(x,xs) -> Cons(f x, map xs)\
+  \ }"
+
+equalExp :: Exp
+equalExp = parse
+  "rec equal = \\m. \\n. case m of \
+  \ { Zero() -> case n of { Zero() -> True(); Suc(n) -> False() } \
+  \ ; Suc(m) -> case n of { Zero() -> False(); Suc(n) -> equal m n }\
+  \ }"
+
+elemExp :: Exp
+elemExp =
+  subst (Variable "equal") equalExp $ parse
+  "\\x. rec elem = \\l. case l of \
+  \ { Nil() -> False() \
+  \ ; Cons(v,vs) -> case (equal x v) of { True() -> True(); False() -> (elem vs) } \
+  \ }"
+
+substBrExp :: Exp
+substBrExp =
+  subst (Variable "elem") elemExp $ parse
+  "\\subst. \\var. \\b. case b of \
+  \ { Branch(c,vs,e') -> case (elem var vs) of \
+  \   { True() -> Branch(c,vs,e') \
+  \   ; False() -> Branch(c,vs, subst e') \
+  \   } \
+  \ }"
+
+substExp :: Exp
+substExp =
+  subst (Variable "equal") equalExp .
+  subst (Variable "substBr") substBrExp .
+  subst (Variable "map") mapExp $ parse
+        "\\var. \\e. rec subst = \\x. case x of\
+        \ { Apply(e1,e2) -> Apply(subst e1, subst e2) \
+        \ ; Lambda(x,y) -> case (equal x var) of \
+        \     { True() -> Lambda(x,y) \
+        \     ; False() -> Lambda(x,subst y) \
+        \     } \
+        \ ; Var(x) -> case (equal x var) of {True() -> e; False() -> Var(x)} \
+        \ ; Const(c,es) -> Const(c, map subst es) \
+        \ ; Rec(x, e') -> case (equal x var) of {True() -> Rec(x,e'); False() -> Rec(x,subst e')}\
+        \ ; Case(e',bs) -> Case(subst e', map (substBr subst var) bs) \
+        \ }"
+
+-- Task 4
+
+lookupExp :: Exp
+lookupExp =
+  subst (Variable "equal") equalExp $ parse
+  "\\c. rec lookup = \\xs. case xs of \
+  \ { Cons(b,bs) -> \
+  \     case b of \
+  \       { Branch(c', xs, e') -> case (equal c c') of \
+  \         { True() -> Pair(xs,e') \
+  \         ; False() -> lookup bs \
+  \         } \
+  \       } \
+  \ }"
+
+substsExp :: Exp
+substsExp =
+  subst (Variable "subst") substExp $ parse
+  "rec substs = \\xs. \\vs. \\e'. case xs of \
+  \ { Nil() -> case vs of { Nil() -> e' } \
+  \ ; Cons(x,xs) -> case vs of { Cons(v,vs) -> subst x v (substs xs vs e') }\
+  \ }"
+
+evalExp :: Exp
+evalExp =
+  subst (Variable "map") mapExp .
+  subst (Variable "lookup") lookupExp .
+  subst (Variable "substs") substsExp .
+  subst (Variable "subst") substExp $ parse
+  "rec eval = \\e. case e of \
+  \ { Lambda(x,e) -> Lambda(x,e) \
+  \ ; Apply(e1,e2) -> case eval e1 of \
+  \    { Lambda(x,e) -> eval (subst x (eval e2) e) } \
+  \ ; Rec(x,e) -> eval (subst x Rec(x,e) e) \
+  \ ; Const(c,es) -> Const(c, map eval es) \
+  \ ; Case(e,bs) -> case eval e of \
+  \     { Const(c,vs) -> case lookup c bs of \
+  \        { Pair(xs,e') -> eval (substs xs vs e') } \
+  \     } \
+  \ ; Var(x) -> Var(x) \
+  \ }"

3or4or6/Interpreter/Turing.hs

@@ -0,0 +1,87 @@
+{-# Language LambdaCase, Strict #-}
+
+module Interpreter.Turing where
+
+import Chi
+import Interpreter.Haskell -- from assignment 3
+
+equalExp :: Exp
+equalExp = parse
+  "rec equal = \\m. \\n. case m of \
+  \ { Zero()  -> case n of { Blank() -> False(); Zero() -> True();  Suc(n) -> False() } \
+  \ ; Suc(m)  -> case n of { Blank() -> False(); Zero() -> False(); Suc(n) -> equal m n } \
+  \ ; Blank() -> case n of { Blank() -> True();  Zero() -> False(); Suc(n) -> False() } \
+  \ }"
+
+lookupExp :: Exp
+lookupExp =
+  subst (Variable "equal") equalExp $ parse
+  "\\s. \\head. rec lookup = \\rules. case rules of \
+  \ { Nil() -> Done() \
+  \ ; Cons(x,xs) -> case x of \
+  \   { Rule(s1, x1, s2, x2, d) -> case equal s s1 of \
+  \     { True()  -> case equal head x1 of \
+  \       { True()  -> Trip(s2,x2,d)\
+  \       ; False() -> lookup xs \
+  \       } \
+  \     ; False() -> lookup xs \
+  \     } \
+  \   }\
+  \ } \
+  \ "
+
+joinExp :: Exp
+joinExp = parse
+  "rec join = \\xs. \\ys. case xs of \
+  \ { Nil() -> ys \
+  \ ; Cons(x,xs) -> join xs Cons(x,ys) \
+  \ }"
+
+appendExp :: Exp
+appendExp = parse
+  "rec append = \\xs. \\ys. case xs of \
+  \ { Nil() -> ys \
+  \ ; Cons(x,xs) -> Cons(x,append xs ys) \
+  \ }"
+
+reverseExp :: Exp
+reverseExp =
+  subst (Variable "append") appendExp $ parse
+  "rec reverse = \\xs. case xs of \
+  \ { Nil() -> Nil() \
+  \ ; Cons(x,xs) -> append xs Cons(x,Nil())\
+  \ }"
+
+removeLastBlanksExp :: Exp
+removeLastBlanksExp = parse
+  "rec removeLastBlanks = \\xs. case xs of \
+  \ { Nil() -> Nil() \
+  \ ; Cons(x,xs) -> case x of \
+  \   { Blank() -> removeLastBlanks xs \
+  \   ; Zero()  -> Cons(x,xs) \
+  \   ; Suc(n)  -> Cons(x,xs) \
+  \   } \
+  \ }\
+  \ "
+
+runExp :: Exp
+runExp =
+  subst (Variable "removeLastBlanks") removeLastBlanksExp .
+  subst (Variable "reverse") reverseExp .
+  subst (Variable "join") joinExp .
+  subst (Variable "lookup") lookupExp $ parse
+  "(rec run = \\rev. \\tm. \\tape. case tm of \
+  \ { TM(state,deltas) -> case tape of \
+  \   { Nil() -> run rev TM(state,deltas) Cons(Blank(), Nil()) \
+  \   ; Cons(head,xs) -> case lookup state head deltas of \
+  \     { Done() -> join rev (reverse (removeLastBlanks (reverse tape))) \
+  \     ; Trip(s2, x2, d) -> case d of \
+  \       { L() -> case rev of \
+  \         { Nil() -> run Nil() TM(s2,deltas) Cons(x2,xs) \
+  \         ; Cons(y,ys) -> run ys TM(s2,deltas) Cons(y,Cons(x2,xs)) \
+  \         } \
+  \       ; R() -> run Cons(x2,rev) TM(s2,deltas) xs \
+  \       } \
+  \     } \
+  \   } \
+  \ }) Nil()"

3or4or6/chi.cabal

@@ -26,6 +26,7 @@ library
     PrintChi
     Interpreter.Haskell
     Interpreter.Self
+    Interpreter.Turing
   hs-source-dirs:
     .
 

5.org

@@ -0,0 +1,193 @@
+#+title: Assignment 5
+#+options: toc:nil
+#+latex_header: \usepackage{parskip}
+#+latex_header: \usepackage{stmaryrd}
+#+latex_header: \usepackage{bussproofs}
+
+In order to pass this assignment you have to get at least four points.
+
+* (2p)
+Let /NN/ be the set containing all closed expressions $e$ that implement functions from $\mathbb{N}$ to $\mathbb{N}$, i.e. expressions $e$ that, for some function $f \in \mathbb{N} \rightarrow \mathbb{N}$, satisfy $\forall n \in \mathbb{N}. \llbracket e\ \ulcorner n \urcorner \rrbracket = \ulcorner f\ n \urcorner$.
+
+Either prove that the following function is $\chi$ computable, or that it is not $\chi$ computable:
+\[ \text{has-fixpoint} \in \text{NN} \rightarrow \mathbb{B} \]
+\[ \text{has-fixpoint}\ e = \text{if}\ \exists n \in \mathbb{N}. \llbracket e\ \ulcorner n \urcorner \rrbracket = \ulcorner n \urcorner\ \text{then}\ true\ \text{else}\ false \]
+
+Note that Rice’s theorem, as stated in a lecture, applies to (total) functions from /CExp/ to /Bool/, whereas /has-fixpoint/ is a function from /NN/ to /Bool/.
+
+** Answer
+Assume that $\text{has-fixpoint}$ is $\chi$ computable.
+Then there exists an expression $\underline{\text{has-fixpoint}}$ that implements this function, i.e. $\llbracket \underline{\text{has-fixpoint}}\ \ulcorner p \urcorner \rrbracket = \ulcorner \text{has-fixpoint}(p) \urcorner$.
+With this, lets reduce it to the halting problem.
+We do this by defining it as the following:
+\[ halts = \lambda e. \underline{\text{has-fixpoint}}\ \ulcorner \lambda n. ((\lambda \_. n) \llcorner e \lrcorner) \urcorner \]
+
+Which means
+\begin{align*}
+\llbracket halts\ \ulcorner p \urcorner \rrbracket &= \llbracket \underline{\text{has-fixpoint}}\ \ulcorner \lambda n. ((\lambda \_. n) \llcorner \ulcorner p \urcorner \lrcorner) \urcorner \rrbracket \\
+        &= \llbracket \underline{\text{has-fixpoint}}\ \ulcorner \lambda n. ((\lambda \_. n)\  p) \urcorner \rrbracket \\
+        &= \ulcorner \text{has-fixpoint}(\lambda n. ((\lambda \_. n)\  p)) \urcorner \\
+        &= \begin{cases}
+                \ulcorner \text{true} \urcorner   &\quad \text{if}\ \exists v \in Exp. \llbracket p \rrbracket = v\ \text{(due to strictness in application)},\\
+                \ulcorner \text{false} \urcorner  &\quad otherwise
+           \end{cases}
+\end{align*}
+
+Since the halting problem could be reduced to $\text{has-fixpoint}$, then $\text{has-fixpoint}$ is not $\chi$ computable.
+* (1p)
+When is a function $f \in \mathbb{N} \rightarrow \mathbb{N}$ Turing-computable?
+
+** Answer
+Given that we have a way of representing elements of $\mathbb{N}$ as elements of $\text{List}\ \Sigma$, where $\Sigma$ is the input alphabet of the turing machine.
+This can be used with the alphabet $\{0,1\}$, and represent a natural number $n$ as $1^n0$ (n ones followed by a single zero).
+
+Then, a function $f \in \mathbb{N} \rightarrow \mathbb{N}$ would be turing computable if there is a turing machine $tm$ that satisfies the following conditions:
++ $\Sigma_{tm} = \Sigma$
++ $\forall n \in \mathbb{N}. \llbracket tm \rrbracket \ulcorner a \urcorner = \ulcorner f\ a \urcorner$
+
+This means that the alphabet is the same, and that for any $n$, then the turing machine applied to the representation of $n$ should be the same as the represention of the function $f$ on $n$.
+* (1p)
+The following Turing machine implements a (total) function on the natural numbers. Which one? The natural number $n$ is represented by $1^n0$ (n ones followed by a single zero).
+
+- Input alphabet: $\{0, 1\}$.
+- Tape alphabet: $\{0, 1, \text{\textvisiblespace} \}$.
+- States: $\{s_0, s_1, s_2\}$.
+- Initial state: $s_0$.
+- Transition function:
+  + $\delta (s_0, 1) = (s_0, 1, R)$
+  + $\delta (s_0, 0) = (s_1, 1, R)$
+  + $\delta (s_1, \text{\textvisiblespace}) = (s_2, 0, R)$
+
+** Answer
+It describes the successor function on natural numbers.
+* (2p)
+Implement a Turing machine (with accepting states) that checks if two natural numbers are equal. The machine should use $\{0, 1\}$ as the input alphabet; you may use more symbols in the tape alphabet. The machine should accept input of the form $1^n01^n0$ (for any $n \in \mathbb{N}$). Input of the form $1^m01^n0$ where $m \ne n$ should be rejected.
+
+Explain how your Turing machine works.
+
+Make sure that you specify the Turing machine completely (the set of states, the alphabets, and so on). In addition to this specification you can also optionally submit your Turing machine in the format used by Anthony Morphett's [[http://morphett.info/turing/turing.html][Turing machine simulator]]. (If you go to “Advanced options”, then you can choose to use semi-infinite tapes.)
+
+** Answer
+We define the following as our turing machine.
+
+\[ S = \{\text{DelR}, \text{Move1}, \text{Head2}, \text{Move2}, \text{Move2'}, \text{Find0}, \text{Accept} \} \]
+\[ s_0 = \text{DelR} \]
+\[ A = \{\text{Accept}\} \]
+\[ \Sigma = \{ 0, 1\} \]
+\[ \Gamma = \{ 0 , 1, \text{\textvisiblespace} \}\]
+
+and the following as our transition function.
+
+\begin{alignat*}{2}
+&\delta (\text{DelR}, 0) &&= (\text{Find0}, \text{\textvisiblespace}, R) \\
+&\delta (\text{DelR}, 1) &&= (\text{Move1}, \text{\textvisiblespace}, R) \\
+&\delta (\text{Move1}, 0) &&= (\text{Head2}, 0, R) \\
+&\delta (\text{Move1}, 1) &&= (\text{Move1}, 1, R) \\
+&\delta (\text{Head2}, 1) &&= (\text{Move2}, \text{\textvisiblespace}, L) \\
+&\delta (\text{Head2}, \text{\textvisiblespace}) &&= (\text{Head2}, \text{\textvisiblespace}, R) \\
+&\delta (\text{Move2}, 0) &&= (\text{Move2'}, 0, L) \\
+&\delta (\text{Move2}, \text{\textvisiblespace}) &&= (\text{Move2}, \text{\textvisiblespace}, l) \\
+&\delta (\text{Move2'}, 1) &&= (\text{Move2'}, 1, L) \\
+&\delta (\text{Move2'}, \text{\textvisiblespace}) &&= (\text{DelR}, \text{\textvisiblespace}, R) \\
+&\delta (\text{Find0}, \text{\textvisiblespace}) &&= (\text{Find0}, \text{\textvisiblespace}, R) \\
+&\delta (\text{Find0}, 0) &&= (\text{Accept}, \text{\textvisiblespace}, L) \\
+\end{alignat*}
+
+With these definitions, we have a turing machine that will find if two natural numbers are equal for the given representation.
+I made the program for this below for easy testing on Anthony Morphett's [[http://morphett.info/turing/turing.html][Turing machine simulator]].
+
+#+begin_src turing machine
+DelR 0 _ r Find0
+DelR 1 _ r Move1
+
+Move1 0 0 r Head2
+Move1 1 1 r Move1
+
+Head2 1 _ l Move2
+Head2 _ _ r Head2
+
+Move2 0 0 l Move2'
+Move2 _ _ l Move2
+
+Move2' 1 1 l Move2'
+Move2' _ _ r DelR
+
+Find0 _ _ r Find0
+Find0 0 _ l Accept
+
+Accept _ _ l halt-accept
+Accept 0 _ l halt-accept
+Accept 1 _ l halt-accept
+#+end_src
+* (2p)
+Give a formal definition of (a reasonable variant of) two-tape Turing machines. Explain how such a Turing machine is defined. Also explain what its semantics is: what partial function from strings to strings does it compute?
+
+** Answer
+Let a two-tape Turing machine be defined by the following:
++ $S$: A finite set of states
++ $s_0 \in S$: An initial state
++ $\Sigma$: The input alphabet, which is a finite set of symbols with $\text{\textvisiblespace} \notin \Sigma$
++ $\Gamma$: The tape alphabet, which is a finite set of symbols such that $\Sigma \cup \{\text{\textvisiblespace}\} \subseteq \Gamma$
++ $\delta \in S \times \Gamma \times \Gamma \rightharpoonup S \times (\Gamma \times \{L,R\}) \times (\Gamma \times \{L,R\})$: The transition "function", which has the pair of tapes used.
+
+\begin{prooftree}
+\alwaysNoLine
+\AxiomC{$S$ is a finite set}
+\UnaryInfC{$s_0 \in S$}
+\AxiomC{$\Sigma$ is a finite set}
+\UnaryInfC{$\text{\textvisiblespace} \notin \Sigma$}
+\AxiomC{$\Gamma$ is a finite set}
+\UnaryInfC{$\Sigma \cup \{\text{\textvisiblespace}\} \subseteq \Gamma$}
+\AxiomC{$\delta \in S \times \Gamma \times \Gamma \rightharpoonup$}
+\UnaryInfC{$S \times (\Gamma \times \{L,R\}) \times (\Gamma \times \{L,R\})$}
+\alwaysSingleLine
+\QuaternaryInfC{$(S,s_0, \Sigma, \Gamma, \delta) \in \text{TM2}$}
+\end{prooftree}
+
+
+With all of these, one has a two tape turing machine.
+Utilizing the functions on Tapes from the lectures, one can define the small step operational semantics as follows:
+
+\begin{prooftree}
+\AxiomC{$\delta (s, \text{head}_T\ t, \text{head}_T\ t') = (s', a, a')$}
+\UnaryInfC{$(s,t,t') \rightarrow (s', \text{act}\ a\ t, \text{act}\ a'\ t') $}
+\end{prooftree}
+
+And the result of running the turing machine, with the two inputs $xs$ and $ys$, would be defined by (using /remove/ as defined from the lectures):
+
+\begin{prooftree}
+\AxiomC{$(s_0, ([], xs), ([],ys)) \rightarrow^{*} (s,t,t')$}
+\AxiomC{$\nexists c. (s, t, t') \rightarrow c$}
+\BinaryInfC{$(xs,ys) \Downarrow (\text{remove}\ (\text{list}\ t), \text{remove}\ (\text{list}\ t'))$}
+\end{prooftree}
+
+The semantics would be given as a partial function by:
+
+\begin{align*}
+&\llbracket \_ \rrbracket \in \forall tm \in \text{TM2}.\ \text{List}\ \Sigma_{tm} \times \text{List}\ \Sigma_{tm }\rightharpoonup \text{List}\ \Gamma_{tm} \times \text{List}\ \Gamma_{tm} \\
+&\llbracket tm \rrbracket\ (xs,ys) = (us,ws)\ \text{if}\ (xs,ys) \Downarrow_{tm} (us,ws)
+\end{align*}
+
+* (2p)
+Consider the following variant of the basic Turing machines (without accepting states) presented in the lectures:
+
++ There are three possible directions: $\{L, R, S\}$. $S$ means "stay" (do not move the head).
++ The meaning of S is specified formally by extending move with another clause:
+    \[ \text{move}\ S\ t\ = t \]
+
+Give a translation /remove-stay/ that takes Turing machines of this kind to Turing machines of the basic kind. The translation should satisfy the following property for every Turing machine tm of the extended kind:
+
++ For every input $xs$ and output $ys$, the result of running $tm$ on $xs$ is $ys$ if and only if the result of running /remove-stay tm/ on $xs$ is $ys$.
+
+You do not have to prove formally that this property holds.
+
+/Hint/: You can handle the non-moving actions by first moving the head to the right, and then back to the left, using extra states to program this movement.
+** Answer
+The semantics of remove-stay should be implemented by the following:
+For all states $m \in S$, and forall $x \in \Gamma$, add the following to the transition function:
+\[ \delta (\text{Stay}_m, x) = (m, x, L) \]
+In transition function, where a definition has the output direction as $S$, i.e.
+\[ \delta(n, x) = (m, y, S) \]
+replace that by the following:
+\[ \delta(n, x) = (\text{Stay}_m, y, R) \]
+