RIS.systems: affine systems of equations
Set Implicit Arguments.
Require Import Recdef.
Require Import Bool.
Require Import tools algebra language regexp automata completenessKA.
Require Import Recdef.
Require Import Bool.
Require Import tools algebra language regexp automata completenessKA.
We fix a decidable set of variables.
We fix a set X equipped with the operations of Kleene
algebra. We do not however assume any axioms.
An affine system with variables of type Q and values of type
X is a finite set of inequations either of the shape x≤q or
x·q≤q'.
Definition cst_leq : Set := X × Q.
Definition var_leq : Set := X × Q × Q.
Definition system : Set := list cst_leq × list var_leq.
Definition var_leq : Set := X × Q × Q.
Definition system : Set := list cst_leq × list var_leq.
We may extract the set of variables appearing in a system.
Definition vars_system : system → list Q :=
fun S ⇒ (map snd (fst S))++(flat_map (fun e ⇒ [snd(fst e);snd e]) (snd S)).
fun S ⇒ (map snd (fst S))++(flat_map (fun e ⇒ [snd(fst e);snd e]) (snd S)).
We define the size of a system to be its number of variables.
A vector is a map from variables to values.
If V is a vector, S a system and q a variable, we may
compute an expression representing the constraints on q: we
take the union x1 ∪ ... ∪ xn ∪ x'1 · q1 ∪ x'k · qk, where the
inequations in S with q on the right hand side are xi≤q
and x'i·qi≤q.
Definition ExprVar (V : vector) (S : system) (x : Q) :=
(Σ (flat_map (fun L ⇒ if (snd L) =?= x then [fst L] else []) (fst S)))
∪ (Σ (flat_map (fun L ⇒ if (snd L) =?= x then [fst (fst L)·V (snd (fst L))] else []) (snd S))).
(Σ (flat_map (fun L ⇒ if (snd L) =?= x then [fst L] else []) (fst S)))
∪ (Σ (flat_map (fun L ⇒ if (snd L) =?= x then [fst (fst L)·V (snd (fst L))] else []) (snd S))).
A vector E is an exact solution of S with respect to some
relation =X if for every variable in the system we have
E(q) =X ExprVar E S q.
Definition exact_solution (eqX : relation X) (S : system) (E : Q → X) : Prop :=
(∀ q, q ∈ vars_system S → eqX (E q) (ExprVar E S q)).
(∀ q, q ∈ vars_system S → eqX (E q) (ExprVar E S q)).
It is a weak solution with respect to a relation ≤X if for
every contraint is satisfied, meaning that:
- if x≤q then x ≤X E q
- if x·q≤q' then x·(E q) ≤X (E q').
Definition weak_solution (leqX : relation X) (S : system) (E : Q → X) : Prop :=
(∀ e q, (e,q) ∈ (fst S) → leqX e (E q))
∧ (∀ p e q, (e,p,q) ∈ (snd S) → leqX (e · E p) (E q)).
(∀ e q, (e,q) ∈ (fst S) → leqX e (E q))
∧ (∀ p e q, (e,p,q) ∈ (snd S) → leqX (e · E p) (E q)).
A vector is a lower bound (of the solutions) if it is is
pointwise smaller than every weak solution.
Definition lower_bound leqX S E : Prop :=
(∀ F, weak_solution leqX S F → ∀ q, q ∈ vars_system S → leqX (E q) (F q)).
(∀ F, weak_solution leqX S F → ∀ q, q ∈ vars_system S → leqX (E q) (F q)).
The least solution is a weak solution that is a lower bound.
cst S q is the sum of constants xi such that xi≤q is in S.
Definition cst (M : system) q := Σ (flat_map (fun C ⇒ if (snd C =?= q) then [fst C] else []) (fst M)).
loop S q is the sum of constants xi such that xi·q≤q is in S.
Definition loop (M : system) q := Σ (flat_map (fun C ⇒ if (snd C =?= q) && (snd(fst C)=?=q)
then [fst (fst C)] else []) (snd M)).
then [fst (fst C)] else []) (snd M)).
succ S q is the list of pairs (x,p) such that p≠q and x·p≤q is in S.
Definition succ (M : system) q := (flat_map (fun C ⇒ if (snd C =?= q) && negb (snd(fst C)=?=q)
then [(fst (fst C),snd (fst C))] else [])
(snd M)).
then [(fst (fst C),snd (fst C))] else [])
(snd M)).
elim_var M q yields a system that is equivalent to M except
that q does not appear in it. It is obtained by removing all
the constraints involving q, and adding
- x · (loop M q)⋆ ·(cst M q) ≤ p for every x·q≤p in the system;
- x · (loop M q)⋆ · y · p' ≤ p for every x·q≤p and every y,p' in succ M q.
Definition elim_var (M : system) q : system :=
(((fun C ⇒ negb (snd C =?= q)) :> fst M)
++ (flat_map (fun C ⇒ if (negb (snd C =?= q)) && (snd(fst C)=?=q)
then [(fst(fst C) · (loop M q) ⋆ · (cst M q),snd C)]
else [])
(snd M)),
(flat_map (fun C ⇒ if (negb (snd C =?= q))
then
if (snd(fst C)=?=q)
then
map (fun C' ⇒ (fst(fst C) · (loop M q) ⋆ · fst C',snd C',snd C)) (succ M q)
else [C]
else [])
(snd M))).
(((fun C ⇒ negb (snd C =?= q)) :> fst M)
++ (flat_map (fun C ⇒ if (negb (snd C =?= q)) && (snd(fst C)=?=q)
then [(fst(fst C) · (loop M q) ⋆ · (cst M q),snd C)]
else [])
(snd M)),
(flat_map (fun C ⇒ if (negb (snd C =?= q))
then
if (snd(fst C)=?=q)
then
map (fun C' ⇒ (fst(fst C) · (loop M q) ⋆ · fst C',snd C',snd C)) (succ M q)
else [C]
else [])
(snd M))).
We compute a vector solution_sys n M by iterating
elim_var. n is a natural number used to ensure
termination. To get the correct result, n should be greater
than the size of the system.
Fixpoint solution_sys n (M : system) : (Q → X) :=
match n with
| 0 ⇒ (fun _ ⇒ zero)
| S n ⇒
match {{vars_system M}} with
| [] ⇒ (fun _ ⇒ zero)
| q::_ ⇒
let E := solution_sys n (elim_var M q) in
(fun p ⇒ if p =?= q
then (loop M q) ⋆ · (cst M q ∪ Σ (map (fun C ⇒ (fst C · E (snd C))) (succ M q)))
else E p)
end
end.
Section solutions.
match n with
| 0 ⇒ (fun _ ⇒ zero)
| S n ⇒
match {{vars_system M}} with
| [] ⇒ (fun _ ⇒ zero)
| q::_ ⇒
let E := solution_sys n (elim_var M q) in
(fun p ⇒ if p =?= q
then (loop M q) ⋆ · (cst M q ∪ Σ (map (fun C ⇒ (fst C · E (snd C))) (succ M q)))
else E p)
end
end.
Section solutions.
We temporarily fix an equivalence relation ⩵ and a partial
order ≦, and assume they provide a Kleene algebra
structure to the set X.
Context {eqX leqX : relation X}.
Context {equivX : @Equivalence X eqX} {preX : @PreOrder X leqX}.
Context {poX : @PartialOrder X eqX equivX leqX preX}.
Context {kaX : @KleeneAlgebra X eqX leqX jX pX zX uX sX}.
Infix " ≦ " := leqX (at level 80).
Infix " ⩵ " := eqX (at level 80).
Context {equivX : @Equivalence X eqX} {preX : @PreOrder X leqX}.
Context {poX : @PartialOrder X eqX equivX leqX preX}.
Context {kaX : @KleeneAlgebra X eqX leqX jX pX zX uX sX}.
Infix " ≦ " := leqX (at level 80).
Infix " ⩵ " := eqX (at level 80).
An exact solution is in particular a weak one.
Equivalent vectors yield equivalent ExprVar.
Lemma ExprVar_ext E F S q :
(∀ p, p ∈ vars_system S → E p ⩵ F p) → ExprVar E S q ⩵ ExprVar F S q.
Lemma weak_solution_ext E F S :
(∀ p, p ∈ vars_system S → E p ⩵ F p) → weak_solution leqX S E ↔ weak_solution leqX S F.
Lemma exact_solution_ext E F S :
(∀ p, p ∈ vars_system S → E p ⩵ F p) → exact_solution eqX S E ↔ exact_solution eqX S F.
Lemma lower_bound_ext E F S :
(∀ p, p ∈ vars_system S → E p ⩵ F p) → lower_bound leqX S E ↔ lower_bound leqX S F.
Lemma least_solution_ext E F S :
(∀ p, p ∈ vars_system S → E p ⩵ F p) →
least_solution leqX S E ↔ least_solution leqX S F.
(∀ p, p ∈ vars_system S → E p ⩵ F p) → ExprVar E S q ⩵ ExprVar F S q.
Lemma weak_solution_ext E F S :
(∀ p, p ∈ vars_system S → E p ⩵ F p) → weak_solution leqX S E ↔ weak_solution leqX S F.
Lemma exact_solution_ext E F S :
(∀ p, p ∈ vars_system S → E p ⩵ F p) → exact_solution eqX S E ↔ exact_solution eqX S F.
Lemma lower_bound_ext E F S :
(∀ p, p ∈ vars_system S → E p ⩵ F p) → lower_bound leqX S E ↔ lower_bound leqX S F.
Lemma least_solution_ext E F S :
(∀ p, p ∈ vars_system S → E p ⩵ F p) →
least_solution leqX S E ↔ least_solution leqX S F.
The zero vector is always a lower bound.
It's also the least solution of any system devoid of variables.
Eliminating variables eliminates variables.
The vector solution_sys n M is uniformly zero on variables
that do not appear in the system.
For any weak solution F the following inequalities hold.
Lemma loop_spec M F q : weak_solution leqX M F → loop M q ⋆ · F q ≦ F q.
Lemma cst_spec M F q : weak_solution leqX M F → cst M q ≦ F q.
Lemma succ_spec M F q : weak_solution leqX M F → ∀ e p, (e,p) ∈ succ M q → e · F p ≦ F q.
Lemma cst_spec M F q : weak_solution leqX M F → cst M q ≦ F q.
Lemma succ_spec M F q : weak_solution leqX M F → ∀ e p, (e,p) ∈ succ M q → e · F p ≦ F q.
Eliminating variables preserves weak solutions.
If the parameter n is big enough, solution_sys n S is an
exact solution and a lower bound of the system S.
Theorem solution_sys_spec S n :
sizeSys S ≤ n →
exact_solution eqX S (solution_sys n S)
∧ lower_bound leqX S (solution_sys n S).
sizeSys S ≤ n →
exact_solution eqX S (solution_sys n S)
∧ lower_bound leqX S (solution_sys n S).
Every least solution is in fact an exact solution.
Lemma least_solution_is_exact S E :
least_solution leqX S E → exact_solution eqX S E.
End solutions.
least_solution leqX S E → exact_solution eqX S E.
End solutions.
Now, if we generalize the previous result, we show that for
every system, the vector solution_sys(sizeSys S) S is the
least solution of S for every choice of ⩵,≦, as long as they
satisfy the axioms of Kleene algebras.
Corollary least_solution_exists : ∀ S : system,
∀ (eqX leqX : relation X),
∀ (equivX : @Equivalence X eqX) (preX : @PreOrder X leqX),
∀ (poX : @PartialOrder X eqX equivX leqX preX),
∀ (kaX : @KleeneAlgebra X eqX leqX jX pX zX uX sX),
least_solution leqX S (solution_sys (sizeSys S) S).
End system.
∀ (eqX leqX : relation X),
∀ (equivX : @Equivalence X eqX) (preX : @PreOrder X leqX),
∀ (poX : @PartialOrder X eqX equivX leqX preX),
∀ (kaX : @KleeneAlgebra X eqX leqX jX pX zX uX sX),
least_solution leqX S (solution_sys (sizeSys S) S).
End system.
Section automata_system.
Context {X : Set}{decX: decidable_set X }.
Context {Q : Set}{decQ: decidable_set Q }.
Context {X : Set}{decX: decidable_set X }.
Context {Q : Set}{decQ: decidable_set Q }.
Given an NFA with states of type Q and alphabet of type X,
we may generate a system sys_of_NFA A with constants regexp X and
variables Q.
Definition sys_of_NFA {Q : Set} (A : NFA Q X) : system Q (@regexp X) :=
(map (fun q ⇒ (e_un,q)) (fst A),
map (fun tr ⇒ (⟪snd(fst tr)⟫,snd tr,fst(fst tr))) (snd A)).
(map (fun q ⇒ (e_un,q)) (fst A),
map (fun tr ⇒ (⟪snd(fst tr)⟫,snd tr,fst(fst tr))) (snd A)).
There exists vector that assigns to every state a regular
expression denoting its language, and that is a weak solution of
sys_of_NFA A.
Lemma sys_of_NFA_solution (A : NFA Q X) :
∃ F,
(∀ q, ⟦F q⟧ ≃ langNFA A q)
∧ weak_solution (fun e f ⇒ ⟦e⟧ ≲ ⟦f⟧) (sys_of_NFA A) F.
∃ F,
(∀ q, ⟦F q⟧ ≃ langNFA A q)
∧ weak_solution (fun e f ⇒ ⟦e⟧ ≲ ⟦f⟧) (sys_of_NFA A) F.
pathSys M p u q n is a proposition saying ``there exists a
path in M of length not exceeding n from p to q labelled
with u''.
Fixpoint pathSys (M : system Q (@regexp X)) p u q n :=
match n with
| 0 ⇒ p = q ∧ u = []
| S n ⇒ ∃ e r v1 v2 , u = v1 ++ v2 ∧ (e,r,p) ∈ (snd M) ∧ ⟦e⟧ v1 ∧ pathSys M r v2 q n
end.
match n with
| 0 ⇒ p = q ∧ u = []
| S n ⇒ ∃ e r v1 v2 , u = v1 ++ v2 ∧ (e,r,p) ∈ (snd M) ∧ ⟦e⟧ v1 ∧ pathSys M r v2 q n
end.
langSys M q is the set of words uv such that there is a path
from q to some state p labelled with u, e≤p is in M and
v∈⟦e⟧.
Definition langSys M q : (@language X) :=
fun u ⇒ ∃ n p e v1 v2, u = v1 ++ v2 ∧ pathSys M q v1 p n ∧ (e,p) ∈ fst M ∧ ⟦e⟧ v2.
fun u ⇒ ∃ n p e v1 v2, u = v1 ++ v2 ∧ pathSys M q v1 p n ∧ (e,p) ∈ fst M ∧ ⟦e⟧ v2.
Every weak solution (w.r.t. language ordering) is greater than
langSys M q.
The language of an NFA is contained in the language of its
system.
Lemma sys_of_NFA_lang A q : langNFA A q ≲ langSys (sys_of_NFA A) q.
Definition eqX := (fun e f :@regexp X ⇒ ⟦e⟧ ≃ ⟦f⟧).
Definition leqX := (fun e f :@regexp X ⇒ ⟦e⟧ ≲ ⟦f⟧).
Instance eqX_eq : Equivalence eqX.
Instance leqX_o : PreOrder leqX.
Instance leqX_po : PartialOrder eqX leqX.
Instance kaX : KleeneAlgebra regexp eqX leqX.
Definition eqX := (fun e f :@regexp X ⇒ ⟦e⟧ ≃ ⟦f⟧).
Definition leqX := (fun e f :@regexp X ⇒ ⟦e⟧ ≲ ⟦f⟧).
Instance eqX_eq : Equivalence eqX.
Instance leqX_o : PreOrder leqX.
Instance leqX_po : PartialOrder eqX leqX.
Instance kaX : KleeneAlgebra regexp eqX leqX.
There is a least solution of sys_of_NFA A that associates to
every state its language.
Theorem sys_of_NFA_least_solution (A : NFA Q X) :
∃ F, (∀ q, ⟦F q⟧ ≃ langNFA A q) ∧ least_solution (fun e f ⇒ ⟦e⟧ ≲ ⟦f⟧) (sys_of_NFA A) F.
End automata_system.
∃ F, (∀ q, ⟦F q⟧ ≃ langNFA A q) ∧ least_solution (fun e f ⇒ ⟦e⟧ ≲ ⟦f⟧) (sys_of_NFA A) F.
End automata_system.
Section regexp.
Context {X : Set}{decX: decidable_set X }.
Lemma vars_Antimirov e : vars_system (sys_of_NFA (NFA_of_regexp e)) ⊆ stateSpace e.
Lemma Antimirov_inf e a f : e ∈ δA a f → ⟪a⟫·e≤KA f.
Theorem Antimirov_fundamental_theorem e A : Var e ⊆ A → e =KA ϵ e ∪ Σ_{A} (fun a ⇒ ⟪a⟫·Σ (δA a e)).
Lemma Antimirov_sys e :
exact_solution (ax_eq KA KA') (sys_of_NFA (NFA_of_regexp e)) id.
Lemma δA_proper_KA l :
Proper ((ax_eq KA KA') ==> (ax_eq KA KA')) (fun e ⇒ Σ (δA l e)).
Theorem CompletenessKA {A : Set} `{decidable_set A} :
∀ (e f : @regexp A), e =KA f ↔ ⟦e⟧ ≃ ⟦f⟧.
Corollary CompletenessKA_inf {A : Set} `{decidable_set A} :
∀ (e f : @regexp A), e ≤KA f ↔ ⟦e⟧ ≲ ⟦f⟧.
Theorem least_solution_Antimirov e :
least_solution (ax_inf KA KA') (sys_of_NFA (NFA_of_regexp e)) id.
End regexp.
Definition equate {A : Set} {decA : decidable_set A} (x y : A) : A → A :=
fun z ⇒ if z =?= y then x else z.
Context {X : Set}{decX: decidable_set X }.
Lemma vars_Antimirov e : vars_system (sys_of_NFA (NFA_of_regexp e)) ⊆ stateSpace e.
Lemma Antimirov_inf e a f : e ∈ δA a f → ⟪a⟫·e≤KA f.
Theorem Antimirov_fundamental_theorem e A : Var e ⊆ A → e =KA ϵ e ∪ Σ_{A} (fun a ⇒ ⟪a⟫·Σ (δA a e)).
Lemma Antimirov_sys e :
exact_solution (ax_eq KA KA') (sys_of_NFA (NFA_of_regexp e)) id.
Lemma δA_proper_KA l :
Proper ((ax_eq KA KA') ==> (ax_eq KA KA')) (fun e ⇒ Σ (δA l e)).
Theorem CompletenessKA {A : Set} `{decidable_set A} :
∀ (e f : @regexp A), e =KA f ↔ ⟦e⟧ ≃ ⟦f⟧.
Corollary CompletenessKA_inf {A : Set} `{decidable_set A} :
∀ (e f : @regexp A), e ≤KA f ↔ ⟦e⟧ ≲ ⟦f⟧.
Theorem least_solution_Antimirov e :
least_solution (ax_inf KA KA') (sys_of_NFA (NFA_of_regexp e)) id.
End regexp.
Definition equate {A : Set} {decA : decidable_set A} (x y : A) : A → A :=
fun z ⇒ if z =?= y then x else z.
Section inf_system.
Context {Q1 : Set}{decQ1: decidable_set Q1 }.
Context {Q2 : Set}{decQ2: decidable_set Q2 }.
Context {X : Set}{decX: decidable_set X }.
Context {jX: Join X}{pX: Product X}{zX: Zero X}{uX:Un X}{sX:Star X}.
Definition system_homomorphism (S1 : system Q1 X) (S2 : system Q2 X) (φ : Q1 → Q2) :=
(∀ a x, (a,x) ∈ fst S1 → (a,φ x) ∈ fst S2) ∧
(∀ a x x', (a,x,x') ∈ snd S1 → (a,φ x,φ x') ∈ snd S2).
Lemma inf_system (S1 : system Q1 X) (S2 : system Q2 X) (φ : Q1 → Q2) :
system_homomorphism S1 S2 φ →
∀ leqX E, weak_solution leqX S2 E → weak_solution leqX S1 (E∘φ).
End inf_system.
Context {Q1 : Set}{decQ1: decidable_set Q1 }.
Context {Q2 : Set}{decQ2: decidable_set Q2 }.
Context {X : Set}{decX: decidable_set X }.
Context {jX: Join X}{pX: Product X}{zX: Zero X}{uX:Un X}{sX:Star X}.
Definition system_homomorphism (S1 : system Q1 X) (S2 : system Q2 X) (φ : Q1 → Q2) :=
(∀ a x, (a,x) ∈ fst S1 → (a,φ x) ∈ fst S2) ∧
(∀ a x x', (a,x,x') ∈ snd S1 → (a,φ x,φ x') ∈ snd S2).
Lemma inf_system (S1 : system Q1 X) (S2 : system Q2 X) (φ : Q1 → Q2) :
system_homomorphism S1 S2 φ →
∀ leqX E, weak_solution leqX S2 E → weak_solution leqX S1 (E∘φ).
End inf_system.
Section intersect.
Context {Q1 : Set}{decQ1: decidable_set Q1 }.
Context {Q2 : Set}{decQ2: decidable_set Q2 }.
Context {X : Set}{decX: decidable_set X }.
Context {jX: Join X}{pX: Product X}{zX: Zero X}{uX:Un X}{sX:Star X}.
Definition intersect (S1 : system Q1 X) (S2 : system Q2 X) : system (Q1×Q2) X :=
(flat_map (fun E ⇒ flat_map (fun F ⇒ if (fst E=?=fst F) then [(fst E,(snd E,snd F))] else [])
(fst S2)) (fst S1),
flat_map (fun E ⇒ flat_map (fun F ⇒ if (fst (fst E)=?=fst (fst F))
then [(fst (fst E),(snd (fst E),snd (fst F)),(snd E,snd F))]
else [])
(snd S2)) (snd S1)).
Lemma intersect_left S1 S2 : system_homomorphism (intersect S1 S2) S1 fst.
Lemma intersect_right S1 S2 : system_homomorphism (intersect S1 S2) S2 snd.
Lemma intersect_univ {Q : Set} (S : system Q X) S1 S2 ϕ1 ϕ2 :
system_homomorphism S S1 ϕ1 → system_homomorphism S S2 ϕ2 →
system_homomorphism S (intersect S1 S2) (fun q ⇒ (ϕ1 q,ϕ2 q)).
End intersect.
Context {Q1 : Set}{decQ1: decidable_set Q1 }.
Context {Q2 : Set}{decQ2: decidable_set Q2 }.
Context {X : Set}{decX: decidable_set X }.
Context {jX: Join X}{pX: Product X}{zX: Zero X}{uX:Un X}{sX:Star X}.
Definition intersect (S1 : system Q1 X) (S2 : system Q2 X) : system (Q1×Q2) X :=
(flat_map (fun E ⇒ flat_map (fun F ⇒ if (fst E=?=fst F) then [(fst E,(snd E,snd F))] else [])
(fst S2)) (fst S1),
flat_map (fun E ⇒ flat_map (fun F ⇒ if (fst (fst E)=?=fst (fst F))
then [(fst (fst E),(snd (fst E),snd (fst F)),(snd E,snd F))]
else [])
(snd S2)) (snd S1)).
Lemma intersect_left S1 S2 : system_homomorphism (intersect S1 S2) S1 fst.
Lemma intersect_right S1 S2 : system_homomorphism (intersect S1 S2) S2 snd.
Lemma intersect_univ {Q : Set} (S : system Q X) S1 S2 ϕ1 ϕ2 :
system_homomorphism S S1 ϕ1 → system_homomorphism S S2 ϕ2 →
system_homomorphism S (intersect S1 S2) (fun q ⇒ (ϕ1 q,ϕ2 q)).
End intersect.