blob: d9be456c34d3419629f6b32fd234dd5e897fe56a (
plain)
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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary using (REL; Setoid; _⟶_Respects_)
module Cfe.Language.Base
{c ℓ} (over : Setoid c ℓ)
where
open Setoid over using () renaming (Carrier to C)
open import Cfe.Function.Power
open import Data.Empty.Polymorphic using (⊥)
open import Data.List
open import Data.List.Relation.Binary.Equality.Setoid over
open import Data.Product
open import Data.Sum
open import Function
open import Level
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary using (Dec; ¬_)
private
variable
a b : Level
------------------------------------------------------------------------
-- Definition
record Language a : Set (c ⊔ ℓ ⊔ suc a) where
field
𝕃 : List C → Set a
∈-resp-≋ : 𝕃 ⟶ 𝕃 Respects _≋_
------------------------------------------------------------------------
-- Special Languages
∅ : Language a
∅ = record
{ 𝕃 = const ⊥
; ∈-resp-≋ = λ _ ()
}
｛ε｝ : Language (c ⊔ a)
｛ε｝ {a} = record
{ 𝕃 = Lift a ∘ ([] ≡_)
; ∈-resp-≋ = λ { [] → id }
}
｛_｝ : C → Language _
｛ c ｝ = record
{ 𝕃 = [ c ] ≋_
; ∈-resp-≋ = λ l₁≋l₂ l₁∈｛c｝ → ≋-trans l₁∈｛c｝ l₁≋l₂
}
------------------------------------------------------------------------
-- Membership
infix 4 _∈_ _∉_
_∈_ : List C → Language a → Set _
_∈_ = flip Language.𝕃
_∉_ : List C → Language a → Set _
w ∉ A = ¬ w ∈ A
------------------------------------------------------------------------
-- Language Combinators
infix 8 ⋃_
infix 7 _∙_
infix 6 _∪_
_∙_ : Language a → Language b → Language _
A ∙ B = record
{ 𝕃 = λ w → ∃₂ λ w₁ w₂ → w₁ ∈ A × w₂ ∈ B × w₁ ++ w₂ ≋ w
; ∈-resp-≋ = λ w≋w′ (_ , _ , w₁∈A , w₂∈B , eq) → -, -, w₁∈A , w₂∈B , ≋-trans eq w≋w′
}
_∪_ : Language a → Language b → Language _
A ∪ B = record
{ 𝕃 = λ w → w ∈ A ⊎ w ∈ B
; ∈-resp-≋ = uncurry Data.Sum.map ∘ < Language.∈-resp-≋ A , Language.∈-resp-≋ B >
}
Sup : (Language a → Language a) → Language a → Language _
Sup F A = record
{ 𝕃 = λ w → ∃[ n ] w ∈ (F ^ n) A
; ∈-resp-≋ = λ w≋w′ (n , w∈FⁿA) → n , Language.∈-resp-≋ ((F ^ n) A) w≋w′ w∈FⁿA
}
⋃_ : (Language a → Language a) → Language _
⋃ F = Sup F ∅
------------------------------------------------------------------------
-- Relations
infix 4 _⊆_ _≈_
data _⊆_ {a b} : REL (Language a) (Language b) (c ⊔ ℓ ⊔ suc (a ⊔ b)) where
sub : ∀ {A : Language a} {B : Language b} → (∀ {w} → w ∈ A → w ∈ B) → A ⊆ B
_⊇_ : REL (Language a) (Language b) _
_⊇_ = flip _⊆_
_≈_ : REL (Language a) (Language b) _
A ≈ B = A ⊆ B × B ⊆ A
_≉_ : REL (Language a) (Language b) _
A ≉ B = ¬ A ≈ B
------------------------------------------------------------------------
-- Membership Properties
-- Contains empty string
Null : ∀ {a} → Language a → Set a
Null A = [] ∈ A
-- Characters that start strings
First : ∀ {a} → Language a → C → Set (c ⊔ a)
First A c = ∃[ w ] c ∷ w ∈ A
-- Characters that can follow a string to make another string in the language
Flast : ∀ {a} → Language a → C → Set (c ⊔ a)
Flast A c = ∃₂ λ c′ w → (c′ ∷ w ∈ A × ∃[ w′ ] c′ ∷ w ++ c ∷ w′ ∈ A)
------------------------------------------------------------------------
-- Proof Properties
-- Membership is decidable
Decidable : Language a → Set _
Decidable A = ∀ w → Dec (w ∈ A)
-- Membership proofs are irrelevant
Irrelevant : Language a → Set _
Irrelevant A = ∀ {w} → (p q : w ∈ A) → p ≡ q
-- Membership proofs are recomputable
Recomputable : Language a → Set _
Recomputable A = ∀ {w} → .(w ∈ A) → w ∈ A
|
