Library LangAlg.language

Basics of languages.

Set Implicit Arguments.

Require Export tools.
Delimit Scope lang_scope with lang.


A language over the alphabet Σ is a predicate over lists of Σ.
Definition language := fun (Σ : Set) ⇒ list Σ → Prop.

Notation " x ⋵ L " := ((L : language _) x) (at level 60).

Section defs.
  Hypothesis Σ : Set.

We define the equality and containment of language as follows:
  Global Instance lang_eq : SemEquiv (language Σ) :=
    fun l m ⇒ ∀ w, w ⋵ l ↔ w ⋵ m.

  Global Instance lang_incl : SemSmaller (language Σ) :=
    fun l m ⇒ ∀ w, w ⋵ l → w ⋵ m.

Equality is an equivalence relation, and containment is a partial order.
  Global Instance lang_eq_Equivalence : Equivalence sequiv.

  Global Instance lang_incl_PreOrder : PreOrder ssmaller.

  Global Instance lang_incl_PartialOrder :
    PartialOrder sequiv ssmaller.

We now define the elementary operations on languages.
  Definition prod (l m : language Σ) : language Σ:=
    fun w ⇒ ∃ u v, u ⋵ l ∧ v ⋵ m ∧ w = u++v.

  Definition union (l m : language Σ) : language Σ:=
    fun w ⇒ w ⋵ l ∨ w ⋵ m.

  Definition intersection (l m : language Σ) : language Σ:=
    fun w ⇒ w ⋵ l ∧ w ⋵ m.

  Definition mirror (l : language Σ) : language Σ:=
    fun w ⇒ (rev w) ⋵ l.

  Definition unit : language Σ := fun w ⇒ w = [].

  Definition empty : language Σ := fun _ ⇒ False.

These operations are monotone.
  Global Instance prod_lang_incl :
    Proper (ssmaller ==> ssmaller ==> ssmaller) prod.

  Global Instance union_lang_incl :
    Proper (ssmaller ==> ssmaller ==> ssmaller) union.

  Global Instance intersection_lang_incl :
    Proper (ssmaller ==> ssmaller ==> ssmaller) intersection.

  Global Instance mirror_lang_incl :
    Proper (ssmaller ==> ssmaller) mirror.

  Global Instance union_lang_eq :
    Proper (sequiv ==> sequiv ==> sequiv) union.

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

  Global Instance intersection_lang_eq :
    Proper (sequiv ==> sequiv ==> sequiv) intersection.

  Global Instance mirror_lang_eq :
    Proper (sequiv ==> sequiv) mirror.

End defs.

The empty words belongs to a language exactly when it belongs to its mirror image.
Lemma mirror_nil {Σ : Set} (L : language Σ) : mirror L [] ↔ L [].

An assignment of type X→Σ is a map from variables in X to languages over Σ.
Definition assignment (X Σ : Set) := X → language Σ.

Notation " 𝕬[ X → Σ ] " := (assignment X Σ).
σ is test-compatible with A, written A ⊢ σ, if for every variable a in A the empty list belongs to σ(a).
Definition test_compatible {Σ X} (σ : 𝕬[X→Σ]) (A : list X) :=
  ∀ a : X, a ∈ A → [] ⋵ σ a.

Notation " A ⊢ σ " := (test_compatible σ A) (at level 70).

Being test-compatible with a concatenation of two lists means being compatible with both lists.
Lemma test_compatible_app {Σ X} A B (σ : 𝕬[X→Σ]): A++B ⊢ σ ↔ A ⊢ σ ∧ B ⊢ σ.