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.

Definitions

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.

  | 𝐓 _ax_seq_assoc e f g : 𝐓 _ax (e ⋅(f ⋅ g )) ((e ⋅f )⋅g)
  | 𝐓 _ax_seq_one_left e : 𝐓 _ax (1⋅e) e
  | 𝐓 _ax_seq_one_right e : 𝐓 _ax (e ⋅1) e

∩ is associative, commutative and idempotent.

  | 𝐓 _ax_inter_assoc e f g : 𝐓 _ax (e ∩(f ∩ g )) ((e ∩f )∩g)
  | 𝐓 _ax_inter_comm e f : 𝐓 _ax (e ∩f) (f ∩e)
  | 𝐓 _ax_inter_idem e : 𝐓 _ax (e ∩ e) e

1∩ _ does not distinguish the two products.

| 𝐓 _ax_inter_one_seq e f : 𝐓 _ax (1 ∩ (e ⋅f )) (1 ∩ (e ∩ f ))

1∩ _ does not distinguish the two types of variables.

| 𝐓 _ax_inter_one_conv a : 𝐓 _ax (1 ∩ 𝐓 _cvar a) (1 ∩ 𝐓 _var a)

Sub-units commute with other terms.

| 𝐓 _ax_inter_one_comm_seq e f : 𝐓 _ax ((1 ∩ e )⋅f) (f ⋅(1∩e ))

Together with the previous axiom, this allows one to group all the sub-units together in a term.

| 𝐓 _ax_inter_one_inter e f g : 𝐓 _ax (((1 ∩ e )⋅f )∩g) ((1∩e )⋅(f ∩g )).

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

Inductive 𝐓 _axeq : 𝐓 → 𝐓 → Prop :=
| 𝐓 _ax_exchange a b c d : 𝐓 _axeq (((a ∩b )⋅(c ∩d ))∩(a ⋅c )) ((a ∩b )⋅(c ∩d )).

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.

Global Instance 𝐓 _inf_PartialOrder : PartialOrder equiv smaller.

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.

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

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

Lemma 𝐓 _inf_variables_incl (e f : 𝐓 X): e ≤ f → ⌈f ⌉ ⊆ ⌈e ⌉.

Properties of ⟨_⟩

The set of variables of the term ⟨l⟩ is equivalent to l itself.

Lemma 𝐓 _variables_to_test (l : list X) : ⌈ ⟨l ⟩ ⌉ ≈ l.

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.

Lemma 𝐓 _to_test_is_par_one (u : 𝐓 X) : ⟨⌈u ⌉⟩ ≡ 1 ∩ u.

We now prove some equational laws of ⟨_⟩.

  Lemma 𝐓 _to_test_comm A (e : 𝐓 X) : ⟨A ⟩ ⋅ e ≡ e ⋅ ⟨A ⟩.

  Lemma 𝐓 _to_test_dupl (A : list X) : ⟨A ⟩ ≡ ⟨A ⟩ ⋅ ⟨A ⟩.

  Lemma 𝐓 _to_test_distr1 A (e f : 𝐓 X) : ⟨A ⟩ ⋅ (e ∩f ) ≡ (⟨A ⟩ ⋅ e )∩ f.

  Lemma 𝐓 _to_test_distr2 A (e f : 𝐓 X) : ⟨A ⟩ ⋅ (e ∩f ) ≡ e ∩(⟨A ⟩ ⋅ f ).

  Lemma 𝐓 _to_test_distr A (e f : 𝐓 X) : ⟨A ⟩ ⋅ (e ∩f ) ≡ (⟨A ⟩ ⋅ e )∩(⟨A ⟩ ⋅ f ).

  Lemma 𝐓 _weak_seq A B (u : 𝐓 X) : (⟨ A ⟩ ⋅ u ) ⋅ ⟨ B ⟩ ≡ (⟨ A ⟩ ∩ ⟨ B ⟩) ⋅ u.

  Lemma 𝐓 _weak_par A B (u v : 𝐓 X) : (⟨ A ⟩ ⋅ u ) ∩ (⟨ B ⟩ ⋅ v ) ≡ (⟨ A ⟩ ∩ ⟨ B ⟩) ⋅ (u ∩ v ).

Mirror of a term

We define the following mirror function on terms.

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

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.

Lemma test_compatible_𝐓 _to_test w : w ⋵ (⟦⟨A ⟩⟧ σ ) ↔ A ⊢ σ ∧ w = [].

If σ is test-compatible with A then the σ-interpretation of the term ⟨A⟩ is the unit language.

Lemma test_compatible_𝐓 _to_test_true : A ⊢ σ → ⟦⟨A ⟩⟧σ ≃ 1.

Otherwise the σ-interpretation of the term ⟨A⟩ is the empty language.

Lemma test_compatible_𝐓 _to_test_false : ¬ A ⊢ σ → ⟦⟨A ⟩⟧σ ≃ 0.

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.