Theory of regular expressions

module Regexp

  type char

Syntax

  type regexp =
    | Empty
    | Epsilon
    | Char    char
    | Alt     regexp regexp
    | Concat  regexp regexp
    | Star    regexp

Semantics

Words are sequences of characters.

  use seq.Seq
  use seq.FreeMonoid
  use int.Int

  type word = seq char

Inductive predicate mem w r means "word w belongs to the language of r".

  inductive mem (w: word) (r: regexp) =
    | mem_eps:
        mem empty Epsilon
    | mem_char:
        forall c: char. mem (singleton c) (Char c)
    | mem_altl:
        forall w: word, r1 r2: regexp. mem w r1 -> mem w (Alt r1 r2)
    | mem_altr:
        forall w: word, r1 r2: regexp. mem w r2 -> mem w (Alt r1 r2)
    | mem_concat:
        forall w1 w2: word, r1 r2: regexp.
        mem w1 r1 -> mem w2 r2 -> mem (w1 ++ w2) (Concat r1 r2)
    | mems1:
        forall r: regexp. mem empty (Star r)
    | mems2:
        forall w1 w2: word, r: regexp.
        mem w1 r -> mem w2 (Star r) -> mem (w1 ++ w2) (Star r)

Optimizing constructors for Alt and Concat

  let alt (r1 r2: regexp) : regexp
    ensures { forall w: word. mem w result <-> mem w (Alt r1 r2) }
  = match r1, r2 with
    | Empty, _ -> r2
    | _, Empty -> r1
    | _        -> Alt r1 r2
    end

  let concat (r1 r2: regexp) : regexp
    ensures { forall w: word. mem w result <-> mem w (Concat r1 r2) }
  = match r1, r2 with
    | Empty, _   -> Empty
    | _, Empty   -> Empty
    | Epsilon, _ -> r2
    | _, Epsilon -> r1
    | _          -> Concat r1 r2
    end

end