Hand ins

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/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

@@ -16,6 +16,24 @@ Either prove that the following function is $\chi$ computable, or that it is not
 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?
 
@@ -120,7 +138,8 @@ Let a two-tape Turing machine be defined by the following:
 \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 S \times (\Gamma \times \{L,R\}) \times (\Gamma \times \{L,R\})$}
+\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}
@@ -164,3 +183,11 @@ 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) \]
+