Turing Machines as Natural Transformations between Polynomial Functors

TM.agda

module TM where
open import Data.Integer

data V : Set where
    One Zero Empty : V

data HeadDir : Set where
    L R : HeadDir
 
-- An encoding of Polynomial Functors
record Poly : Set where
  constructor _▹_
  field
    pos : Set
    dir : pos -> Set
open Poly

-- morphisms of polynomails (natural transformation)
record Poly[_,_](p q : Poly) : Set where
    constructor _⇒ₚ_
    field
        onPos : pos p → pos q
        onDir : (i : pos p) → dir q (onPos i) → dir p i
open Poly[_,_]

-- Lense are just morphisms of monomials  
-- Syᵀ → Ayᴮ
Lens : Set → Set → Set → Set → Set
Lens S T A B = Poly[ S ▹ (λ _ →  T) , A ▹ (λ _ → B) ]

TuringMachine : Set
TuringMachine = Lens ((ℤ → V) × ℤ) ((ℤ → V) × ℤ) V ( V × HeadDir)

tm : TuringMachine
tm = (λ {(tape , head) → tape(head)}) ⇒ₚ λ{ (tape , head) ( v , L) → (tape [ head ⇒ v ]) , head - (+_ 1)
                                         ; (tape , head) ( v , R) → (tape [ head ⇒ v ]) , head + (+_ 1) }

-- Show that `tm` is a natural transformation between polynomial functors

-- this shows that `tm` also has the type Poly[ p , q] where p q are type Poly (representations of polynomial functors)
_ : Poly[ Σ (ℤ → V) (λ x → ℤ) ▹ (λ _ → Σ (ℤ → V) (λ x → ℤ)) , V ▹ (λ _ → Σ V (λ x → HeadDir)) ]
_ = tm

-- lets explicitly name the polynomials in the mapping
p : Poly
p =  Σ (ℤ → V) (λ x → ℤ)  ▹  (λ _ → Σ (ℤ → V) (λ x → ℤ))  

q : Poly
q =  V  ▹  (λ _ → Σ V (λ x → HeadDir)) 

-- therefore we can say that `tm` is a map between Poly(s)
_ : Poly[ p , q ]
_ = tm

-- Poly actually represents a Polynomial functor via the yoneda lemma
-- This shows that Poly represents a polynomial functor 
PFun : Poly → Functor Agda Agda 
PFun p = record { 
    F₀ = ⦅ p ⦆ ; 
    F₁ = lift p ; 
    identity = refl ; 
    homomorphism = λ f g → refl }

--where
-- "action" on objects
⦅_⦆ : Poly → Set → Set
⦅ P ▹ D ⦆ X = Σ[ p ∈ P ] (D p → X)

-- "action" on morphisms
lift : {X Y : Set} → (p : Poly) → (X → Y) → (⦅ p ⦆ X → ⦅ p ⦆ Y)
lift p f = λ{ (fst₁ , snd₁) → fst₁ , snd₁ ؛ f}

-- so lets denote p and q as their represented polynomial functors
pF : Functor Agda Agda
pF = PFun p

qF : Functor Agda Agda
qF  = PFun q

-- Poly[ p , q ]  represents a natural transformation between polynomial functors (again via yoneda lemma)
PNat : {p q : Poly } → Poly[ p , q ] → NatTrans (PFun p) (PFun q)
PNat (onPos ⇒ₚ onDir) = record { 
                            η = λ ob → λ{ (posp , dirp) → onPos posp , λ z → dirp (onDir posp z) } ; 
                            commute = λ {f (fst , snd) → refl }
                            }
                            
-- therefore we can say `tm` is a turing machine, but also a natural transformation between polynomial functors
_ : NatTrans pF qF  
_ = PNat tm    




-------- apendix -------
-- definition of Category
record Category : Set where
  field
    Ob : Set 
    _⇒_ : Rel Ob
    _≋_ : ∀{A B : Ob} → Rel (A ⇒ B) 
    _∘_  : ∀ {x y z : Ob} -> y ⇒ z -> x ⇒ y -> x ⇒ z
    id : ∀ {o : Ob} -> o ⇒ o
    idˡ : ∀ {x y : Ob} (f : x ⇒ y) -> f ∘ (id {x}) ≡ f
    idʳ : ∀ {x y : Ob} (f : x ⇒ y) -> (id {y}) ∘ f ≡ f
    ∘-assoc : ∀ {x y z w : Ob} (f : x ⇒ y) (g : y ⇒ z) (h : z ⇒ w) -> h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f

--definition of Functor
record Functor (𝒞 𝒟 : Category) : Set where
    private 
        module C = Category 𝒞
        module D = Category 𝒟
    field
        F₀ : C.Ob -> D.Ob
        F₁ : ∀ {A B} (f : C._⇒_ A B ) -> D._⇒_ (F₀ A) (F₀ B)

        identity : ∀ {A} -> (F₁ (C.id {A})) ≡ D.id {(F₀ A)}
        homomorphism : ∀ {A B C} -> (f : C._⇒_ A B) -> (g : C._⇒_ B C) ->
            F₁ (C._∘_ g f) ≡ D._∘_ (F₁ g) (F₁ f)

-- definition of Natural Transformation
record NatTrans {C D : Category } (ℱ 𝒢 : Functor C D) : Set where
    private
        module F = Functor ℱ
        module G = Functor 𝒢
    open F using (F₀ ; F₁)
    open Category C renaming (_⇒_ to _⇒C_)
    open Category D renaming (_⇒_ to _⇒D_; _∘_ to _∘D_; _≋_ to _≋D_)
    field
        η : ∀ X → F.F₀ X ⇒D G.F₀ X
        commute : ∀ {X Y}(f : X ⇒C Y) → ((η Y) ∘D (F₁ f)) ≋D (((G.F₁ f) ∘D η X))

-- Agda as a category
Agda : Category
Agda = record
        { Ob = Set
        ; _⇒_ = λ x y → (x → y)
        ; _≋_ = λ {A} → λ f g → ∀ (a : A) → f a ≡ g a
        ; _∘_ = _o_
        ; id = λ x → x
        ; idˡ = λ f → refl
        ; idʳ = λ f → refl
        ; ∘-assoc = λ f g h → refl 
        }