Library RelationAlgebra.gregex


gregex: generalised typed regular expressions, for KAT

we define a typed syntax for KAT expressions:
  • typed because we have to prove KAT completeness at the typed level
  • generalised w.r.t. regular expressions since it has to embeds Boolean expressions, for tests

Require Import lsyntax glang kat boolean atoms sups.
Set Implicit Arguments.

Generalised regular expressions


Section s.

I is the set of objects of the category (or types, or indices)
Notation I := positive.
Sigma is the set of (Kleene) variables, those interpreted as relations, for instance
Notation Sigma := positive.
pred is the number of predicate variables (elementary tests), so that tests are just expressions with variables in ord pred
Variable pred: nat.
src and tgt assign a type to each Kleene variable
Variables src tgt: Sigma I.
Note that we do not type elementary tests: we shall actually prove a specific untyping theorem about KAT which makes this possible
generalised regular expressions are just typed regular expressions, with an additional constructor, g_prd, for embedding Boolean expressions
Inductive gregex: I I Set :=
| g_zer: {n m}, gregex n m
| g_prd: {n} (a: expr (ord pred)), gregex n n
| g_var: (i: Sigma), gregex (src i) (tgt i)
| g_pls: n m (e f: gregex n m), gregex n m
| g_dot: n m p (e: gregex n m) (f: gregex m p), gregex n p
| g_itr: n (e: gregex n n), gregex n n.

1 is derived, as the injection of the top expression
Definition g_one {n} := @g_prd n e_top.

Also note that g_itr is chosen as primitive, rather than g_str
Definition g_str n (e: gregex n n) := g_pls g_one (g_itr e).

Interpretation into an arbitrary Kleene algebra with tests


Section e.

to interpret an expressions, we need:
  • a KAT X,
  • an interpretation fo of syntactic types (I)
  • a properly typed interpretation fs of each Kleene variable
  • an interpretation fp of each predicate variable into the tests of X, at each type n
(consider for instance, the expression p*a*q, with a: X n m, p: tst n, q: tst m, which can be represented by the term @g_prd 1 (e_var 1) × g_var 1 × @g_prd 2 (e_var 1), with the environments fo(1)=n, fo(2)=m, fs(1)=1, fp(1)(1)=p, fp(2)(1)=q).
Context {X: kat.ops}.
Variable fo: I ob X.
Variable fp: n, ord pred tst (fo n).
Variable fs: i, X (fo (src i)) (fo (tgt i)).

Fixpoint eval n m (e: gregex n m): X (fo n) (fo m) :=
  match e with
    | g_zer ⇒ 0
    | @g_prd n p[lsyntax.eval (fp n) p]
    | g_pls e feval e + eval f
    | g_dot e feval e × eval f
    | g_itr eeval e ^+
    | g_var ifs i
  end.

End e.

generalised regular expressions form a model of KAT

(in)equalitiy on gregex is defined as a smallest fixed-point, impredicatevely
Definition g_leq n m (x y: gregex n m) :=
   X (L: kat.laws X) fo fp fa, @eval X fo fp fa n m x <== @eval X fo fp fa n m y.
Definition g_weq n m (x y: gregex n m) :=
   X (L: kat.laws X) fo fp fa, @eval X fo fp fa n m x == @eval X fo fp fa n m y.

packing all operations using canonical structures
Canonical Structure gregex_lattice_ops n m := {|
  car := gregex n m;
  leq := @g_leq n m;
  weq := @g_weq n m;
  cup := @g_pls n m;
  bot := @g_zer n m;
  cap := assert_false (@g_pls n m);
  top := assert_false (@g_zer n m);
  neg := assert_false id
|}.

Canonical Structure gregex_monoid_ops := {|
  ob := I;
  mor := gregex_lattice_ops;
  dot := g_dot;
  one := @g_one;
  itr := g_itr;
  str := g_str;
  cnv n m := assert_false (fun _ bot);
  ldv n m p := assert_false (fun _ _ bot);
  rdv n m p := assert_false (fun _ _ bot)
|}.

Canonical Structure gregex_kat_ops :=
  kat.mk_ops gregex_monoid_ops (fun nexpr_ops _ BL) (@g_prd).

lattice laws
Global Instance gregex_lattice_laws n m: lattice.laws BKA (gregex_lattice_ops n m).
Proof.
  constructor; try right; try discriminate. constructor.
   intros x X L fo fa fs. reflexivity.
   intros x y z H H' X L fo fa fs. transitivity (eval fo fa fs y); auto.
   intros x y. split.
    intro H. split; intros X L fo fa fs. now apply weq_leq, H. now apply weq_geq, H.
    intros [H H'] X L fo fa fs. apply antisym; auto.
   intros Hl x y z. split.
    intro H. split; intros X L fo fa fs; specialize (H X L fo fa fs); simpl in H; hlattice.
    intros [H H'] X L fo fa fs. simpl. apply cup_spec; auto.
   intros x X L fo fa fs. apply leq_bx.
Qed.

kleene algebra laws
Global Instance gregex_monoid_laws: monoid.laws BKA gregex_monoid_ops.
Proof.
  constructor; (try discriminate); repeat right; repeat intro; simpl.
   apply gregex_lattice_laws.
   apply dotA.
   rewrite inj_top. apply dot1x.
   rewrite inj_top. apply dotx1.
   apply dot_leq; auto.
   now rewrite dotplsx.
   now rewrite dotxpls.
   now rewrite dot0x.
   now rewrite dotx0.
   lattice.
   rewrite inj_top, <-str_itr. apply str_cons.
   rewrite inj_top, <-str_itr. apply str_ind_l. now refine (H0 _ _ _ _ _).
   rewrite inj_top, <-str_itr. apply str_ind_r. now refine (H0 _ _ _ _ _).
   rewrite inj_top, <-str_itr. apply itr_str_l.
Qed.

KAT laws
Global Instance gregex_kat_laws: kat.laws gregex_kat_ops.
Proof.
  constructor. apply gregex_monoid_laws. intro. apply lower_lattice_laws.
  constructor; try discriminate; repeat intro.
  apply inj_leq, H, tst_BL.
  apply inj_weq, H, tst_BL.
  apply inj_cup.
  apply inj_bot.
  reflexivity.
  repeat intro. apply inj_cap.
Qed.

additional properties of the injection (g_prd)
Definition inj_cup := @inj_cup _ gregex_kat_laws.
Definition inj_bot := @inj_bot _ gregex_kat_laws.
Definition inj_cap := @inj_cap _ gregex_kat_laws.
Definition inj_top := @inj_top _ gregex_kat_laws.
Definition inj_weq := @inj_weq _ gregex_kat_laws.
Definition inj_leq := @inj_leq _ gregex_kat_laws.

Lemma inj_sup n I J (f: I expr_ BL): @g_prd n (sup f J) == \sup_(i\in J) g_prd (f i).
Proof. apply f_sup_weq. apply inj_bot. apply inj_cup. Qed.

Interpretation in the guarded strings model

atoms are functions from predicate variables to bool
Notation Atom := (ord (pow2 pred)).
guarded string languages, typed according to the src and tgt functions
Notation glang n m := (tglang_kat_ops pred src tgt n m).

injection of atoms
Notation g_atom n a := (@g_prd n (atom a)).

(guarded string) language of a generalised regular expression. unlike for regular expressions, we define it inductively
Definition lang: n m, gregex_kat_ops n m glang n m :=
  eval id (fun _ ⇒ @e_var _) ttsingle.

this interpretation function is a KA morphism, by definition

Global Instance lang_leq n m: Proper (leq ==> leq) (@lang n m).
Proof. intros e f H. apply H. apply tglang_kat_laws. Qed.
Global Instance lang_weq n m: Proper (weq ==> weq) (@lang n m) := op_leq_weq_1.

Lemma lang_0 n m: @lang n m 0 = 0.
Proof. reflexivity. Qed.

Lemma lang_1 n: @lang n n 1 == 1.
Proof. intros [|]; simpl; intuition. Qed.

Lemma lang_pls n m (e f: gregex n m): lang (e+f) = lang e + lang f.
Proof. reflexivity. Qed.

Lemma lang_dot n m p (e: gregex n m) (f: gregex m p): lang (e×f) = lang e × lang f.
Proof. reflexivity. Qed.

Lemma lang_itr n (e: gregex n n): lang (e^+) = lang e^+.
Proof. reflexivity. Qed.

Lemma lang_sup n m I J (f: I _): @lang n m (sup f J) = \sup_(i\in J) lang (f i).
Proof. apply f_sup_eq; now f_equal. Qed.

languages of atoms

Lemma lang_atom n a: lang (g_atom n a) == tatom n a.
Proof.
  intros [b|]. 2: intros; compute; intuition discriminate.
  simpl. setoid_rewrite eval_var.
  split. intros H. now apply eval_atom in H as <-.
  intro E. injection E. clear E. intros <-.
  unfold atom. rewrite eval_inf.
  rewrite is_true_inf. intros i _.
  case_eq (set.mem a i); simpl; intros ->; reflexivity.
Qed.

End s.
Arguments g_var {pred src tgt} i.