RIS.language: Languages.

Set Implicit Arguments.

Require Import tools algebra.

Section lang.
Context {A : Set}.

Definitions

A language is a set of words, i.e. a predicate over lists.

Definition language := list A → Prop.

Two languages are equivalent if they agree on every word.

Global Instance eq_lang : SemEquiv language := fun l1 l2 ⇒ ∀ w, l1 w ↔ l2 w.

Languages may be ordered by containment.

  Global Instance inf_lang : SemSmaller language := fun l1 l2 ⇒ ∀ w, l1 w → l2 w.

  Global Instance eq_lang_equiv : Equivalence (@sequiv _ eq_lang).
  Global Instance inf_lang_preorder : PreOrder (@ssmaller _ inf_lang).
  Global Instance inf_lang_PartialOrder : PartialOrder sequiv (@ssmaller _ inf_lang).

The unit language only contains the empty word.

Global Instance unLang : Un language := (fun w ⇒ w =[]).

The empty language has no elements.

Global Instance zeroLang : Zero language := fun _ : list A ⇒ False.

From any two languages we may define their union and their concatenation.

Global Instance joinLang : Join language:= fun l1 l2 w ⇒ l1 w ∨ l2 w.
Global Instance prodLang : Product language := fun l1 l2 w ⇒ ∃ u v, w = u ++v ∧ l1 u ∧ l2 v.

We may iterate the product on a language for any number of times.

  Reserved Notation " l ^{ n } " (at level 35).
  Fixpoint iter_lang n l : language :=
    match n with
    | 0 ⇒ 𝟭
    | S n ⇒ l · (l ^{n })
    end
  where "l ^{ n }" := (iter_lang n l).

The Kleene star of a language is the union of its iterates.

Global Instance starLang : Star language := fun l w ⇒ ∃ n, l ^{n } w.

Compatibily of the operations with the ordering

Applying any of the operations we have defined to equivalent arguments yields equivalent results.

  Global Instance proper_joinLang : Proper (sequiv ==> sequiv ==> sequiv) join.

  Global Instance proper_prodLang : Proper (sequiv ==> sequiv ==> sequiv) prod.

  Global Instance inf_lang_iter_lang n :
    Proper (sequiv ==> sequiv) (iter_lang n).

  Global Instance proper_starLang : Proper (sequiv ==> sequiv) star.

Algebraic properties

The containment order is the natural order stemming from ∪.

Global Instance joinOrderLang : JoinOrder language sequiv ssmaller join.

The set of languages is a semi-ring.

Global Instance lang_Semiring : SemiRing language sequiv prod join un zero.

Remark iter_lang_last n l : l ^{S n } ≃ l ^{n } · l.

It is actually a Kleene algebra.

Global Instance lang_KA : KleeneAlgebra language sequiv ssmaller.

End lang.