Move for next

3or4or6/Interpreter/Turing.hs

@@ -0,0 +1,4 @@
+-- | 
+
+module Interpreter.Turing where
+

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,\\
+                \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?
 
@@ -164,3 +182,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) \]
+