## ~jorge-jbs/theory-of-computation

edd33e47baf11b4685cce96c4baffa28f5de7fdc — Jorge Blázquez Saborido 1 year, 9 months ago
```Implement multi-tape Turing machines
```
```2 files changed, 240 insertions(+), 1 deletions(-)

A MTTM.agda
M TM.agda
```
`A MTTM.agda => MTTM.agda +239 -0`
```@@ 0,0 1,239 @@
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
+
+module MTTM where
+
+open import Cubical.Foundations.Prelude hiding (_∎)
+open import Cubical.Foundations.Logic
+open import Cubical.Foundations.Function
+open import Cubical.HITs.PropositionalTruncation.Base
+open import Cubical.Relation.Nullary using (Discrete; yes; no)
+open import Cubical.Data.List hiding ([_])
+open import Cubical.Data.Vec as Vec hiding (head; tail)
+open import Cubical.Data.Nat
+open import Cubical.Data.Maybe
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum as ⊎
+open import Cubical.Data.Unit
+open import Cubical.Codata.Stream
+open Stream
+
+open import Common
+open import Lang
+open import Fin
+
+private
+  variable
+    ℓ : Level
+    A B C : Type ℓ
+
+list-map : (A → B) → List A → List B
+list-map f [] = []
+list-map f (x ∷ xs) = f x ∷ list-map f xs
+
+_∷ₛ_ : A → Stream A → Stream A
+head (x ∷ₛ xs) = x
+tail (x ∷ₛ xs) = xs
+
+repeat : A → Stream A
+tail (repeat x) = repeat x
+
+data Suffix {A : Type₀} : Stream A → Stream A → Type₀ where
+  here : ∀ {xs} → Suffix xs xs
+  there : ∀ {xs y ys} → Suffix xs ys → Suffix xs (y , ys)
+
+from-list : A → List A → Stream A
+from-list z [] = repeat z
+from-list z (x ∷ xs) = x ∷ₛ from-list z xs
+
+vec-map₂ : ∀ {k} → (A → B → C) → Vec A k → Vec B k → Vec C k
+vec-map₂ f [] [] = []
+vec-map₂ f (x ∷ xs) (y ∷ ys) = f x y ∷ vec-map₂ f xs ys
+
+vec-repeat : ∀ {k} → A → Vec A k
+vec-repeat {k = zero} x = []
+vec-repeat {k = suc k} x = x ∷ vec-repeat x
+
+vec-zip : ∀ {k} → Vec A k → Vec B k → Vec (A × B) k
+vec-zip = {!!}
+
+data Dir : Type₀ where
+  left-dir right-dir : Dir
+
+module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
+  --| Multi-tape Turing machines over an alphabet A.
+  record MTTM : Type₁ where
+    field
+      --| States.
+      State : Type₀
+      {{isFinSetState}} : isFinSet State
+      --| Symbols exclusively for the tape.
+      InternalSymbol : Type₀
+      {{isFinSetInternalSymbol}} : isFinSet InternalSymbol
+      --| Number of work tapes
+      num-work-tapes : ℕ
+
+    {-|
+    The tape symbols (i.e. the input symbols plus the exclusively tape symbols).
+    -}
+    TapeSymbol : Type₀
+    TapeSymbol = A ⊎ InternalSymbol
+
+    {-|
+    Total number of tapes (i.e. the number of work tapes plus one for the input
+    tape).
+    -}
+    num-tapes : ℕ
+    num-tapes = suc num-work-tapes
+
+    field
+      --| Transition function.
+      δ
+        : State
+        → Vec TapeSymbol num-tapes
+        → State × Vec (TapeSymbol × Dir) num-tapes
+      --| Initial state.
+      init : State
+      --| Blank symbol.
+      blank : InternalSymbol
+      {-|
+      Accepting states.
+
+      A multi-tape Turing machine can only halt by reaching a final state, and
+      it always halts when it reaches a final state.
+      -}
+      FinalState : ℙ State
+
+    blank′ = ⊎.inr blank
+
+    record Tape : Type₀ where
+      constructor mk-tape
+      field
+        --| Symbols on the left of the head.
+        left : Stream TapeSymbol
+        --| Symbols on the head of the tape.
+        --| Symbols on the right of the head.
+        right : Stream TapeSymbol
+
+    Tapes : Type₀
+    Tapes = Vec Tape num-tapes
+
+    heads : Tapes → Vec TapeSymbol num-tapes
+
+    blanks : Stream TapeSymbol
+    blanks = repeat blank′
+
+    blank-tape : Tape
+    Tape.left blank-tape = blanks
+    Tape.right blank-tape = blanks
+
+    {-|
+    We say a stream is bounded when, past a point, all its elements are the same.
+    Or, in other words, it has a suffix of the form `repeat z` for some z.
+    -}
+    IsBoundedStream : Stream TapeSymbol → Type₀
+    IsBoundedStream = Suffix blanks
+
+    IsBoundedTape : Tape → Type₀
+    IsBoundedTape (mk-tape l _ r) = IsBoundedStream l × IsBoundedStream r
+
+    move : Dir → Tape → Tape
+    Tape.left (move left-dir (mk-tape l h r)) = l .tail
+    Tape.right (move left-dir (mk-tape l h r)) = h ∷ₛ r
+    Tape.left (move right-dir (mk-tape l h r)) = h ∷ₛ l
+    Tape.right (move right-dir (mk-tape l h r)) = r .tail
+
+    move-all : Tapes → Vec (TapeSymbol × Dir) num-tapes → Tapes
+      vec-map₂
+        (λ (mk-tape l h r) (h′ , dir) → move dir (mk-tape l h′ r))
+        tapes
+
+    initial-input-tape : List A → Tape
+    Tape.left (initial-input-tape xs) = blanks
+    Tape.head (initial-input-tape []) = blank′
+    Tape.head (initial-input-tape (x ∷ xs)) = ⊎.inl x
+    Tape.right (initial-input-tape []) = blanks
+    Tape.right (initial-input-tape (x ∷ xs)) = from-list blank′ (list-map ⊎.inl xs)
+
+    initial-tapes : List A → Tapes
+    initial-tapes w = initial-input-tape w ∷ vec-repeat blank-tape
+
+    record Config : Type₀ where
+      constructor config
+      field
+        --| Current state.
+        state : State
+        --| The tapes.
+        tapes : Tapes
+
+    data _⊢_ : Config → Config → Type₀ where
+      step
+        : ∀ {q tapes}
+        → config q tapes ⊢ config p (move-all tapes heads-and-dirs)
+
+    {-|
+    Multi-tape multi-tape Turing machines can step from one configuration to
+    another in only one way.
+    -}
+    isProp-⊢ : ∀ {C D} → isProp (C ⊢ D)
+    isProp-⊢ = TODO
+
+    {-|
+    Given a multi-tape multi-tape Turing machine configuration, there is only
+    one configuration that goes after it, or none.
+    -}
+    tm-deterministic : ∀ {C} → isProp (Σ[ D ∈ Config ] C ⊢ D)
+    tm-deterministic = TODO
+
+    infix  3 _∎
+    infixr 2 _⊢⟨_⟩_
+
+    --| The transitive closure of `_⊢_`.
+    data _⊢*_ : Config → Config → Type₀ where
+      _∎
+        : ∀ I
+        → I ⊢* I
+      _⊢⟨_⟩_
+        : ∀ I {J K}
+        → I ⊢ J
+        → J ⊢* K
+        → I ⊢* K
+
+    {-|
+    The language accepted by a multi-tape multi-tape Turing machine.
+    -}
+    lang : Lang A
+    lang w = ∃[ p ∶ State ] ∃[ final-tapes ∶ Tapes ]
+      FinalState p ⊓ ∥ config init (initial-tapes w) ⊢* config p final-tapes ∥ₚ
+
+  module _ (M : MTTM) where
+    open MTTM M
+
+    {-
+    {-|
+    A multi-tape multi-tape Turing machine can only read/write finitely many
+    cells in finite time.
+
+    tapes `initial-tapes w` where `w` is the input to the machine.
+    -}
+    is-bounded-tape
+      : ∀ {w C}
+      → config init (initial-tape w) ⊢* C
+      → IsBoundedTape (Config.tape C)
+    is-bounded-tape = TODO
+    -}
+
+  {-|
+  Languages definable by multi-tape multi-tape Turing machines.
+  -}
+  MttmLangs : ℙ (Lang A)
+  MttmLangs L = ∃[ M ∶ MTTM ] (MTTM.lang M ≡ L) , powersets-are-sets _ _

```
`M TM.agda => TM.agda +1 -1`
```@@ 117,7 117,7 @@ module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
blanks = repeat blank′

{-|
-    We say a stream is bounded when, past a point, all its elements are repeated.
+    We say a stream is bounded when, past a point, all its elements are the same.
Or, in other words, it has a suffix of the form `repeat z` for some z.
-}
IsBoundedStream : Stream TapeSymbol → Type₀

```