------------------------------------------------------------------------ -- This module proves that the recognisers correspond exactly to -- decidable predicates of type List Bool → Bool (when the alphabet is -- Bool) ------------------------------------------------------------------------ -- This result could be generalised to other finite alphabets. module TotalRecognisers.Simple.ExpressiveStrength where open import Coinduction open import Data.Bool open import Data.Bool.Properties open import Function open import Function.Equality using (_⟨\$⟩_) open import Function.Equivalence using (_⇔_; equivalence; module Equivalence) open import Data.List open import Data.Product open import Relation.Binary.PropositionalEquality open import Relation.Nullary.Decidable import TotalRecognisers.Simple open TotalRecognisers.Simple Bool _≟_ -- One direction of the correspondence has already been established: -- For every grammar there is an equivalent decidable predicate. grammar⇒pred : ∀ {n} (p : P n) → ∃ λ (f : List Bool → Bool) → ∀ s → s ∈ p ⇔ T (f s) grammar⇒pred p = ((λ s → ⌊ s ∈? p ⌋) , λ _ → equivalence fromWitness toWitness) -- For every decidable predicate there is a corresponding grammar. -- Note that these grammars are all "infinite LL(1)". pred⇒grammar : (f : List Bool → Bool) → ∃ λ (p : P (f [])) → ∀ s → s ∈ p ⇔ T (f s) pred⇒grammar f = (grammar f , λ s → equivalence (sound f) (complete f s)) where accept-if-true : ∀ b → P b accept-if-true true = empty accept-if-true false = fail grammar : (f : List Bool → Bool) → P (f []) grammar f = tok true · ♯ grammar (f ∘ _∷_ true ) ∣ tok false · ♯ grammar (f ∘ _∷_ false) ∣ accept-if-true (f []) accept-if-true-sound : ∀ b {s} → s ∈ accept-if-true b → s ≡ [] × T b accept-if-true-sound true empty = (refl , _) accept-if-true-sound false () accept-if-true-complete : ∀ {b} → T b → [] ∈ accept-if-true b accept-if-true-complete ok with Equivalence.to T-≡ ⟨\$⟩ ok ... | refl = empty sound : ∀ f {s} → s ∈ grammar f → T (f s) sound f (∣-right s∈) with accept-if-true-sound (f []) s∈ ... | (refl , ok) = ok sound f (∣-left (∣-left (tok · s∈))) = sound (f ∘ _∷_ true ) s∈ sound f (∣-left (∣-right (tok · s∈))) = sound (f ∘ _∷_ false) s∈ complete : ∀ f s → T (f s) → s ∈ grammar f complete f [] ok = ∣-right {n₁ = false} \$ accept-if-true-complete ok complete f (true ∷ bs) ok = ∣-left {n₁ = false} \$ ∣-left {n₁ = false} \$ tok · complete (f ∘ _∷_ true ) bs ok complete f (false ∷ bs) ok = ∣-left {n₁ = false} \$ ∣-right {n₁ = false} \$ tok · complete (f ∘ _∷_ false) bs ok