% $Id: Grammar.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
%
% Finite context-free grammars.
[Dragon]
Grammar: trait
includes
List(Symbol, String for List[E]), % assumes list?
Set(Symbol, FiniteSet[Symbol] for Set[E]),
RelSet(String, Set[String]),
Set(Rule, FiniteSet[Rule] for Set[E]),
Relation(String, Rel[String],
__ \< __ \> __ for __ 〈 __ 〉 __,
bot for ⊥, top for ⊤)
Rule tuple of lhs: Symbol, rhs: String
Grammar tuple of start: Symbol, terminals: FiniteSet[Symbol],
rules: FiniteSet[Rule]
introduces
derives1: Grammar → Rel[String]
derives: Grammar → Rel[String]
L: Grammar → Set[String]
stringsOver: FiniteSet[Symbol] → Set[String]
__ ⇒ __ : Symbol, String → Rule
asserts
∀ A: Symbol, alpha, beta, gamma, w: String,
G: Grammar, sigma: FiniteSet[Symbol]
w ∈ L(G) = (({G.start}) \< derives(G) \> w)
∧ w ∈ stringsOver(G.terminals);
derives(G) = derives1(G) \superplus;
[A, gamma] ∈ G.rules ⇒
(alpha||{A}||beta) \< derives1(G) \> (alpha||gamma||beta);
empty ∈ stringsOver(sigma);
({A} || w) ∈ stringsOver(sigma) = (A ∈ sigma ∧
w ∈ stringsOver(sigma));
(A ⇒ gamma) ∈ G.rules ⇒ A \notin G.terminals;
(A ⇒ gamma) = [A, gamma];
[Index]
HTML generated using lsl2html.