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.
  Lemma variables_๐–_par (s t : ๐– X) :
    โŒˆs โŠ• tโŒ‰ โ‰ˆ โŒˆsโŒ‰ ++ โŒˆtโŒ‰.

  Lemma variables_๐–_seq (s t : ๐– X) :
    โŒˆs โŠ— tโŒ‰ โ‰ˆ โŒˆsโŒ‰ ++ โŒˆtโŒ‰.

Both products are monotone operations.
  Global Instance ๐–_seq_๐–_inf :
    Proper (smaller ==> smaller ==> smaller) ๐–_seq.

  Global Instance ๐–_seq_๐–_equiv :
    Proper (equiv ==> equiv ==> equiv) ๐–_seq.
  Global Instance ๐–_par_๐–_inf :
    Proper (smaller ==> smaller ==> smaller) ๐–_par.

  Global Instance ๐–_par_๐–_equiv :
    Proper (equiv ==> equiv ==> equiv) ๐–_par.

We now list some (in)equalities between weak terms.
  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)).

The size of e โŠ• f is smaller than the sum of the sizes of e and f, plus one.
  Lemma ๐–_size_๐–_par e f : โฆƒe โŠ• fโฆ„ โ‰ค S (โฆƒeโฆ„ + โฆƒfโฆ„).

The size of e โŠ— f is smaller than the sum of the sizes of e and f, plus one.
 Lemma ๐–_size_๐–_seq e f : โฆƒe โŠ— fโฆ„ โ‰ค S (โฆƒeโฆ„ + โฆƒfโฆ„).

End s.

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.
  Lemma is_balanced_๐–'_variables w :
    is_balanced (๐–'_variables w).

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.
  Lemma ๐–_prod_semantics ฮฃ u v (ฯƒ : ๐•ฌ[Xโ†’ฮฃ]) : (โŸฆuโŠ—vโŸงฯƒ) โ‰ƒ (โŸฆuโŸงฯƒ) โ‹… (โŸฆvโŸงฯƒ).

The interpretation of a parallel product is the intersection of the interpretations.
  Lemma ๐–_intersection_semantics ฮฃ u v (ฯƒ : ๐•ฌ[Xโ†’ฮฃ]) : โŸฆuโŠ•vโŸงฯƒ โ‰ƒ (โŸฆuโŸงฯƒ) โˆฉ (โŸฆvโŸงฯƒ).

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.