# Library LangAlg.expr

This module defines the full signature of language algebra we consider here, and its finite complete axiomatization. We also define here some normalisation functions, and list some of their properties.

Set Implicit Arguments.

Require Export tools language.

Delimit Scope expr_scope with expr.
Open Scope expr_scope.

Section s.

# Main definitions

Variable X : Set.
Variable dec_X : decidable_set X.

𝐄 X is the type of expressions with variables ranging over the type X. They are built out of the constants 0 and 1, the concatenation (also called sequential product) , the intersection , the union + and the mirror image, denoted by the postfix operator °.
Inductive 𝐄 : Set :=
| 𝐄_one : 𝐄
| 𝐄_zero : 𝐄
| 𝐄_var : X 𝐄
| 𝐄_seq : 𝐄 𝐄 𝐄
| 𝐄_inter : 𝐄 𝐄 𝐄
| 𝐄_plus : 𝐄 𝐄 𝐄
| 𝐄_conv : 𝐄 𝐄.

Notation "x ⋅ y" := (𝐄_seq x y) (at level 40) : expr_scope.
Notation "x + y" := (𝐄_plus x y) (left associativity, at level 50) : expr_scope.
Notation "x ∩ y" := (𝐄_inter x y) (at level 45) : expr_scope.
Notation "x °" := (𝐄_conv x) (at level 25) : expr_scope.
Notation " 1 " := 𝐄_one : expr_scope.
Notation " 0 " := 𝐄_zero : expr_scope.

The size of an expression is the number of nodes in its syntax tree.
Global Instance size_𝐄 : Size 𝐄 :=
fix 𝐄_size (e: 𝐄) : nat :=
match e with
| 0 | 1 | 𝐄_var _ ⇒ 1%nat
| e + f | e f | e fS (𝐄_size e + 𝐄_size f)
| e°S (𝐄_size e)
end.

If the set of variables X is decidable, then so is the set of expressions. Note that we are here considering syntactic equality, as no semantic or axiomatic equivalence relation has been defined for expressions.
Global Instance 𝐄_decidable_set : decidable_set 𝐄.

The following are the axioms of the algebra of languages over this signature.
Inductive ax : 𝐄 𝐄 Prop :=

⟨𝐄,⋅,1⟩ is a monoid.
| ax_seq_assoc e f g : ax (e⋅(f g)) ((ef)⋅g)
| ax_seq_1 e : ax (1e) e
| ax_1_seq e : ax (e1) e

⟨𝐄,+,0⟩ is a commutative idempotent monoid.
| ax_plus_com e f : ax (e+f) (f+e)
| ax_plus_idem e : ax (e+e) e
| ax_plus_ass e f g : ax (e+(f+g)) ((e+f)+g)
| ax_plus_0 e : ax (e+0) e

⟨𝐄,⋅,+,1,0⟩ is an idempotent semiring.
| ax_seq_0 e : ax (e0) 0
| ax_0_seq e : ax (0e) 0
| ax_plus_seq e f g: ax ((e + f)⋅g) (eg + fg)
| ax_seq_plus e f g: ax (e⋅(f + g)) (ef + eg)

⟨𝐄,∩⟩ is a commutative and idempotent semigroup.
| ax_inter_assoc e f g : ax (e∩(f g)) ((ef)∩g)
| ax_inter_comm e f : ax (ef) (fe)
| ax_inter_idem e : ax (e e) e

⟨𝐄,+,∩⟩ forms a distributive lattice, and 0 is absorbing for .
| ax_plus_inter e f g: ax ((e + f)∩g) (eg + fg)
| ax_inter_plus e f : ax ((ef)+e) e
| ax_inter_0 e : ax (e0) 0

° is an involution that flips concatenations and commutes with every other operation.
| ax_conv_conv e : ax (e°°) e
| ax_conv_1 : ax (1°) 1
| ax_conv_0 : ax (0°) 0
| ax_conv_plus e f: ax ((e + f) (e° + f°)
| ax_conv_seq e f: ax ((e f) (f° e°)
| ax_conv_inter e f: ax ((ef) (e° f°)

The four laws that follow are the most interesting ones. They concern subunits, terms that are smaller than 1. With our signature, any term can be projected to a subunit using the operation 1 _ .
• For subunits, intersection and concatenation coincide.
| ax_inter_1_seq e f : ax (1 (ef)) (1 (e f))

• Mirror image is the identity on subunits.
| ax_inter_1_conv e : ax (1 (e°)) (1 e)

• Subunits commute with every term.
| ax_inter_1_comm_seq e f : ax ((1 e)⋅f) (f⋅(1 e))

• This last law is less intuitive, but with the previous ones, it allows one to extract from any union-free expressions a single global subunit.
| ax_inter_1_inter e f g : ax (((1 e)⋅f) g) ((1 e)⋅(f g)).

We use these axioms to generate an axiomatic equivalence relation and an axiomatic order relations.
Inductive 𝐄_eq : Equiv 𝐄 :=
| eq_refl e : e e
| eq_trans f e g : e f f g e g
| eq_sym e f : e f f e
| eq_plus e f g h : e g f h (e + f) (g + h)
| eq_seq e f g h : e g f h (e f) (g h)
| eq_inter e f g h : e g f h (e f) (g h)
| eq_conv e f : e f (e°) (f°)
| eq_ax e f : ax e f e f.
Global Instance 𝐄_Equiv : Equiv 𝐄 := 𝐄_eq.

For the order to match the equivalence relation, we need to add this axiom, stating that 0 is a minimal element.
Inductive 𝐄_inf : Smaller 𝐄 :=
| inf_refl e : e e
| inf_trans f e g : e f f g e g
| inf_plus e f g h : e g f h (e + f) (g + h)
| 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)
| inf_conv e f : e f (e°) (f°)
| inf_ax e f : ax e f ax f e e f
| inf_zero e : 0 e.
Global Instance 𝐄_Smaller : Smaller 𝐄 := 𝐄_inf.

Hint Constructors 𝐄_eq ax 𝐄_inf.

# Some elementary properties of this algebra

It is immediate to check that the equivalence we defined is indeed an equivalence relation, that the order relation is a preorder, and that every operator is monotone for both relations.
Global Instance equiv_Equivalence : Equivalence equiv.

Global Instance smaller_PreOrder : PreOrder smaller.

Global Instance inter_equiv :
Proper (equiv ==> equiv ==> equiv) 𝐄_inter.

Global Instance plus_equiv :
Proper (equiv ==> equiv ==> equiv) 𝐄_plus.

Global Instance seq_equiv :
Proper (equiv ==> equiv ==> equiv) 𝐄_seq.

Global Instance conv_equiv :
Proper (equiv ==> equiv) 𝐄_conv.

Global Instance inter_smaller :
Proper (smaller ==> smaller ==> smaller) 𝐄_inter.

Global Instance plus_smaller :
Proper (smaller ==> smaller ==> smaller) 𝐄_plus.

Global Instance seq_smaller :
Proper (smaller ==> smaller ==> smaller) 𝐄_seq.

Global Instance conv_smaller :
Proper (smaller ==> smaller) 𝐄_conv.

From the axioms, we can infer the following simple laws.
Lemma equiv_0_inter e : (0e) 0.

Lemma inter_plus e f g : (e∩(f + g)) (ef + eg).

Lemma inf_ax_inter_l e f : e f e.

Lemma inf_ax_inter_r e f : e f f.

We can now prove that if e is smaller than f, then their union must be equal to f.
Lemma smaller_equiv e f : e f e + f f.

This allows us to prove that the order we defined is indeed antisymmetric with respect to .
We now strengthen our earlier lemma, by proving the following reduction from ordering to equivalence.
Lemma smaller_equiv_iff_plus e f : e f e + f f.

Mirror is actually more than monotone, it is bijective.
Lemma smaller_conv_iff e f :
e f e° f°.

We establish few properties of subunits.
Lemma inter_1_abs e f : ((1 e)⋅(1 f)) (1 (e f)).

Lemma inter_onel e : (1 e + (1 e)⋅e) ((1 e)⋅e).

Lemma inter_oner e : (1 e + e⋅(1 e)) (e⋅(1 e)).

Using these, we get a second reduction from ordering to equivalence, relying on intersection rather than union.
Lemma smaller_equiv_iff_inter e f : e f e f e.

A product is larger than 1 if and only if both its arguments are.
Lemma split_one e f : 1 ef 1 e 1 f.

# Sum of a list of elements

The expression [e1;e2;...;en] is e1+(e2+...(en+0)...)
Definition sum := fold_right 𝐄_plus 0.
Notation " ⋃ l " := (sum l) (at level 30).

This operator satisfies some simple distributivity properties.
Lemma sum_app l m : (l++m) l + m.

Lemma seq_distr l m : l m (bimap (fun e f : 𝐄e f) l m).

Lemma inter_distr l m : l m bimap (fun e f : 𝐄e f) l m.

If lm, then l m
If a appears in m, then the following identity holds:
Lemma split_list a m :
a m m a + rm a m.

# Normalisation of expressions

An expression is called a term if it doesn't contain unions or 0, and if ° only appears on variables.
Fixpoint is_term (e : 𝐄) : bool :=
match e with
| 1 | 𝐄_var _ | (𝐄_var _true
| e f | e fis_term e && is_term f
| _° | _ + _ | 0 ⇒ false
end.

comb e true produces a list of terms whose sum is equal to e. Here is the definition of comb:
Fixpoint comb e (dir : bool) :=
match e with
| 0 ⇒ []
| 1 ⇒ 
| e + fcomb e dir ++ comb f dir
| e fbimap (fun e fe f) (comb e dir) (comb f dir)
| e °comb e (negb dir)
| 𝐄_var aif dir then [𝐄_var a] else [𝐄_var a°]
| e f
if dir
then bimap (fun e fe f) (comb e dir) (comb f dir)
else bimap (fun e fe f) (comb f dir) (comb e dir)
end.

We prove the claim that indeed every expression in comb e d is a term.
Lemma is_term_comb e d u : u (comb e d) is_term u = true.

We can now verify the second claim, that e is equal to the sum of comb e true.
Lemma comb_equiv e : e comb e true.

Close Scope expr_scope.
End s.

Infix " ⋅ " := 𝐄_seq (at level 40) : expr_scope.
Infix " + " := 𝐄_plus (left associativity, at level 50) : expr_scope.
Infix " ∩ " := 𝐄_inter (at level 45) : expr_scope.
Notation "x °" := (𝐄_conv x) (at level 25) : expr_scope.
Notation " 1 " := 𝐄_one : expr_scope.
Notation " 0 " := 𝐄_zero : expr_scope.
Notation "⋃ l " := (sum l) (at level 30).

Section language.

# Language interpretation

Context { X : Set }.

We interpret expressions as languages in the obvious way:
Global Instance to_lang_𝐄 {Σ}: semantics 𝐄 language X Σ :=
fix to_lang_𝐄 σ e:=
match e with
| 1 ⇒ 1%lang
| 0 ⇒ 0%lang
| 𝐄_var a ⇒ (σ a)
| e + f ⇒ ((to_lang_𝐄 σ e) + (to_lang_𝐄 σ f))%lang
| e f ⇒ ((to_lang_𝐄 σ e) (to_lang_𝐄 σ f))%lang
| e f ⇒ ((to_lang_𝐄 σ e) (to_lang_𝐄 σ f))%lang
| e°(to_lang_𝐄 σ e%lang
end.

This interpretation is sound in the sense that axiomatically equivalent expressions are semantically equivalent. Differently put, the axioms we imposed hold in every algebra of languages.
Theorem 𝐄_eq_equiv_lang : e f : 𝐄 X, e f e f.

This extends to ordering as well.
Lemma 𝐄_inf_incl_lang (e f : 𝐄 X) : e f e f.

A word is in the language of a sum if and only if it is in the language of one of its components.
Lemma sum_lang l Σ (σ:𝕬[XΣ]) w :
(w l σ) ( t : 𝐄 X, t l ( t σ) w).

Thus we may find for every word in the language of e a term in comb e true containing that word.
Lemma comb_lang e Σ (σ:𝕬[XΣ]) w :
w (eσ) t, t (comb e true) w (tσ).

End language.