Derivation trees of a context-free grammar

A derivation tree, or parse tree, of a context-free grammar is a rose tree over its symbols, RoseTree (Symbol T N). A grammar licenses a tree when every terminal node is a leaf and every nonterminal node, read with the symbols of its children, is a rule: the trees a grammar licenses are the local set of its rules (RoseTree.Licensed). The yield of a tree is the list of terminals at its leaves, left to right.

Main definitions

• RoseTree.yield: the terminal frontier.
• ContextFreeGrammar.Licenses g: the local trees the grammar g licenses.
• RoseTree.ruleCount, RoseTree.corpusRuleCount: the number of applications of a rule in a tree and in a corpus of trees.
• RoseTree.ruleAt?: the rule applied at a Gorn address.

Main results

• RoseTree.Licensed.derives: a licensed tree derives its yield from its root symbol.
• ContextFreeGrammar.exists_licensed_tree: every word of the language has a licensed derivation tree from the start symbol.
• RoseTree.Licensed.replaceAt, RoseTree.Licensed.exists_repeat: replacing a subtree by one with the same root symbol keeps the tree licensed, and a long enough path in a licensed tree passes two nodes with the same nonterminal; together with RoseTree.numNodes_replaceAt_lt these are the ingredients of the pumping lemma.

The yield

def RoseTree.yield {T : Type u_1} {N : Type u_2} (t : RoseTree (Symbol T N)) : List T

The terminal frontier of a tree lists the terminals among its leaves, left to right.

Equations

• t.yield = List.filterMap Symbol.terminal? t.leafList

@[simp]

theorem RoseTree.yield_node_nil {T : Type u_1} {N : Type u_2} (s : Symbol T N) : (node s []).yield = s.terminal?.toList

@[simp]

theorem RoseTree.yield_leaf {T : Type u_1} {N : Type u_2} (s : Symbol T N) : (leaf s).yield = s.terminal?.toList

theorem RoseTree.yield_node_of_ne_nil {T : Type u_1} {N : Type u_2} (s : Symbol T N) {cs : List (RoseTree (Symbol T N))} (h : cs ≠ []) : (node s cs).yield = (List.map yield cs).flatten

@[simp]

theorem RoseTree.yield_node_cons {T : Type u_1} {N : Type u_2} (s : Symbol T N) (c : RoseTree (Symbol T N)) (cs : List (RoseTree (Symbol T N))) : (node s (c :: cs)).yield = (List.map yield (c :: cs)).flatten

@[simp]

theorem RoseTree.yield_node_nonterminal {T : Type u_1} {N : Type u_2} (A : N) (cs : List (RoseTree (Symbol T N))) : (node (Symbol.nonterminal A) cs).yield = (List.map yield cs).flatten

@[simp]

theorem RoseTree.yield_map {T : Type u_1} {N : Type u_2} {N' : Type u_3} (f : N → N') (t : RoseTree (Symbol T N)) : (map (Symbol.mapNonterminal f) t).yield = t.yield

theorem RoseTree.yield_replaceAt {T : Type u_1} {N : Type u_2} {t s : RoseTree (Symbol T N)} {p : List ℕ} (h : t.subtreeAt p = some s) : ∃ (pre : List T) (post : List T), t.yield = pre ++ s.yield ++ post ∧ ∀ (new : RoseTree (Symbol T N)), (t.replaceAt p new).yield = pre ++ new.yield ++ post

Replacing inside the tree splits the yield into the terminals left of the address, the yield of the subtree there, and the terminals to its right.

Licensing

def ContextFreeGrammar.Licenses {T : Type u_1} (g : ContextFreeGrammar T) : Symbol T g.NT → List (Symbol T g.NT) → Prop

A grammar licenses a local tree when it is a terminal without children, or a nonterminal whose children's symbols are the right-hand side of one of its rules.

Equations

• g.Licenses (Symbol.terminal t) x✝ = (x✝ = [])
• g.Licenses (Symbol.nonterminal A) x✝ = ({ input := A, output := x✝ } ∈ g.rules)

theorem RoseTree.Licensed.terminal {T : Type u_1} {g : ContextFreeGrammar T} (a : T) : Licensed g.Licenses (leaf (Symbol.terminal a))

theorem RoseTree.Licensed.nonterminal {T : Type u_1} {g : ContextFreeGrammar T} (A : g.NT) (cs : List (RoseTree (Symbol T g.NT))) (hrule : { input := A, output := List.map value cs } ∈ g.rules) (hcs : ∀ c ∈ cs, Licensed g.Licenses c) : Licensed g.Licenses (node (Symbol.nonterminal A) cs)

theorem RoseTree.Licensed.rule_mem {T : Type u_1} {g : ContextFreeGrammar T} {A : g.NT} {cs : List (RoseTree (Symbol T g.NT))} (h : Licensed g.Licenses (node (Symbol.nonterminal A) cs)) : { input := A, output := List.map value cs } ∈ g.rules

theorem RoseTree.Licensed.eq_nil_of_terminal {T : Type u_1} {g : ContextFreeGrammar T} {a : T} {cs : List (RoseTree (Symbol T g.NT))} (h : Licensed g.Licenses (node (Symbol.terminal a) cs)) : cs = []

theorem RoseTree.Licensed.exists_nonterminal_of_ne_nil {T : Type u_1} {g : ContextFreeGrammar T} {s : Symbol T g.NT} {cs : List (RoseTree (Symbol T g.NT))} (h : Licensed g.Licenses (node s cs)) (hcs : cs ≠ []) : ∃ (A : g.NT), s = Symbol.nonterminal A

A node with children is a nonterminal node.

theorem RoseTree.Licensed.grammar_induction {T : Type u_1} {g : ContextFreeGrammar T} {motive : (t : RoseTree (Symbol T g.NT)) → Licensed g.Licenses t → Prop} (terminal : ∀ (a : T), motive (leaf (Symbol.terminal a)) ⋯) (nonterminal : ∀ (A : g.NT) (cs : List (RoseTree (Symbol T g.NT))) (hrule : { input := A, output := List.map value cs } ∈ g.rules) (hcs : ∀ c ∈ cs, Licensed g.Licenses c), (∀ (c : RoseTree (Symbol T g.NT)) (hc : c ∈ cs), motive c ⋯) → motive (node (Symbol.nonterminal A) cs) ⋯) {t : RoseTree (Symbol T g.NT)} (ht : Licensed g.Licenses t) : motive t ht

Induction over the trees a grammar licenses, by the two shapes it licenses.

Rule counts

def RoseTree.ruleCount {T : Type u_1} {N : Type u_2} [DecidableEq T] [DecidableEq N] (r : ContextFreeRule T N) (t : RoseTree (Symbol T N)) : ℕ

ruleCount r t counts the applications of the rule r in t, the nonterminal nodes whose symbol and children's symbols spell out r.

Equations

• RoseTree.ruleCount r t = List.count (Symbol.nonterminal r.input, r.output) t.localTrees

theorem RoseTree.ruleCount_node_nonterminal {T : Type u_1} {N : Type u_2} [DecidableEq T] [DecidableEq N] (r : ContextFreeRule T N) (A : N) (cs : List (RoseTree (Symbol T N))) : ruleCount r (node (Symbol.nonterminal A) cs) = (if r = { input := A, output := List.map value cs } then 1 else 0) + (List.map (ruleCount r) cs).sum

theorem RoseTree.ruleCount_node_terminal {T : Type u_1} {N : Type u_2} [DecidableEq T] [DecidableEq N] (r : ContextFreeRule T N) (a : T) (cs : List (RoseTree (Symbol T N))) : ruleCount r (node (Symbol.terminal a) cs) = (List.map (ruleCount r) cs).sum

def RoseTree.corpusRuleCount {T : Type u_1} {N : Type u_2} [DecidableEq T] [DecidableEq N] (r : ContextFreeRule T N) (D : Multiset (RoseTree (Symbol T N))) : ℕ

The number of applications of the rule r in a corpus of trees.

Equations

• RoseTree.corpusRuleCount r D = (Multiset.map (RoseTree.ruleCount r) D).sum

@[simp]

theorem RoseTree.corpusRuleCount_zero {T : Type u_1} {N : Type u_2} [DecidableEq T] [DecidableEq N] (r : ContextFreeRule T N) : corpusRuleCount r 0 = 0

@[simp]

theorem RoseTree.corpusRuleCount_singleton {T : Type u_1} {N : Type u_2} [DecidableEq T] [DecidableEq N] (r : ContextFreeRule T N) (t : RoseTree (Symbol T N)) : corpusRuleCount r {t} = ruleCount r t

theorem RoseTree.corpusRuleCount_add {T : Type u_1} {N : Type u_2} [DecidableEq T] [DecidableEq N] (r : ContextFreeRule T N) (D₁ D₂ : Multiset (RoseTree (Symbol T N))) : corpusRuleCount r (D₁ + D₂) = corpusRuleCount r D₁ + corpusRuleCount r D₂

The rule at an address

def RoseTree.ruleAt? {T : Type u_1} {g : ContextFreeGrammar T} (t : RoseTree (Symbol T g.NT)) (p : List ℕ) : Option (ContextFreeRule T g.NT)

The rule applied at a Gorn address is the nonterminal there with the symbols of its children, and none off the tree or at a terminal.

Equations

• One or more equations did not get rendered due to their size.

theorem RoseTree.ruleAt?_eq_some {T : Type u_1} {g : ContextFreeGrammar T} {t : RoseTree (Symbol T g.NT)} {p : List ℕ} {A : g.NT} {cs : List (RoseTree (Symbol T g.NT))} (h : t.subtreeAt p = some (node (Symbol.nonterminal A) cs)) : t.ruleAt? p = some { input := A, output := List.map value cs }

theorem RoseTree.Licensed.exists_subtreeAt_take {T : Type u_1} {g : ContextFreeGrammar T} {t : RoseTree (Symbol T g.NT)} (ht : Licensed g.Licenses t) {p : List ℕ} {s : RoseTree (Symbol T g.NT)} (hs : t.subtreeAt p = some s) (hh : 1 < s.height) {k : ℕ} (hk : k ≤ p.length) : ∃ (A : g.NT) (cs : List (RoseTree (Symbol T g.NT))), t.subtreeAt (List.take k p) = some (node (Symbol.nonterminal A) cs)

Along an address into a licensed tree, every proper prefix ends at a nonterminal node, and so does the address itself when the subtree there has children.

theorem RoseTree.Licensed.exists_repeat {T : Type u_1} {g : ContextFreeGrammar T} {t : RoseTree (Symbol T g.NT)} (ht : Licensed g.Licenses t) {p : List ℕ} {s : RoseTree (Symbol T g.NT)} (hs : t.subtreeAt p = some s) (hh : 1 < s.height) (hlen : g.rules.card ≤ p.length) : ∃ (i : ℕ) (j : ℕ), i < j ∧ j ≤ p.length ∧ ∃ (A : g.NT) (csᵢ : List (RoseTree (Symbol T g.NT))) (csⱼ : List (RoseTree (Symbol T g.NT))), t.subtreeAt (List.take i p) = some (node (Symbol.nonterminal A) csᵢ) ∧ t.subtreeAt (List.take j p) = some (node (Symbol.nonterminal A) csⱼ)

By pigeonhole, a path of at least g.rules.card steps through a licensed tree, ending at a node with children, passes two nodes with the same nonterminal.

theorem RoseTree.Licensed.exists_min_numNodes {T : Type u_1} {g : ContextFreeGrammar T} {t : RoseTree (Symbol T g.NT)} (ht : Licensed g.Licenses t) : ∃ (t' : RoseTree (Symbol T g.NT)), Licensed g.Licenses t' ∧ t'.yield = t.yield ∧ t'.value = t.value ∧ ∀ (t'' : RoseTree (Symbol T g.NT)), Licensed g.Licenses t'' → t''.yield = t.yield → t''.value = t.value → t'.numNodes ≤ t''.numNodes

Among the licensed trees with a given yield and root symbol there is one of least size.

Soundness and completeness

theorem RoseTree.Licensed.derives {T : Type u_1} {g : ContextFreeGrammar T} {t : RoseTree (Symbol T g.NT)} (ht : Licensed g.Licenses t) : g.Derives [t.value] (List.map Symbol.terminal t.yield)

Soundness. A licensed tree derives its yield from its root symbol.

theorem ContextFreeGrammar.exists_licensed_tree {T : Type u_1} (g : ContextFreeGrammar T) {w : List T} (hw : w ∈ g.language) : ∃ (t : RoseTree (Symbol T g.NT)), RoseTree.Licensed g.Licenses t ∧ t.yield = w ∧ t.value = Symbol.nonterminal g.initial

Completeness. Every word of the language has a licensed derivation tree from the start symbol.