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

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

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

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