Library LangAlg.sp_terms

This module deals with series-parallel terms.

Set Implicit Arguments.

Require Export tools language.

Terms

Section s0.
Variable X : Set.

Unsurprisingly, here terms are built out of variables and two binary operations.

  Inductive 𝐒𝐏 : Set :=
  | 𝐒𝐏 _var : X → 𝐒𝐏
  | 𝐒𝐏 _seq : 𝐒𝐏 → 𝐒𝐏 → 𝐒𝐏
  | 𝐒𝐏 _par : 𝐒𝐏 → 𝐒𝐏 → 𝐒𝐏.

End s0.

In the following, ⨾ denotes the sequential composition, and ∥ the parallel composition.

Infix " ⨾ " := 𝐒𝐏 _seq (at level 40).
Infix " ∥ " := 𝐒𝐏 _par (at level 50).
Section s.
Context {X : Set}.

Set of variables of a term. Being associated with the class Alphabet, we can write the set of variables of a term e as ⌈e⌉.

  Global Instance 𝐒𝐏 _variables : Alphabet 𝐒𝐏 X :=
    fix 𝐒𝐏_variables e :=
      match e with
      | 𝐒𝐏 _var a ⇒ [a]
      | e ⨾ f | e ∥ f ⇒ 𝐒𝐏 _variables e ++ 𝐒𝐏 _variables f
      end.

We define the size of a term as the number of nodes in its syntax tree.

  Global Instance 𝐒𝐏 _size : Size (𝐒𝐏 X) :=
    fix 𝐒𝐏_size (u : 𝐒𝐏 X) : nat :=
      match u with
      | 𝐒𝐏 _var _ ⇒ S O
      | u ⨾ v | u ∥ v ⇒ S (𝐒𝐏 _size u + 𝐒𝐏 _size v)
      end.

The length of the list of variables of a term is smaller than its size.

Lemma 𝐒𝐏 _size_𝐒𝐏 _variables (u : 𝐒𝐏 X) :
length ⌈ u ⌉ ≤ ⦃ u ⦄.

In fact, because the length of the list of variables is the number of leaves of the syntax tree of the term, and because that tree is binary, we have the following identity:

Lemma 𝐒𝐏 _size_𝐒𝐏 _variables_eq (u : 𝐒𝐏 X) :
⦃ u ⦄ = 2 × length ⌈ u ⌉ - 1.

Parametric axiomatization

For series parallel terms, we don't axiomatize equality but instead consider containment. Furthermore, this axiomatization will be parametric in a set of variables. This parameter will contain the variables that are super-units for the sequential product: that is variables a such that for any term u we have u≤u⨾a and u≤a⨾u. In the following, we call the variables from the parameter tests.

The axioms are split into two groups: the equality axioms, which can be used in both directions, and the containment axioms which must be read from left to right.

The equality axioms simply state that ⨾ is associative, and that ∥ is associative, commutative, and idempotent.

  Inductive 𝐒𝐏 _ax : 𝐒𝐏 X → 𝐒𝐏 X → Prop :=
  | 𝐒𝐏 _seq_assoc e f g : 𝐒𝐏 _ax (e ⨾(f ⨾ g )) ((e ⨾f )⨾g)
  | 𝐒𝐏 _par_assoc e f g : 𝐒𝐏 _ax (e ∥(f ∥ g )) ((e ∥f )∥g)
  | 𝐒𝐏 _par_comm e f : 𝐒𝐏 _ax (e ∥f) (f ∥e)
  | 𝐒𝐏 _par_idem e : 𝐒𝐏 _ax (e ∥ e) e.

The containment axioms state that ∥ is a deceasing operation (it is in fact the greatest lower bound), and that is a term is only composed of tests, then it is a super-unit.

  Inductive 𝐒𝐏 _axinf (A : list X) : 𝐒𝐏 X → 𝐒𝐏 X → Prop :=
  | 𝐒𝐏 _axinf_weak e f : 𝐒𝐏 _axinf A (e ∥ f) e
  | 𝐒𝐏 _axinf_1_seql e f : ⌈e ⌉ ⊆ A → 𝐒𝐏 _axinf A f (e ⨾ f)
  | 𝐒𝐏 _axinf_1_seqr e f : ⌈e ⌉ ⊆ A → 𝐒𝐏 _axinf A f (f ⨾ e).

  Reserved Notation " A ⊨ e << f " (at level 80).

The relation A⊨ e << f is then the smallest order relation (that is reflexive and transitive) containing both sets of axioms, and such that ⨾ and ∥ are monotone operations.

  Inductive 𝐒𝐏 _inf (A : list X) : 𝐒𝐏 X → 𝐒𝐏 X → Prop :=
  | 𝐒𝐏 _inf_re e : A ⊨ e << e
  | 𝐒𝐏 _inf_trans e f g : A ⊨ e << f → A ⊨ f << g → A ⊨ e << g
  | 𝐒𝐏 _inf_ax e f : 𝐒𝐏 _ax e f ∨ 𝐒𝐏 _ax f e → A ⊨ e << f
  | 𝐒𝐏 _inf_axinf e f: 𝐒𝐏 _axinf A e f → A ⊨ e << f

  | 𝐒𝐏 _inf_seq e f g h :
      A ⊨ e << g → A ⊨ f << h → A ⊨ e ⨾ f << g ⨾ h
  | 𝐒𝐏 _inf_par e f g h :
      A ⊨ e << g → A ⊨ f << h → A ⊨ e ∥ f << g ∥ h
  where " A ⊨ e << f " := (𝐒𝐏 _inf A e f).

  Hint Constructors 𝐒𝐏 _inf 𝐒𝐏 _ax 𝐒𝐏 _axinf.

  Global Instance 𝐒𝐏 _inf_PreOrder A : PreOrder (𝐒𝐏 _inf A).

  Global Instance par_𝐒𝐏 _inf A :
    Proper ((𝐒𝐏 _inf A ) ==> (𝐒𝐏 _inf A ) ==> (𝐒𝐏 _inf A ))
           (@𝐒𝐏 _par X).
  Global Instance seq_𝐒𝐏 _inf A :
    Proper ((𝐒𝐏 _inf A ) ==> (𝐒𝐏 _inf A ) ==> (𝐒𝐏 _inf A ))
           (@𝐒𝐏 _seq X).

Adding tests only makes the relation grow.

Lemma incl_𝐒𝐏 _inf A B e f :
A ⊆ B → A ⊨ e << f → B ⊨ e << f.

This relation has a very useful property: if e is smaller than f with tests A, then the variables in f all appear either as variables of e of as tests.

Lemma 𝐒𝐏 _inf_variables (A : list X) e f :
A ⊨ e << f → ⌈ f ⌉ ⊆ ⌈ e ⌉ ++ A.

End s.

Terms over a duplicated alphabet

Section primed.
Context { X : Set }.

We define the primed variables of a term e as follows:

  Fixpoint 𝐒𝐏'_variables (e : 𝐒𝐏 X') : list (@X' X) :=
    match e with
    | 𝐒𝐏 _var (a,_) ⇒ [(a,true );(a,false )]
    | e ⨾ f | e ∥ f ⇒ 𝐒𝐏'_variables e ++ 𝐒𝐏'_variables f
    end.

By construction this function generates balanced sets.

Lemma is_balanced_𝐒𝐏'_variables u : is_balanced (𝐒𝐏'_variables u).

The result of this function is always a superset of the set of variables of the term.

Lemma 𝐒𝐏 _variables_𝐒𝐏'_variables e : ⌈e ⌉ ⊆ 𝐒𝐏'_variables e.

The primed variable (a,b) is in 𝐒𝐏'_variables u exactly when either (a,true) or (a,false) appears in ⌈u⌉.

Lemma 𝐒𝐏 _variables_𝐒𝐏'_variables_iff u a b :
(a ,b ) ∈ (𝐒𝐏'_variables u ) ↔ (a ,true ) ∈ ⌈u ⌉ ∨ (a ,false ) ∈ ⌈u ⌉.

This is another formulation of the same result.

Lemma fst_𝐒𝐏 _variables (u : 𝐒𝐏 (@X' X)) : map fst ⌈u ⌉ ≈ map fst (𝐒𝐏'_variables u).

The length of the result of this function is the size of the term plus one.

Lemma 𝐒𝐏 _size_𝐒𝐏'_variables u :
length (𝐒𝐏'_variables u) = S ⦃u ⦄.
End primed.

Section language.

Language interpretation

Context { X : Set }.

Open Scope lang.

We interpret the sequential product by concatenation and the parallel product by intersection.

  Global Instance to_lang_𝐒𝐏 {Σ} : semantics 𝐒𝐏 language X Σ :=
    fix to_lang_𝐒𝐏 σ e:=
      match e with
      | 𝐒𝐏 _var a ⇒ (σ a)
      | e ⨾ f ⇒ (to_lang_𝐒𝐏 σ e ) ⋅ (to_lang_𝐒𝐏 σ f)
      | e ∥ f ⇒ (to_lang_𝐒𝐏 σ e ) ∩ (to_lang_𝐒𝐏 σ f)
      end.

We define semantic equality and containment of series parallel from those of languages.

  Global Instance semSmaller_𝐒𝐏 : SemSmaller (𝐒𝐏 X) :=
    (@semantic_containment _ _ _ _ _).

  Global Instance 𝐒𝐏 _sem_PreOrder : PreOrder (fun e f : 𝐒𝐏 X ⇒ e ≲ f).

  Global Instance semEquiv_𝐒𝐏 : SemEquiv (𝐒𝐏 X) :=
    (@semantic_equality _ _ _ _ _).

  Global Instance 𝐒𝐏 _sem_equiv : Equivalence (fun e f : 𝐒𝐏 X ⇒ e ≃ f).

  Global Instance 𝐒𝐏 _sem_PartialOrder :
    PartialOrder (fun e f : 𝐒𝐏 X ⇒ e ≃ f) (fun e f : 𝐒𝐏 X ⇒ e ≲ f).

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).

An assignment σ is test-compatible with the set of variables of u if and only if the σ-interpretation of u contains the empty list.

  Lemma test_compatible_nil (Σ : Set) (u : 𝐒𝐏 X) (σ : 𝕬[X →Σ ]) :
    ⌈ u ⌉ ⊢ σ ↔ (⟦u ⟧ σ) [].

  Close Scope lang.
End language.