% $Id: RegExp.lsl,v 1.3 2000/01/17 21:33:40 connolly Exp $

[Dragon] % "Regular Expressions", p 94

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

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

        L: Exp ® Set[String]

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

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

        L(empty) = {empty};
        L([A]) = {{A}};
        L(e \U f) = L(e) \U 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 \U empty;
        e \+ = e || (e\*);

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

[Index]

[source]

HTML generated using lsl2html.