1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary
module Cfe.Language.Base
{c ℓ} (setoid : Setoid c ℓ)
where
open Setoid setoid renaming (Carrier to A)
open import Data.Empty
open import Data.List
open import Data.List.Relation.Binary.Equality.Setoid setoid
open import Data.Product as Product
open import Function
open import Level
import Relation.Binary.PropositionalEquality as ≡
import Relation.Binary.Indexed.Heterogeneous as I
record IsLanguage {a aℓ} (𝕃 : List A → Set a) (_≈ᴸ_ : ∀ {l} → Rel (𝕃 l) aℓ) (⤖ : ∀ {l₁ l₂} → l₁ ≋ l₂ → 𝕃 l₁ → 𝕃 l₂) : Set (c ⊔ ℓ ⊔ a ⊔ aℓ) where
field
≈ᴸ-isEquivalence : ∀ {l} → IsEquivalence (_≈ᴸ_ {l})
⤖-cong : ∀ {l₁ l₂ l₁≋l₂} → (⤖ l₁≋l₂) Preserves _≈ᴸ_ {l₁} ⟶ _≈ᴸ_ {l₂}
⤖-bijective : ∀ {l₁ l₂ l₁≋l₂} → Bijective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ l₁≋l₂)
⤖-refl : ∀ {l l∈𝕃} → (⤖ {l} ≋-refl l∈𝕃) ≈ᴸ l∈𝕃
⤖-sym : ∀ {l₁ l₂ l₁∈𝕃 l₂∈𝕃 l₁≋l₂}
→ (⤖ {l₁} l₁≋l₂ l₁∈𝕃) ≈ᴸ l₂∈𝕃
→ (⤖ {l₂} (≋-sym l₁≋l₂) l₂∈𝕃) ≈ᴸ l₁∈𝕃
⤖-trans : ∀ {l₁ l₂ l₃ l₁∈𝕃 l₂∈𝕃 l₃∈𝕃 l₁≋l₂ l₂≋l₃}
→ (⤖ {l₁} l₁≋l₂ l₁∈𝕃) ≈ᴸ l₂∈𝕃
→ (⤖ {l₂} l₂≋l₃ l₂∈𝕃) ≈ᴸ l₃∈𝕃
→ (⤖ {_} {l₃} (≋-trans l₁≋l₂ l₂≋l₃) l₁∈𝕃) ≈ᴸ l₃∈𝕃
≈ᴸ-refl : ∀ {l} → Reflexive (_≈ᴸ_ {l})
≈ᴸ-refl = IsEquivalence.refl ≈ᴸ-isEquivalence
≈ᴸ-sym : ∀ {l} → Symmetric (_≈ᴸ_ {l})
≈ᴸ-sym = IsEquivalence.sym ≈ᴸ-isEquivalence
≈ᴸ-trans : ∀ {l} → Transitive (_≈ᴸ_ {l})
≈ᴸ-trans = IsEquivalence.trans ≈ᴸ-isEquivalence
≈ᴸ-reflexive : ∀ {l} → ≡._≡_ ⇒ (_≈ᴸ_ {l})
≈ᴸ-reflexive = IsEquivalence.reflexive ≈ᴸ-isEquivalence
⤖-injective : ∀ {l₁ l₂ l₁≋l₂} → Injective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ l₁≋l₂)
⤖-injective = proj₁ ⤖-bijective
⤖-surjective : ∀ {l₁ l₂ l₁≋l₂} → Surjective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ {l₁} l₁≋l₂)
⤖-surjective = proj₂ ⤖-bijective
⤖-isIndexedEquivalence : I.IsIndexedEquivalence 𝕃 (λ l₁∈𝕃 l₂∈𝕃 → ∃[ l₁≋l₂ ] ((⤖ l₁≋l₂ l₁∈𝕃) ≈ᴸ l₂∈𝕃))
⤖-isIndexedEquivalence = record
{ refl = ≋-refl , ⤖-refl
; sym = Product.map ≋-sym ⤖-sym
; trans = Product.zip ≋-trans ⤖-trans
}
⤖-reflexive : ∀ {l l∈𝕃 l∈𝕃′} → l∈𝕃 ≡.≡ l∈𝕃′ → ∃[ l≋l ]((⤖ {l} l≋l l∈𝕃) ≈ᴸ l∈𝕃′)
⤖-reflexive = I.IsIndexedEquivalence.reflexive ⤖-isIndexedEquivalence
record Language a aℓ : Set (c ⊔ ℓ ⊔ suc (a ⊔ aℓ)) where
infix 4 _≈ᴸ_
field
𝕃 : List A → Set a
_≈ᴸ_ : ∀ {l} → Rel (𝕃 l) aℓ
⤖ : ∀ {l₁ l₂} → l₁ ≋ l₂ → 𝕃 l₁ → 𝕃 l₂
isLanguage : IsLanguage 𝕃 _≈ᴸ_ ⤖
open IsLanguage isLanguage public
open Language
infix 4 _∈_
_∈_ : ∀ {a aℓ} → List A → Language a aℓ → Set a
l ∈ A = 𝕃 A l
∅ : Language 0ℓ 0ℓ
∅ = record
{ 𝕃 = const ⊥
; _≈ᴸ_ = ≡._≡_
; ⤖ = const id
; isLanguage = record
{ ≈ᴸ-isEquivalence = ≡.isEquivalence
; ⤖-cong = ≡.cong id
; ⤖-bijective = (λ {x} → ⊥-elim x) , (λ ())
; ⤖-refl = λ {_} {l∈𝕃} → ⊥-elim l∈𝕃
; ⤖-sym = λ {_} {_} {l₁∈𝕃} → ⊥-elim l₁∈𝕃
; ⤖-trans = λ {_} {_} {_} {l₁∈𝕃} → ⊥-elim l₁∈𝕃
}
}
⦃ε⦄ : Language (c ⊔ ℓ) (c ⊔ ℓ)
⦃ε⦄ = record
{ 𝕃 = [] ≋_
; _≈ᴸ_ = ≡._≡_
; ⤖ = flip ≋-trans
; isLanguage = record
{ ≈ᴸ-isEquivalence = ≡.isEquivalence
; ⤖-cong = λ {_} {_} {l₁≋l₂} → ≡.cong (flip ≋-trans l₁≋l₂)
; ⤖-bijective = λ {_} {_} {l₁≋l₂} →
( (λ {x} {y} x≡y → case x , y return (λ (x , y) → x ≡.≡ y) of λ { ([] , []) → ≡.refl })
, (λ { [] → (case l₁≋l₂ return (λ x → ∃[ y ](≋-trans y x ≡.≡ [])) of λ { [] → [] , ≡.refl})}))
; ⤖-refl = λ {_} {[]≋l} → case []≋l return (λ []≋l → ≋-trans []≋l ≋-refl ≡.≡ []≋l) of λ {[] → ≡.refl}
; ⤖-sym = λ {_} {_} {[]≋l₁} {[]≋l₂} {l₁≋l₂} _ →
case []≋l₁ , []≋l₂ , l₁≋l₂
return (λ ([]≋l₁ , []≋l₂ , l₁≋l₂) → ≋-trans []≋l₂ (≋-sym l₁≋l₂) ≡.≡ []≋l₁)
of λ { ([] , [] , []) → ≡.refl }
; ⤖-trans = λ {_} {_} {_} {[]≋l₁} {[]≋l₂} {[]≋l₃} {l₁≋l₂} {l₂≋l₃} _ _ →
case []≋l₁ , []≋l₂ , []≋l₃ , l₁≋l₂ , l₂≋l₃
return (λ ([]≋l₁ , []≋l₂ , []≋l₃ , l₁≋l₂ , l₂≋l₃) → ≋-trans []≋l₁ (≋-trans l₁≋l₂ l₂≋l₃) ≡.≡ []≋l₃)
of λ { ([] , [] , [] , [] , []) → ≡.refl }
}
}
_≤_ : {a aℓ b bℓ : Level} → REL (Language a aℓ) (Language b bℓ) (c ⊔ a ⊔ b)
A ≤ B = ∀ {l} → l ∈ A → l ∈ B
|
