Library LangAlg.terms

In this module we define and study an algebra of terms with sequential composition and its unit, intersection, and a mirror operation restricted to variables.

Set Implicit Arguments.

Require Export tools language.
Delimit Scope term_scope with term.

Open Scope term.

Section def.


  Variable X : Set.
  Variable Λ : decidable_set X.

In this module, terms are built out of five constructs: the unit 1; variables and mirrored variables; and two binary products, the sequential product and the meet .
  Inductive 𝐓 : Set :=
  | 𝐓_one : 𝐓
  | 𝐓_var : X 𝐓
  | 𝐓_cvar : X 𝐓
  | 𝐓_seq : 𝐓 𝐓 𝐓
  | 𝐓_inter : 𝐓 𝐓 𝐓.

  Notation " 1 " := 𝐓_one : term_scope.
  Infix " ⋅ " := 𝐓_seq (at level 40) : term_scope.
  Infix " ∩ " := 𝐓_inter (at level 45) : term_scope.

The axioms are organised as follows: most axioms are identity axioms, in the group 𝐓_ax. These will be used to define both the equivalence and order relations. Then there is the axiom in 𝐓_axinf, only used for the order relation, and the axiom in 𝐓_axeq, to define the equivalence relation.
  Inductive 𝐓_ax : 𝐓 𝐓 Prop :=
⟨𝐓,⋅,1⟩ is a monoid.
is associative, commutative and idempotent.
1∩ _ does not distinguish the two products.
  | 𝐓_ax_inter_one_seq e f : 𝐓_ax (1 (ef)) (1 (e f))
1∩ _ does not distinguish the two types of variables.
Sub-units commute with other terms.
Together with the previous axiom, this allows one to group all the sub-units together in a term.
The intersection is smaller than its arguments.
  Inductive 𝐓_axinf : 𝐓 𝐓 Prop :=
  | 𝐓_inter_inf e f : 𝐓_axinf (e f) e.

This equality law is equivalent to saying that the sequential product is monotone with respect to the order relation (rule 𝐓_inf_seq below).
Order relation on terms.
  Inductive 𝐓_inf : Smaller 𝐓 :=
  | 𝐓_inf_refl e : e e
  | 𝐓_inf_trans e f g : e f f g e g
  | 𝐓_inf_axinf e f : 𝐓_axinf e f e f
  | 𝐓_inf_ax e f : 𝐓_ax e f 𝐓_ax f e e f
  | 𝐓_inf_seq e f g h : e g f h (e f) (g h)
  | 𝐓_inf_inter e f g h : e g f h (e f) (g h).
  Global Instance 𝐓_Smaller : Smaller 𝐓 := 𝐓_inf.

Equivalence relation on terms.

  Global Instance 𝐓_Equiv : Equiv 𝐓 := 𝐓_eq.

General properties

The axiomatic equivalence of terms is an equivalence relation.
  Global Instance 𝐓_eq_Equivalence : Equivalence equiv.

The axiomatic containment of terms is a preorder relation.
  Global Instance 𝐓_inf_PreOrder : PreOrder smaller.

Both products are monotone with respect to both relations.
  Global Instance 𝐓_inter_equiv :
    Proper (equiv ==> equiv ==> equiv) 𝐓_inter.

  Global Instance 𝐓_seq_equiv :
    Proper (equiv ==> equiv ==> equiv) 𝐓_seq.

  Global Instance 𝐓_inter_smaller :
    Proper (smaller ==> smaller ==> smaller) 𝐓_inter.

  Global Instance 𝐓_seq_smaller :
    Proper (smaller ==> smaller ==> smaller) 𝐓_seq.

To be larger than an intersection, it suffices to be larger than its arguments.
  Lemma 𝐓_inter_elim e f g : e g f g e f g.

The intersection is a least upper bound.
  Lemma 𝐓_inter_intro e f g : e f e g e f g.

The equivalence relation is contained in the order relation.
  Lemma 𝐓_eq_inf u v : u v u v.

The order relation can be encoded inside the equivalence relation.
  Lemma 𝐓_inf_eq_inter u v : u v u v u.

With the last two lemma, it is very simple to check that axiomatic containment is a partial order with respect to axiomatic equivalence.
The following few laws are simple consequences of our axioms.
  Lemma 𝐓_inter_one_abs e f : (1 e)⋅(1 f) 1 (e f).

  Lemma 𝐓_inter_onel e : 1 e (1 e)⋅e.

  Lemma 𝐓_inter_oner e : 1 e e (1 e).

  Lemma 𝐓_inf_one_prod_is_inter u v : u 1 v 1 u v u v.

End def.
Section s.

Variables and size

  Context{ X : Set }.
  Context{ Λ : decidable_set X }.

As usual, we define the size of a term as the number of nodes in its syntax tree.
  Global Instance 𝐓_size : Size (𝐓 X) :=
    fix 𝐓_size t :=
      match t with
      | 1 | 𝐓_cvar _ | 𝐓_var _S 0
      | s t | s tS (𝐓_size s + 𝐓_size t)

[a_1 ;...; a_n] is the term (a_1 a_1') ( ... ((a_n a_n') 1)), where a_i' represents the mirrored version of a variable.
  Definition to_test :=
    fold_right (fun a (t : 𝐓 X) ⇒ 𝐓_var a 𝐓_cvar a t) 1.
  Notation " ⟨ l ⟩ " := (to_test l) : term_scope.

The variables of a term are the variables appearing in it either plainly or in mirrored version.
  Global Instance suppT : Alphabet 𝐓 X :=
    fix 𝐓_variables (s : 𝐓 X) :=
      match s with
      | 1 ⇒ []
      | 𝐓_var a[a]
      | 𝐓_cvar a[a]
      | s t | s t𝐓_variables s ++ 𝐓_variables t

If e is smaller than f, then every variable of f appears in e.

Properties of _

The set of variables of the term l is equivalent to l itself.
The size of the term l is related to the length of l as follows.
  Lemma 𝐓_size_to_test (l : list X) : l = 4 × (length l) + 1.

The function _ only produces sub-units.
  Lemma 𝐓_to_test_one (l : list X) : l 1.

The function _ transforms unions into intersections.
  Lemma 𝐓_to_test_app (l m : list X) :
    l++m l m.

Adding to a list an element that is already there does not change the image by _.
  Lemma 𝐓_to_test_in (a : X) l : a l l a::l.

_ is contravariant with respect to the order.
  Lemma 𝐓_to_test_incl_inf (l m : list X) :
    l m m l.

  Global Instance to_test_inf :
    Proper (Basics.flip (@incl X) ==> smaller) to_test.

  Global Instance to_test_inf_flip :
    Proper (@incl X ==> Basics.flip smaller) to_test.

_ is monotone with respect to equivalence.
  Global Instance to_test_equivalent :
    Proper (@equivalent X ==> equiv) to_test.

Applying _ to the set of variables of a term is equivalent to intersecting it with 1.
We now prove some equational laws of _.

Mirror of a term

We define the following mirror function on terms.
  Fixpoint 𝐓_conv (t : 𝐓 X) :=
    match t with
    | 1 ⇒ 1
    | 𝐓_var a𝐓_cvar a
    | 𝐓_cvar a𝐓_var a
    | u v𝐓_conv u 𝐓_conv v
    | u v𝐓_conv v 𝐓_conv u

  Notation " t ° " := (𝐓_conv t) (at level 25) : term_scope.

It is idempotent.
  Lemma 𝐓_conv_idem t : t°° t.

It disappears under 1∩_.
  Lemma 𝐓_conv_one t : 1 (t°) 1 t.

This operation is also monotone.
  Global Instance 𝐓_conv_equiv : Proper (equiv ==> equiv) 𝐓_conv.
  Global Instance 𝐓_conv_inf : Proper (smaller ==> smaller) 𝐓_conv.

End s.

Section language.

Language interpretation

  Context { X : Set }.
  Open Scope lang.

We interpret expressions as languages in the obvious way:
  Global Instance to_lang_𝐓 {Σ} : semantics 𝐓 language X Σ :=
    fix to_lang_𝐓 σ e:=
      match e with
      | 1%term ⇒ 1
      | 𝐓_var a ⇒ (σ a)
      | 𝐓_cvar a(σ a
      | (e f)%term(to_lang_𝐓 σ e) (to_lang_𝐓 σ f)
      | (e f)%term(to_lang_𝐓 σ e) (to_lang_𝐓 σ 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) (@𝐓_inter X).
  Global Instance sem_eq_𝐓_seq :
    Proper (sequiv ==> sequiv ==> sequiv) (@𝐓_seq X).
  Global Instance sem_eq_𝐓_inter :
    Proper (sequiv ==> sequiv ==> sequiv) (@𝐓_inter X).

  Context { Σ : Set } { σ : 𝕬[XΣ] } {A : list X}.

A word w is contained in the σ-interpretation of the term A if and only if w is empty and σ is test-compatible with A.
If σ is test-compatible with A then the σ-interpretation of the term A is the unit language.
Otherwise the σ-interpretation of the term A is the empty language.
This is just the contrapositive of the previous statement.
  Lemma test_compatible_𝐓_to_test_not_empty w :
    w⋵(Aσ) A σ.

Close Scope lang.

End language.

Close Scope term.