% $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.