Library LangAlg.w_terms

This module introduces weak terms, and establishes some of their general properties.

Set Implicit Arguments.

Require Export tools sp_terms.

Plain weak terms

Definitions

Section s0.
Fix a set of variables X.
Variable X : Set.

A weak term consists of a pair whose first projection is either a series-parallel term or the constant None (which stands for 1 in this context), and whose second projection is a list of variables, called the set of tests of the term.
Definition ๐ : Set := (option (๐๐ X)) ร list X.

The weak term ๐ญ is the pair (None,[]).
Definition ๐_one : ๐ := (None,[]).

End s0.
Notation " ๐ญ " := ๐_one.

Section s.
Context {X : Set}.
We define the sequential product of weak terms as follows.
Definition ๐_seq (u v : ๐ X) : ๐ X :=
match (u,v) with
| ((None,A),(s,B)) โ (s,A++B)
| ((s,A),(None,B)) โ (s,A++B)
| ((Some s,A),(Some t,B)) โ (Some (sโจพt),A++B)
end.
Infix " โ " := ๐_seq (at level 40).

We define the parallel product of weak terms as follows.
Definition ๐_par (u v : ๐ X) : ๐ X :=
match (u,v) with
| ((None,A),(None,B)) โ (None,A++B)
| ((None,A),(Some s,B)) โ (None,A++B++โsโ)
| ((Some s,A),(None,B)) โ (None,A++B++โsโ)
| ((Some s,A),(Some t,B)) โ (Some (sโฅt),A++B)
end.
Infix " โ " := ๐_par (at level 50).

We use the parametric ordering on series-parallel terms to define the ordering of weak_terms.
Global Instance ๐_inf : Smaller (๐ X) :=
fun e f โ
match (e,f) with
| ((None,A),(None,B)) โ B โ A
| ((None,A),(Some u,B)) โ B โ A โง โuโ โ A
| ((Some u,A),(None,B)) โ False
| ((Some u,A),(Some v,B)) โ B โ A โง A โจ u << v
end.

As usual, this relation is indeed a preorder.
Global Instance ๐_inf_PreOrder : PreOrder smaller.

By taking its symmetric closure, we get an equivalence relation.
Global Instance ๐_equiv : Equiv (๐ X) := fun e f โ e โค f โง f โค e.

Global Instance ๐_equiv_Equivalence :
Equivalence equiv.

Global Instance ๐_inf_PartialOrder: PartialOrder equiv smaller.

We now define the size and the set of variables of a weak term.
Global Instance ๐_size : Size (๐ X) :=
fun u โ
match u with
| (None,A) โ length A
| (Some s,A) โ โฆsโฆ + length A
end.

Global Instance ๐_variables : Alphabet ๐ X :=
fun u โ
match u with
| (None,A) โ A
| (Some u,A) โ โuโ ++ A
end.

Properties of weak terms.

Both product act as a union with respect to sets of variables.
Both products are monotone operations.
We now list some (in)equalities between weak terms.
The size of e โ f is smaller than the sum of the sizes of e and f, plus one.
The size of e โ f is smaller than the sum of the sizes of e and f, plus one.

Primed weak terms.

Section primed.
Context { X : Set }.

Definitions

Primed weak terms are weak terms over a duplicated alphabet, such that their set of tests are balanced (that is each variable appears positively if and only if it appears negatively).
Definition ๐' := { w : ๐ (@X' X) | is_balanced (snd w) }.

We define the primed weak term ๐ญ'.
Definition ๐'_one : ๐' :=
exist _ (None,[]) (@balanced_nil X).
Notation " ๐ญ' " := ๐'_one.

We define their set of variables using the set of primed variables of the underlining series-parallel term over the duplicated alphabet.
Definition ๐'_variables (u : ๐') :=
match ฯ{u} with
| (None,A) โ A
| (Some u,A) โ ๐๐'_variables u ++ A
end.

The size of a primed weak term is simply its size as a weak term.
Global Instance ๐'_size : Size ๐' := fun u โ โฆฯ{u}โฆ.

The set of variables of a primed weak term is always balanced.
Sequential product of primed weak terms.
Definition ๐'_seq (u v : ๐') : ๐' :=
match (u,v) with
| ((exist _ (None,A) p1),(exist _ (None,B) p2)) โ
exist _ (None,A++B)
(is_balanced_app p1 p2)
| ((exist _ (None,A) p1),(exist _ (Some s,B) p2)) โ
exist _ (Some s,A++B) (is_balanced_app p1 p2)
| ((exist _ (Some s,A) p1),(exist _ (None,B) p2)) โ
exist _ (Some s,A++B) (is_balanced_app p1 p2)
| ((exist _ (Some s,A) p1),(exist _ (Some t,B) p2)) โ
exist _ (Some (sโจพt),A++B) (is_balanced_app p1 p2)
end.
Infix " โ' " := ๐'_seq (at level 40).

Parallel product of primed weak terms.
Definition ๐'_par (u v : ๐') : ๐':=
match (u,v) with
| ((exist _ (None,A) p1),(exist _ (None,B) p2)) โ
exist _ (None,A++B)
(is_balanced_app p1 p2)
| ((exist _ (None,A) p1),(exist _ (Some s,B) p2)) โ
exist _ (None,A++B++๐๐'_variables s)
(is_balanced_app p1 (is_balanced_app
p2(is_balanced_๐๐'_variables s)))
| ((exist _ (Some s,A) p1),(exist _ (None,B) p2)) โ
exist _ (None,A++B++๐๐'_variables s)
(is_balanced_app p1 (is_balanced_app
p2(is_balanced_๐๐'_variables s)))
| ((exist _ (Some s,A) p1),(exist _ (Some t,B) p2)) โ
exist _ (Some (sโฅt),A++B) (is_balanced_app p1 p2)
end.
Infix " โ' " := ๐'_par (at level 50).

The order relations on primed weak terms are simply imported from those of weak terms.
Global Instance ๐'_inf : Smaller ๐' := fun u v โ ฯ{u} โค ฯ{v}.
Global Instance ๐'_equiv : Equiv ๐' := fun u v โ ฯ{u} โก ฯ{v}.

Global Instance ๐'_inf_PreOrder : PreOrder smaller.

Global Instance ๐'_equiv_Equivalence: Equivalence equiv.

Global Instance ๐'_inf_PartialOrder : PartialOrder equiv smaller.

Properties of primed weak terms.

Lemma variables_๐'_par (s t : ๐') :
๐'_variables (s โ' t) โ ๐'_variables s ++ ๐'_variables t.

Lemma variables_๐'_seq (s t : ๐') :
๐'_variables (s โ' t) โ ๐'_variables s ++ ๐'_variables t.

Global Instance ๐'_par_๐'_inf :
Proper (smaller ==> smaller ==> smaller) ๐'_par.
Global Instance ๐'_seq_๐'_inf :
Proper (smaller ==> smaller ==> smaller) ๐'_seq.

Global Instance ๐'_par_๐'_equiv :
Proper (equiv ==> equiv ==> equiv) ๐'_par.
Global Instance ๐'_seq_๐'_equiv :
Proper (equiv ==> equiv ==> equiv) ๐'_seq.

Lemma ๐'_par_comm e f : e โ' f โก f โ' e.

Lemma ๐'_par_idem e : e โ' e โก e.

Lemma ๐'_seq_assoc e f g : eโ'(f โ' g) โก (eโ'f)โ'g.

Lemma ๐'_par_assoc e f g : eโ'(f โ' g) โก (eโ'f)โ'g.
Lemma ๐'_seq_one_l e : ๐ญ' โ' e โก e.
Lemma ๐'_seq_one_r e : e โ' ๐ญ' โก e.

Lemma ๐'_par_inf e f : e โ' f โค e.
Lemma ๐'_par_one_l e : ๐ญ' โ' e โค (๐ญ' โ' e)โ'e.
Lemma ๐'_par_one_r e : ๐ญ' โ' e โค eโ'(๐ญ' โ' e).

Lemma ๐'_par_one_seq_par e f : ๐ญ' โ' (eโ'f) โก ๐ญ' โ' (e โ' f).
Lemma ๐'_par_one_seq_par_one e f: (๐ญ' โ' e)โ'(๐ญ'โ'f) โก ๐ญ'โ'(eโ'f).
Lemma ๐'_par_one_seq e f : (๐ญ' โ' e)โ'f โก fโ'(๐ญ'โ'e).
Lemma ๐'_par_one_par e f g: ((๐ญ' โ' e)โ'f)โ'g โก (๐ญ'โ'e)โ'(fโ'g).

Lemma ๐'_size_๐'_par e f : โฆe โ' fโฆ โค S (โฆeโฆ + โฆfโฆ).
Lemma ๐'_size_๐'_seq e f : โฆe โ' fโฆ โค S (โฆeโฆ + โฆfโฆ).

Lemma sub_identity_par_one (A : list (@X' X)) (p : is_balanced A) :
(exist _ (None,A) p) โก ๐ญ' โ' (exist _ (None,A) p).

End primed.

Infix " โ' " := ๐'_par (at level 50).
Infix " โ' " := ๐'_seq (at level 40).
Notation "๐ญ'" := ๐'_one.

Section language.

Language interpretation

Open Scope lang.
Context { X : Set }.

The function T ฯ t is the full language if the assignment ฯ is test-compatible with the set of tests of the weak term t, or the empty language otherwise.
Definition T {ฮฃ} (ฯ : ๐ฌ[Xโฮฃ]) (t : ๐ X) : language ฮฃ := fun _ โ snd t โข ฯ.

The interpretation of the weak term (s,A) with respect to the assignment ฯ is either the ฯ-interpretation of s (as a series parallel term) if ฯ is test-compatible with A, or 0 otherwise.
Global Instance to_lang_๐ {ฮฃ} : semantics ๐ language X ฮฃ :=
fun ฯ t โ T ฯ t โฉ (match fst t with
| None โ 1
| Some u โ โฆuโงฯ
end).

The interpretation of a sequential product is the concatenation of the interpretations.
The interpretation of a parallel product is the intersection of the interpretations.
Both products are monotone.
Global Instance sem_incl_๐_seq :
Proper (ssmaller ==> ssmaller ==> ssmaller) (@๐_seq X).

Global Instance sem_incl_๐_inter :
Proper (ssmaller ==> ssmaller ==> ssmaller) (@๐_par X).

Global Instance sem_eq_๐_seq :
Proper (sequiv ==> sequiv ==> sequiv) (@๐_seq X).

Global Instance sem_eq_๐_inter :
Proper (sequiv ==> sequiv ==> sequiv) (@๐_par X).

Section ฮ.
Variable ฮฃ : Set.

ฮ transforms an assignment from X to ฮฃ into an assignment from the duplicated alphabet to the same ฮฃ.
Definition ฮ (ฯ : ๐ฌ[Xโฮฃ]) : (๐ฌ[X'โฮฃ]) :=
fun x โ
match x with
| (a,true) โ ฯ a
| (a,false) โ (ฯ a)ยฐ
end.

ฮ preserves test-compatibility.
Lemma test_compatible_ฮ (ฯ : ๐ฌ[Xโฮฃ]) A :
map fst A โข ฯ โ A โข ฮ ฯ.

End ฮ.

Close Scope lang.
End language.