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 ⋅ f ⇒ S (𝐄 _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 )) ((e ⋅f )⋅g)
  | ax_seq_1 e : ax (1⋅e) e
  | ax_1_seq e : ax (e ⋅1) 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 (e ⋅0) 0
  | ax_0_seq e : ax (0⋅e) 0
  | ax_plus_seq e f g: ax ((e + f )⋅g) (e ⋅g + f ⋅g)
  | ax_seq_plus e f g: ax (e ⋅(f + g )) (e ⋅f + e ⋅g)

⟨𝐄,∩⟩ is a commutative and idempotent semigroup.

  | 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

⟨𝐄,+,∩⟩ forms a distributive lattice, and 0 is absorbing for ∩.

  | ax_plus_inter e f g: ax ((e + f )∩g) (e ∩g + f ∩g)
  | ax_inter_plus e f : ax ((e ∩f )+e) e
  | ax_inter_0 e : ax (e ∩0) 0

° is an involution that flips concatenations and commutes with every other operation.

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 ∩ (e ⋅f )) (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 : (0∩e ) ≡ 0.

  Lemma inter_plus e f g : (e ∩(f + g )) ≡ (e ∩f + e ∩g ).

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

Global Instance smaller_PartialOrder : PartialOrder equiv smaller.

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 ≤ e ⋅f ↔ 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 l⊆m, then ⋃ l ≤ ⋃ m

Lemma fold_right_incl_smaller :
Proper ((@incl 𝐄 ) ==> smaller) (fold_right 𝐄 _plus 0).

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 ∩ f ⇒ is_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 ⇒ [1]
    | e + f ⇒ comb e dir ++ comb f dir
    | e ∩ f ⇒ bimap (fun e f ⇒ e ∩ f) (comb e dir) (comb f dir)
    | e ° ⇒ comb e (negb dir)
    | 𝐄 _var a ⇒ if dir then [𝐄 _var a] else [𝐄 _var a°]
    | e ⋅ f ⇒
      if dir
      then bimap (fun e f ⇒ e ⋅ f) (comb e dir) (comb f dir)
      else bimap (fun e f ⇒ e ⋅ 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.