diff --git a/5.org b/5.org index 3623613..53a3a87 100644 --- a/5.org +++ b/5.org @@ -2,6 +2,7 @@ #+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. @@ -27,7 +28,6 @@ Then, a function $f \in \mathbb{N} \rightarrow \mathbb{N}$ would be turing compu + $\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). @@ -50,14 +50,109 @@ 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 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). ++ 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 \]