Simulation modular automata

ModularAutomata.agda

{-# OPTIONS --cubical #-}

module modularAutomata where

open import Data.Maybe
open import Cubical.Data.Prod
open import Cubical.Foundations.Everything

-- first, setup a type of infinite (coinductive) lists, we will need it later for simulation
record νList (A : Set) : Set where
  coinductive
  constructor _,_
  field
    head : A
    tail : Maybe (νList A)

-- next, define what we need from a queue to compute with it
-- we want to access its head and tail, and prepend must be
-- "inverse" to those.
-- we don't use the laws so far, but they would be nice to have
-- in a correctness proof I guess
record QueueType (Word : Set) : Set₁ where
  field
    Queue : Set
    -- operations
    prepend : Word → Word → Queue → Queue
    head : Queue → Word
    tail : Queue → Queue
    --laws
    head-prepend : ∀ a b q → head (prepend a b q) ≡ a
    head-tail-prepend : ∀ a b q → head (tail (prepend a b q)) ≡ b
    tail-tail-prepend : ∀ a b q → tail (tail (prepend a b q)) ≡ q

data LR : Set where
  L R : LR

module Automata (Word : Set) (QT : QueueType Word) where
  open QueueType QT

  State = Queue × Queue
  getLeft = proj₁
  getRight = proj₂

  -- group in a record for readability
  record ConfigurationResult : Set where
    constructor _∣_,_
    field
      side : LR
      first second : Word

  -- a configuration is a total function that maps two words
  -- to either nothing (a terminal state) or two words and a side
  -- to push them
  Configuration = Word → Word → Maybe ConfigurationResult

  -- helper to prepend a configuration result in front of a given state
  prepend-result : State → ConfigurationResult → State
  prepend-result state (L ∣ first , second) = prepend first second (getLeft state) , getRight state
  prepend-result state (R ∣ first , second) = getLeft state , prepend first second (getRight state)
  -- one step of the simulation. Evaluate the configuration at the heads, the prepend-result on the tail state
  simulateStep : Configuration → State → Maybe State
  simulateStep config state = Data.Maybe.map (prepend-result stateTail) (config firstLeft firstRight) where
    firstLeft = getLeft state .head
    firstRight = getRight state .head
    stateTail = getLeft state .tail , getRight state .tail
  -- full simulation. This just loops simulate step, gradually unfolding into a νList
  simulate : Configuration → State → νList State
  νList.head (simulate config state) = state
  νList.tail (simulate config state) with simulateStep config state
  ...                                | nothing = nothing
  ...                                | just nextStep = just (simulate config nextStep)

open import Data.Nat
open import Data.Fin using (Fin)
module FiniteAutomata (m : ℕ) = Automata (Fin m)

open import Cubical.Codata.Stream
open import Data.List

-- two possible queue types. Although StreamQueue is not used later on, it's
-- nice to show off. Since a stream can't be collapsed into a single value like List
-- it's not as nice to debug, though
StreamQueue : ∀ A → QueueType A
StreamQueue A = record
  { Queue = Stream A
  ; prepend = λ a b q → a , b , q
  ; head = Stream.head
  ; tail = Stream.tail
  ; head-prepend = λ a b q i → a
  ; head-tail-prepend = λ a b q i → b
  ; tail-tail-prepend = λ a b q i → q
  }
-- note that for a ListQueue you need to choose a default element that head returns
-- if the list is empty
ListQueue : ∀ A → A → QueueType A
ListQueue A zr = record
  { Queue = List A
  ; prepend = λ a b ls → a ∷ b ∷ ls
  ; head = λ { [] → zr ; (x ∷ xs) → x }
  ; tail = λ { [] → [] ; (x ∷ xs) → xs }
  ; head-prepend = λ a b q i → a
  ; head-tail-prepend = λ a b q i → b
  ; tail-tail-prepend = λ a b q i → q
  }

module Example where
  open import Data.Fin using (Fin; toℕ; #_)
  open import Data.Nat.DivMod
  -- if we have a configuration for some type A, and two functions (not necessarily an isomorphism) between A and B
  -- we can construct a configuration of type B
  remapConfig : ∀ {A B P Q} → (B → A) → (A → B) → Automata.Configuration A P → Automata.Configuration B Q
  remapConfig {A} {B} {P} {Q} f g configA a b = Data.Maybe.map mapResult (configA (f a) (f b)) where
    open Automata -- to get the constructor _∣_,_ in scope
    mapResult : Automata.ConfigurationResult A P → Automata.ConfigurationResult B Q
    mapResult (side ∣ first , second ) = (side ∣ g first , g second )
  -- takeLimit: get a potentially infinite list and take at most n elements from it
  takeLimit : ∀ {A} → (n : ℕ) → νList A → List A
  takeLimit zero vl = []
  takeLimit (suc x) vl with vl .νList.tail
  ...                  | nothing = vl .νList.head ∷ []
  ...                  | just tl = vl .νList.head ∷ takeLimit x tl

  -- for automata over lists over some finite field, we can display the state as simply integers
  module _ {m : ℕ} {d : Fin m} where
    open FiniteAutomata m (ListQueue _ d)
    collapseToℕ : ∀ {m} → List (Fin m) → ℕ
    collapseToℕ [] = 0
    collapseToℕ {m} (x ∷ xs)  = collapseToℕ xs * m + toℕ x
    humanizeState : State → ℕ × ℕ
    humanizeState (l , r) = collapseToℕ l , collapseToℕ r
    simulateStepSample : Configuration → State → Maybe (ℕ × ℕ)
    simulateStepSample config state = Data.Maybe.map humanizeState (simulateStep config state)
    simulateAndSample : Configuration → State → List (ℕ × ℕ)
    simulateAndSample config state = Data.List.map humanizeState (takeLimit 10 (simulate config state))

  -- now, let's finally construct our example
  open FiniteAutomata 5 (ListQueue _ (# zero))
    hiding (_∣_,_) -- hide this, we will remap the configuration from ℕ

  pattern one = suc 0
  pattern two = suc (suc 0)
  pattern four = suc (suc (suc (suc 0)))
  testConfig : Configuration
  testConfig = remapConfig toℕ (_mod 5) config where
    open Automata
    config : Automata.Configuration ℕ (ListQueue ℕ zero)
    config zero zero = just (R ∣ 2 , zero )
    config two two = just (L ∣ 4 , zero )
    config four one = just (R ∣ zero , zero )
    config x y = nothing

  testState : State
  testState = # 2 ∷ # 2 ∷ [] , # 2 ∷ # 1 ∷ []
  stepTest : _
  stepTest = simulateStepSample testConfig testState
  test : _
  test = simulateAndSample testConfig testState

  testResult : test ≡ (12 , 7) ∷ (54 , 1) ∷ (10 , 0) ∷ (2 , 2) ∷ (4 , 0) ∷ []
  testResult = refl