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