% $Id: RegExp.html,v 1.1 2003/10/01 07:22:16 connolly Exp $

[Dragon] % "Regular Expressions", p 94

RegExp: trait
    includes
        Natural,
        AC(∪, Exp),
        Associative(__||__, Exp),
        List(Symbol, String for List[E]),
        RelSet(String, Set[String])

    introduces
        empty: → Exp
        [__] : Symbol → Exp
        __ ∪ __ : Exp, Exp → Exp
        __ || __ : Exp, Exp → Exp
        __ ^ __ : Exp, N → Exp
        __ \* : Exp → Exp
        __ \+ : Exp → Exp
        __ \? : Exp → Exp

        L: Exp → Set[String]

    asserts
        Exp generated by empty, [__], __ ∪ __, __ || __, __ \*

        ∀ A, B: Symbol, s, s1, s2: String, e, f: Exp, n: N

        L(empty) = {empty};
        L([A]) = {{A}};
        L(e ∪ f) = L(e) ∪ L(f);
        (s ∈ L(e || f)) = (∃ s1 ∃ s2 (s = s1 || s2
                                               ∧ s1 ∈ L(e)
                                          ∧ s2 ∈ L(f)));

        e ^ 0 = empty;
        e ^ (n+1) = e || (e^n);

        s ∈ L(e \*) = ∃ n (s ∈ L(e^n));

        e \? = e ∪ empty;
        e \+ = e || (e\*);

    implies
        Identity(empty for unit, || for \circ, String for T)
        forall r, s, t: Exp
            L(r\*) = L((r ∪ empty)\*);
            L(r\*\*) = L(r\*);
        converts __ \+, __ \?, __^__

[Index]


HTML generated using lsl2html.