From a8c41dfd7d99602462b8d35f363ad9d072b50a9a Mon Sep 17 00:00:00 2001 From: pingu Date: Mon, 8 Dec 2025 15:21:42 +0100 Subject: [PATCH] Move for next --- {3or4 => 3or4or6}/.envrc | 0 {3or4 => 3or4or6}/.gitignore | 0 {3or4 => 3or4or6}/3.org | 0 {3or4 => 3or4or6}/4.org | 0 {3or4 => 3or4or6}/Chi.cf | 0 {3or4 => 3or4or6}/Chi.hs | 0 {3or4 => 3or4or6}/Interpreter/Haskell.hs | 0 {3or4 => 3or4or6}/Interpreter/Self.hs | 0 3or4or6/Interpreter/Turing.hs | 4 ++++ {3or4 => 3or4or6}/app/Main.hs | 0 {3or4 => 3or4or6}/cabal.project | 0 {3or4 => 3or4or6}/chi.cabal | 0 {3or4 => 3or4or6}/flake.lock | 0 {3or4 => 3or4or6}/flake.nix | 0 5.org | 26 ++++++++++++++++++++++++ 15 files changed, 30 insertions(+) rename {3or4 => 3or4or6}/.envrc (100%) rename {3or4 => 3or4or6}/.gitignore (100%) rename {3or4 => 3or4or6}/3.org (100%) rename {3or4 => 3or4or6}/4.org (100%) rename {3or4 => 3or4or6}/Chi.cf (100%) rename {3or4 => 3or4or6}/Chi.hs (100%) rename {3or4 => 3or4or6}/Interpreter/Haskell.hs (100%) rename {3or4 => 3or4or6}/Interpreter/Self.hs (100%) create mode 100644 3or4or6/Interpreter/Turing.hs rename {3or4 => 3or4or6}/app/Main.hs (100%) rename {3or4 => 3or4or6}/cabal.project (100%) rename {3or4 => 3or4or6}/chi.cabal (100%) rename {3or4 => 3or4or6}/flake.lock (100%) rename {3or4 => 3or4or6}/flake.nix (100%) diff --git a/3or4/.envrc b/3or4or6/.envrc similarity index 100% rename from 3or4/.envrc rename to 3or4or6/.envrc diff --git a/3or4/.gitignore b/3or4or6/.gitignore similarity index 100% rename from 3or4/.gitignore rename to 3or4or6/.gitignore diff --git a/3or4/3.org b/3or4or6/3.org similarity index 100% rename from 3or4/3.org rename to 3or4or6/3.org diff --git a/3or4/4.org b/3or4or6/4.org similarity index 100% rename from 3or4/4.org rename to 3or4or6/4.org diff --git a/3or4/Chi.cf b/3or4or6/Chi.cf similarity index 100% rename from 3or4/Chi.cf rename to 3or4or6/Chi.cf diff --git a/3or4/Chi.hs b/3or4or6/Chi.hs similarity index 100% rename from 3or4/Chi.hs rename to 3or4or6/Chi.hs diff --git a/3or4/Interpreter/Haskell.hs b/3or4or6/Interpreter/Haskell.hs similarity index 100% rename from 3or4/Interpreter/Haskell.hs rename to 3or4or6/Interpreter/Haskell.hs diff --git a/3or4/Interpreter/Self.hs b/3or4or6/Interpreter/Self.hs similarity index 100% rename from 3or4/Interpreter/Self.hs rename to 3or4or6/Interpreter/Self.hs diff --git a/3or4or6/Interpreter/Turing.hs b/3or4or6/Interpreter/Turing.hs new file mode 100644 index 0000000..44b834f --- /dev/null +++ b/3or4or6/Interpreter/Turing.hs @@ -0,0 +1,4 @@ +-- | + +module Interpreter.Turing where + diff --git a/3or4/app/Main.hs b/3or4or6/app/Main.hs similarity index 100% rename from 3or4/app/Main.hs rename to 3or4or6/app/Main.hs diff --git a/3or4/cabal.project b/3or4or6/cabal.project similarity index 100% rename from 3or4/cabal.project rename to 3or4or6/cabal.project diff --git a/3or4/chi.cabal b/3or4or6/chi.cabal similarity index 100% rename from 3or4/chi.cabal rename to 3or4or6/chi.cabal diff --git a/3or4/flake.lock b/3or4or6/flake.lock similarity index 100% rename from 3or4/flake.lock rename to 3or4or6/flake.lock diff --git a/3or4/flake.nix b/3or4or6/flake.nix similarity index 100% rename from 3or4/flake.nix rename to 3or4or6/flake.nix diff --git a/5.org b/5.org index 53a3a87..87fae1e 100644 --- a/5.org +++ b/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) \] +