-- Andreas Abel -- Formal languages, coinductively formalized in Agda -- -- 2017-01-31 Types meeting Ljubljana -- Abstract: -- Formal languages can be represented in Type Theory as infinite -- tries. Using Agdas copatterns and coinduction mechanism, we can -- define constructions on formal languages elegantly by their -- Brzozowski derivatives, and reason about them using equation -- chains. module _ where -- Wellfounded coinduction open import Size open import Data.Bool open import Relation.Binary open import Relation.Binary.PropositionalEquality import Relation.Binary.EqReasoning as EqR module Coinduction (A : Set) where infixl 4 _∪_ infixl 6 _∙_ infixr 15 _* -- Languages as coinductive type: infinite trie record Lang (i : Size) : Set where coinductive field ν : Bool δ : ∀{j : Size< i} → A → Lang j open Lang -- Some language constructions -- Empty language ∅ : ∀{i} → Lang i ∅ = {!!} -- Language of the empty word ε : ∀{i} → Lang i ε = {!!} -- Language union _∪_ : ∀{i} (k l : Lang i) → Lang i k ∪ l = {!!} -- Language concatenation -- k ∙ l = { uv | u ∈ k and v ∈ l } _∙_ : ∀{i} (k l : Lang i) → Lang i k ∙ l = {!!} -- Making sizes explicit for didactic purposes: module ExplainSizes where union : ∀ i (k l : Lang i) → Lang i ν (union i k l) = ν k ∨ ν l δ (union i k l) {j} x = union j (δ k x) (δ l {j} x) concat : ∀ i (k l : Lang i) → Lang i ν (concat i k l) = ν k ∧ ν l δ (concat i k l) {j} x = if ν k then union j (concat j (δ k {j} x) l) (δ l {j} x) else concat j (δ k {j} x) l -- Language iteration (Kleene star) _* : ∀{i} (l : Lang i) → Lang i ν (l *) = true δ (l *) x = δ l x ∙ (l *) -- The following definition is invalid and rejected by Agda module Illegal where -- _∗ : ∀{i} (l : Lang i) → Lang i -- ν (l ∗) = true -- δ (l ∗) x = δ (l ∗) x ∙ l -- Language equality (bisimilarity) infix 1 _≅⟨_⟩≅_ record _≅⟨_⟩≅_ (k : Lang ∞) (i : Size) (l : Lang ∞) : Set where coinductive field ≅ν : ν k ≡ ν l ≅δ : ∀{j : Size< i} (a : A) → δ k a ≅⟨ j ⟩≅ δ l a open _≅⟨_⟩≅_ -- Equivalence laws -- Reflexivity ≅refl : ∀{i} {l : Lang ∞} → l ≅⟨ i ⟩≅ l ≅refl = {!!} -- Symmetry ≅sym : ∀{i} {k l : Lang ∞} (p : k ≅⟨ i ⟩≅ l) → l ≅⟨ i ⟩≅ k ≅sym p = {!!} -- Transitivity ≅trans : ∀{i} {k l m : Lang ∞} (p : k ≅⟨ i ⟩≅ l) (q : l ≅⟨ i ⟩≅ m) → k ≅⟨ i ⟩≅ m ≅trans p q = {!!} -- Languages form a setoid under bisimilarity ≅isEquivalence : (i : Size) → IsEquivalence _≅⟨ i ⟩≅_ IsEquivalence.refl (≅isEquivalence i) = ≅refl IsEquivalence.sym (≅isEquivalence i) = ≅sym IsEquivalence.trans (≅isEquivalence i) = ≅trans Bis : ∀(i : Size) → Setoid _ _ Setoid.Carrier (Bis i) = Lang ∞ Setoid._≈_ (Bis i) = _≅⟨ i ⟩≅_ Setoid.isEquivalence (Bis i) = ≅isEquivalence i {- -- Language laws of the language unions -- A congruence law: union-congˡ : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → l ∪ m ≅⟨ i ⟩≅ k ∪ m ≅ν (union-congˡ p) rewrite ≅ν p = refl ≅δ (union-congˡ p) a = union-congˡ (≅δ p a) -- More laws of the union postulate union-assoc : ∀{i} (k {l m} : Lang ∞) → (k ∪ l) ∪ m ≅⟨ i ⟩≅ k ∪ (l ∪ m) union-union-distr : ∀{i} (k {l m} : Lang ∞) → (k ∪ l) ∪ m ≅⟨ i ⟩≅ (k ∪ m) ∪ (l ∪ m) union-swap23 : ∀{i} (k {l m} : Lang ∞) → (k ∪ l) ∪ m ≅⟨ i ⟩≅ (k ∪ m) ∪ l union-swap24 : ∀{i} {k l m n : Lang ∞} → (k ∪ l) ∪ (m ∪ n) ≅⟨ i ⟩≅ (k ∪ m) ∪ (l ∪ n) -- An interesting proof: -- Concatenation distributes over unions (from the left). concat-union-distribʳ : ∀{i} (k {l m} : Lang ∞) → k ∙ (l ∪ m) ≅⟨ i ⟩≅ (k ∙ l) ∪ (k ∙ m) ≅ν (concat-union-distribʳ k) = {!!} -- ∧-∨-distribˡ (ν k) _ _ ≅δ (concat-union-distribʳ k) a with ν k ≅δ (concat-union-distribʳ k {l} {m}) a | true = begin δ k a ∙ (l ∪ m) ∪ (δ l a ∪ δ m a) ≈⟨ union-congˡ (concat-union-distribʳ (δ k a)) ⟩ (δ k a ∙ l ∪ δ k a ∙ m) ∪ (δ l a ∪ δ m a) ≈⟨ union-swap24 ⟩ (δ k a ∙ l ∪ δ l a) ∪ (δ k a ∙ m ∪ δ m a) ∎ where open EqR (Bis _) ≅δ (concat-union-distribʳ k) a | false = concat-union-distribʳ (δ k a) -- -} -- -} -- -} -- -} -- -} -- -}