Library LangAlg.sp_terms

This module deals with series-parallel terms.

Set Implicit Arguments.

Require Export tools language.


Section s0.
  Variable X : Set.

Unsurprisingly, here terms are built out of variables and two binary operations.
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

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)

The length of the list of variables of a term is smaller than its size.
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:

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.
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.
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.
Adding tests only makes the relation grow.
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.

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

By construction this function generates balanced sets.
The result of this function is always a superset of the set of variables of the term.
The primed variable (a,b) is in ๐’๐'_variables u exactly when either (a,true) or (a,false) appears in โŒˆuโŒ‰.
This is another formulation of the same result.
The length of the result of this function is the size of the term plus one.

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)

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