% $Id: BNF.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
BNF: trait
includes
Grammar,
RegExp
introduces
__ ..= __: Symbol, Exp → FiniteSet[Rule]
% ..= is poor-man's ::=
sym: Exp → Symbol
% an arbitrary symbol corresponding to a regexp
symbolsIn: Exp → FiniteSet[Symbol]
% the set of symbols mentioned in an expression
asserts
∀ A, B: Symbol, e, f: Exp
A ..= [B] = {A ⇒ {B}};
A ..= (e ∪ f) = (A ..= e) ∪ (A ..= f);
A ..= (e || f) = {A ⇒ {sym(e)} || {sym(f)}}
∪ (sym(e) ..= e)
∪ (sym(f) ..= f);
A ..= (e \*) = {A ⇒ empty} ∪ { A ⇒ ({A} || {sym(e)}) };
sym([B]) = B;
symbolsIn([A]) = {A};
symbolsIn(e ∪ f) = symbolsIn(e) ∪ symbolsIn(f);
symbolsIn(e || f) = symbolsIn(e) ∪ symbolsIn(f);
symbolsIn(e\*) = symbolsIn(e);
implies
forall A: Symbol, e: Exp, terminals: FiniteSet[Symbol]
A \notin terminals ∧ symbolsIn(e) \subseteq terminals ⇒
L([A, terminals, A ..= e]) = L(e);
[Index]
HTML generated using lsl2html.