DFAs in agda

dfa.agda

open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)

--- Preamble: this is probably in the standard library -------------------------

-- Finite sets

data Fin : ℕ → Set where
  fzero : ∀{n} → Fin (suc n)
  fsuc  : ∀{n} → Fin n → Fin (suc n)

-- Some computable functions for lists of finite numbers

_==f_ : ∀{n m} → Fin n → Fin m → Bool
fzero  ==f fzero  = true
fsuc x ==f fsuc y = x ==f y
_      ==f _      = false

_∈f_ : ∀{n m} → Fin n → List (Fin m) → Bool
y ∈f [] = false
y ∈f (x ∷ xs) with y ==f x
...           | false = y ∈f xs
...           | true  = true

_∷f_ : ∀{n} → Fin n → List (Fin n) → List (Fin n)
x ∷f xs with x ∈f xs
...     | false = x ∷ xs
...     | true  = xs

_++f_ : ∀{n} → List (Fin n) → List (Fin n) → List (Fin n)
[] ++f ys = ys
(x ∷ xs) ++f ys = x ∷f (xs ++f ys)

∪f : ∀{n} → List (List (Fin n)) → List (Fin n)
∪f [] = []
∪f (x ∷ xs) = x ++f ∪f xs


-- Syntax sugar

fone : ∀{n}   → Fin (suc (suc n))
ftwo : ∀{n}   → Fin (suc (suc (suc n)))
fthree : ∀{n} → Fin (suc (suc (suc (suc n))))
ffour : ∀{n}  → Fin (suc (suc (suc (suc (suc n)))))
ffive : ∀{n}  → Fin (suc (suc (suc (suc (suc (suc n))))))
fone   = fsuc fzero
ftwo   = fsuc fone
fthree = fsuc ftwo
ffour  = fsuc fthree
ffive  = fsuc ffour


-- Function tools

map : {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

any : {A : Set} → (A → Bool) → List A → Bool
any f [] = false
any f (x ∷ xs) with f x
...            | false = any f xs
...            | true  = true


data ε∣ (A : Set) : Set where
  ∣ε∣ : ε∣ A
  ∣_∣ : A → ε∣ A


-- End of preamble -------------------------------------------------------------

record DFA (Σ : Set)(n : ℕ) : Set where
  constructor dfa
  field
    finals     : List (Fin n)
    transition : Fin n → Σ → Fin n

  transitions : Fin n → List Σ → Fin n
  transitions n []       = n
  transitions n (x ∷ xs) = transitions (transition n x) xs

-- Can't pattern-match on n inside the record module, sadly
accepts : ∀{A n} → DFA A n → List A → Bool
accepts {n = zero}  aut xs = false
accepts {n = suc n} aut xs = DFA.transitions aut fzero xs ∈f DFA.finals aut


record NFA (Σ : Set)(n : ℕ) : Set where
  constructor nfa
  field
    finals     : List (Fin n)
    transition : Fin n → ε∣ Σ → List (Fin n)

  transitions : Fin n → List (ε∣ Σ) → List (Fin n)
  transitions n []       = n ∷ []
  transitions n (x ∷ xs) = ∪f (map closure (transition n x))
                           where closure = λ m → transitions m xs

ndaccepts : ∀{Σ n} → NFA Σ n → List Σ → Bool
ndaccepts {n = zero}  aut xs = false
ndaccepts {n = suc n} aut xs = any isfinal (NFA.transitions aut fzero ∣xs∣)
                               where isfinal = λ s → s ∈f NFA.finals aut
                                     ∣xs∣ = map ∣_∣ xs

--- Examples
open import Agda.Builtin.Equality

data Alphabeta : Set where
  α β : Alphabeta

endswithβ : NFA Alphabeta 2
NFA.finals endswithβ = fone ∷ []
NFA.transition endswithβ fzero            ∣ε∣   = []
NFA.transition endswithβ fzero            ∣ α ∣ = fzero ∷ []
NFA.transition endswithβ fzero            ∣ β ∣ = fzero ∷ fone ∷ []
NFA.transition endswithβ (fsuc fzero)     ∣ε∣   = []
NFA.transition endswithβ (fsuc fzero)     ∣ α ∣ = []
NFA.transition endswithβ (fsuc fzero)     ∣ β ∣ = []
NFA.transition endswithβ (fsuc (fsuc ()))

endswithβpf : ndaccepts endswithβ (α ∷ β ∷ []) ≡ true
endswithβpf = refl