~jorge-jbs/theory-of-computation

0bb075e69013078a263e09bb76524d4ee2d407e1 — Jorge Blázquez Saborido 1 year, 9 months ago 454a3a8
Add definition of Turing Machines
1 files changed, 244 insertions(+), 0 deletions(-)

A TM.agda
A TM.agda => TM.agda +244 -0
@@ 0,0 1,244 @@
{-# OPTIONS --cubical --allow-unsolved-metas #-}

module TM 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.Maybe
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as ⊎
open import Cubical.Data.Unit

open import Common
open import Lang
open import Fin

private
  variable
    ℓ : Level
    A B : Type ℓ

data LastIsNot {A : Type ℓ} (z : A) : List A → Type ℓ where
  lin-nil : LastIsNot z []
  lin-singleton : ∀ {x} → (x ≡ z → [ ⊥ ]) → LastIsNot z (x ∷ [])
  lin-cons : ∀ {x y xs} → LastIsNot z (x ∷ xs) → LastIsNot z (y ∷ x ∷ xs)

inl-neq-inr : ∀ {x : A} {y : B} → ⊎.inl x ≡ ⊎.inr y → [ ⊥ ]
inl-neq-inr {x = x} {y = y} inl-eq-inr =
  elim {C = C} (λ _ → C-inl) (λ _ → C-inr) (⊎.inr y)
  where
    C : A ⊎ B → Type _
    C (⊎.inl _) = [ ⊤ ]
    C (⊎.inr _) = [ ⊥ ]

    C-inl : C (⊎.inl x)
    C-inl = tt

    C-inr : C (⊎.inr y)
    C-inr = transport (cong C inl-eq-inr) C-inl

list-map : (A → B) → List A → List B
list-map f [] = []
list-map f (x ∷ xs) = f x ∷ list-map f xs

lin-map-inl
  : ∀ {z : B} {xs : List A}
  → LastIsNot (⊎.inr z) (list-map ⊎.inl xs)
lin-map-inl {xs = []} = lin-nil
lin-map-inl {xs = x ∷ []} = lin-singleton inl-neq-inr
lin-map-inl {xs = x ∷ y ∷ xs} = lin-cons (lin-map-inl {xs = y ∷ xs})

data Dir : Type₀ where
  left-dir right-dir : Dir

module _ {A : Type ℓ} (_≟_ : Discrete A) (blank : A) where
  move : Dir → List A → A → List A → List A × A × List A
  move left-dir [] z [] with z ≟ blank
  ... | yes _ = [] , blank , []
  ... | no _ = [] , blank , z ∷ []
  move left-dir [] z (y ∷ ys) = [] , blank , z ∷ y ∷ ys
  move left-dir (x ∷ xs) z [] with z ≟ blank
  ... | yes _ = xs , x , []
  ... | no _ = xs , x , z ∷ []
  move left-dir (x ∷ xs) z (y ∷ ys) = xs , x , z ∷ y ∷ ys
  move right-dir [] z [] with z ≟ blank
  ... | yes _ = [] , blank , []
  ... | no _ = z ∷ [] , blank , []
  move right-dir (x ∷ xs) z [] = z ∷ x ∷ xs , blank , []
  move right-dir [] z (y ∷ ys) with z ≟ blank
  ... | yes _ = [] , y , ys
  ... | no _ = z ∷ [] , y , ys
  move right-dir (x ∷ xs) z (y ∷ ys) = z ∷ x ∷ xs , y , ys

  -- This should really be automated -.-
  lin-move
    : (dir : Dir)
    → {xs : List A}
    → {z : A}
    → {ys : List A}
    → (let xs′ , z′ , ys′ = move dir xs z ys)
    → LastIsNot blank xs
    → LastIsNot blank ys
    -------------------------------------------
    → LastIsNot blank xs′ × LastIsNot blank ys′
  lin-move left-dir {[]} {z} {[]} lin-xs lin-ys with z ≟ blank
  ... | yes _ = lin-nil , lin-nil
  ... | no z-neq-blank = lin-nil , lin-singleton z-neq-blank
  lin-move left-dir {[]} {z} {y ∷ ys} lin-xs lin-ys = lin-nil , lin-cons lin-ys
  lin-move left-dir {x ∷ xs} {z} {[]} lin-xs lin-ys with z ≟ blank
  lin-move left-dir {x ∷ .[]} {z} {[]} (lin-singleton x₁) lin-ys | yes _ =
    lin-nil , lin-nil
  lin-move left-dir {x ∷ .(_ ∷ _)} {z} {[]} (lin-cons lin-xs) lin-ys | yes _ =
    lin-xs , lin-nil
  lin-move left-dir {x ∷ .[]} {z} {[]} (lin-singleton x₁) lin-ys | no z-neq-blank =
    lin-nil , lin-singleton z-neq-blank
  lin-move left-dir {x ∷ .(_ ∷ _)} {z} {[]} (lin-cons lin-xs) lin-ys | no z-neq-blank =
    lin-xs , lin-singleton z-neq-blank
  lin-move left-dir {x ∷ []} {z} {y ∷ ys} (lin-singleton _) lin-ys =
    lin-nil , lin-cons lin-ys
  lin-move left-dir {x ∷ xs} {z} {y ∷ ys} (lin-cons lin-xs) lin-ys =
    lin-xs , lin-cons lin-ys
  lin-move right-dir {[]} {z} {[]} lin-xs lin-ys with z ≟ blank
  ... | yes _ = lin-nil , lin-nil
  ... | no z-neq-blank = lin-singleton z-neq-blank , lin-nil
  lin-move right-dir {x ∷ xs} {z} {[]} lin-xs lin-ys = lin-cons lin-xs , lin-nil
  lin-move right-dir {[]} {z} {y ∷ ys} lin-xs lin-ys with z ≟ blank
  lin-move right-dir {[]} {z} {y ∷ []} lin-xs (lin-singleton x₁) | yes _ =
    lin-nil , lin-nil
  lin-move right-dir {[]} {z} {y ∷ ys} lin-xs (lin-cons lin-ys) | yes _ =
    lin-nil , lin-ys
  lin-move right-dir {[]} {z} {y ∷ []} lin-xs (lin-singleton x) | no z-neq-blank =
    lin-singleton z-neq-blank , lin-nil
  lin-move right-dir {[]} {z} {y ∷ ys} lin-xs (lin-cons lin-ys) | no z-neq-blank =
    lin-singleton z-neq-blank , lin-ys
  lin-move right-dir {x ∷ xs} {z} {y ∷ .[]} lin-xs (lin-singleton _) =
    lin-cons lin-xs , lin-nil
  lin-move right-dir {x ∷ xs} {z} {y ∷ .(_ ∷ _)} lin-xs (lin-cons lin-ys) =
    lin-cons lin-xs , lin-ys

module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
  --| Turing machines over an alphabet A.
  record TM : Type₁ where
    field
      --| States.
      Q : Type₀
      {{isFinSetQ}} : isFinSet Q
      --| Symbols exclusively for the tape.
      S : Type₀
      {{isFinSetS}} : isFinSet S

    {-|
    The tape symbols (i.e. the input symbols plus the exclusively tape symbols).
    -}
    Γ : Type₀
    Γ = A ⊎ S

    Discrete-Γ : Discrete Γ
    Discrete-Γ = isFinSet→Discrete

    field
      --| Transition function.
      δ : Q → Γ → Maybe (Q × Γ × Dir)
      --| Initial state.
      init : Q
      --| Blank symbol.
      blank : S
      --| Accepting states.
      F : ℙ Q

    blank′ = ⊎.inr blank

    record Config : Type₀ where
      constructor config
      field
        --| Current state
        state : Q
        --| Symbols on the left of the head
        left : List Γ
        {-
        TODO: is this the best way to do it? We could consider:

        - Using HITs: would it make it more pleasant?
        - Ignoring this condition: would it be a good definition of
          configurations?
        -}
        {-|
        We don't store the blank symbols on the left of the left-most symbol of
        the tape (except if the head is on the left of that symbol).
        -}
        last-left-not-blank : LastIsNot (⊎.inr blank) left
        --| Symbol behind head
        head : Γ
        --| Symbols on the right of the head
        right : List Γ
        {-|
        We don't store the blank symbols on the right of the right-most symbol of
        the tape (except if the head is on the right of that symbol).
        -}
        last-right-not-blank : LastIsNot (⊎.inr blank) right

    data _⊢_ : Config → Config → Type₀ where
      step
        : ∀ {q p X X′ left right lin-left lin-right dir}
        → δ q X ≡ just (p , X′ , dir)
        → (let left′ , Y , right′ = move Discrete-Γ blank′ dir left X′ right )
        → (let lin-left′ , lin-right′ =
                 lin-move Discrete-Γ blank′ dir lin-left lin-right
          )
        → config q left  lin-left  X right  lin-right
        ⊢ config p left′ lin-left′ Y right′ lin-right′

    {-|
    Turing Machines can step from one configuration to another in only one
    way.
    -}
    isProp-⊢ : ∀ {C D} → isProp (C ⊢ D)
    isProp-⊢ = TODO

    {-|
    Given a 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 Turing Machine.

    The input is placed one cell at the right of the head. That means that the
    head is blank initially.
    -}
    lang : Lang A
    lang w =
      ∃[ p ∶ Q ]
      ∃[ l ∶ List Γ ] ∃[ lin-l ∶ LastIsNot blank′ l ]
      ∃[ h ∶ Γ ]
      ∃[ r ∶ List Γ ] ∃[ lin-r ∶ LastIsNot blank′ r ]
        F p ⊓
          ∥  config init [] lin-nil blank′ (list-map ⊎.inl w) lin-map-inl
          ⊢* config p    l  lin-l   h      r                  lin-r
          ∥ₚ

  {-
  Languages definable by Turing machines.
  -}
  TmLangs : ℙ (Lang A)
  TmLangs L = ∃[ M ∶ TM ] (TM.lang M ≡ L) , powersets-are-sets _ _