Parse Trees for Chomsky Grammars

This file defines parse trees and proves the basic height and yield lemmas used in the pumping argument.

Main declarations

• yield_derives
• yield_length_le_two_pow_height
• subtree_height
• Derives.yield

inductive ChomskyNormalFormGrammar.parseTree {T : Type uT} {g : ChomskyNormalFormGrammar T} : g.NT → Type (max uN uT)

A parseTree n encodes a ChomskyNormalFormGrammar derivation of a word from a nonterminal n

• leaf {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} (t : T) (hnt : ChomskyNormalFormRule.leaf n t ∈ g.rules) : parseTree n

  Single rule application transforming a nonterminal into a terminal.

• node {T : Type uT} {g : ChomskyNormalFormGrammar T} {n c₁ c₂ : g.NT} (t₁ : parseTree c₁) (t₂ : parseTree c₂) (hnc : ChomskyNormalFormRule.node n c₁ c₂ ∈ g.rules) : parseTree n

  Application of rule of the second kind.

def ChomskyNormalFormGrammar.parseTree.yield {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} (p : parseTree n) : List T

The yield of a tree is the word the tree derives

Equations

• (ChomskyNormalFormGrammar.parseTree.leaf t hnt).yield = [t]
• (t₁.node t₂ hnc).yield = t₁.yield ++ t₂.yield

def ChomskyNormalFormGrammar.parseTree.height {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} (p : parseTree n) : ℕ

The height of a tree

Equations

• (ChomskyNormalFormGrammar.parseTree.leaf t hnt).height = 1
• (t₁.node t₂ hnc).height = max t₁.height t₂.height + 1

inductive ChomskyNormalFormGrammar.parseTree.IsSubtreeOf {T : Type uT} {g : ChomskyNormalFormGrammar T} {n₁ n₂ : g.NT} : parseTree n₁ → parseTree n₂ → Prop

IsSubTreeOf p₁ p₂ encodes that p₁ is a subtree of p₂

• eq {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} (p : parseTree n) : p.IsSubtreeOf p

  A parse tree is a subtree of itself

• left_sub {T : Type uT} {g : ChomskyNormalFormGrammar T} {l r n₁ n₂ : g.NT} (p₁ : parseTree l) (p₂ : parseTree r) (p : parseTree n₂) (hrn₁ : ChomskyNormalFormRule.node n₁ l r ∈ g.rules) (hpp₁ : p.IsSubtreeOf p₁) : p.IsSubtreeOf (p₁.node p₂ hrn₁)

  If p₁ is a subtree of p₂, it is also a subtree of node p₂ p₃

• right_sub {T : Type uT} {g : ChomskyNormalFormGrammar T} {l r n₁ n₂ : g.NT} (p₁ : parseTree l) (p₂ : parseTree r) (p : parseTree n₂) (hrn₁ : ChomskyNormalFormRule.node n₁ l r ∈ g.rules) (hpp₂ : p.IsSubtreeOf p₂) : p.IsSubtreeOf (p₁.node p₂ hrn₁)

  If p₁ is a subtree of p₃, it is also a subtree of node p₂ p₃

theorem ChomskyNormalFormGrammar.parseTree.yield_derives {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} {p : parseTree n} : g.Derives [Symbol.nonterminal n] (List.map Symbol.terminal p.yield)

theorem ChomskyNormalFormGrammar.parseTree.height_pos {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} {p : parseTree n} : p.height > 0

theorem ChomskyNormalFormGrammar.parseTree.yield_length_le_two_pow_height {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} {p : parseTree n} : p.yield.length ≤ 2 ^ (p.height - 1)

theorem ChomskyNormalFormGrammar.parseTree.yield_length_pos {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} {p : parseTree n} : p.yield.length > 0

theorem ChomskyNormalFormGrammar.parseTree.subtree_decomposition {T : Type uT} {g : ChomskyNormalFormGrammar T} {n₁ n₂ : g.NT} {p₁ : parseTree n₁} {p₂ : parseTree n₂} (hpp : p₂.IsSubtreeOf p₁) : ∃ (u : List T) (v : List T), p₁.yield = u ++ p₂.yield ++ v ∧ g.Derives [Symbol.nonterminal n₁] (List.map Symbol.terminal u ++ [Symbol.nonterminal n₂] ++ List.map Symbol.terminal v)

theorem ChomskyNormalFormGrammar.parseTree.strict_subtree_decomposition {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} {p₁ p₂ : parseTree n} (hpp : p₂.IsSubtreeOf p₁) (hne : p₁ ≠ p₂) : ∃ (u : List T) (v : List T), p₁.yield = u ++ p₂.yield ++ v ∧ (u ++ v).length > 0 ∧ g.Derives [Symbol.nonterminal n] (List.map Symbol.terminal u ++ [Symbol.nonterminal n] ++ List.map Symbol.terminal v)

theorem ChomskyNormalFormGrammar.parseTree.IsSubtreeOf.refl {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} {p : parseTree n} : p.IsSubtreeOf p

theorem ChomskyNormalFormGrammar.parseTree.IsSubtreeOf.trans {T : Type uT} {g : ChomskyNormalFormGrammar T} {n₁ n₂ n₃ : g.NT} {p₁ : parseTree n₁} {p₂ : parseTree n₂} {p₃ : parseTree n₃} (hp₁ : p₁.IsSubtreeOf p₂) (hp₂ : p₂.IsSubtreeOf p₃) : p₁.IsSubtreeOf p₃

theorem ChomskyNormalFormGrammar.parseTree.subtree_height {T : Type uT} {g : ChomskyNormalFormGrammar T} {n₁ n₂ : g.NT} {p₁ : parseTree n₁} {p₂ : parseTree n₂} (hpp : p₁.IsSubtreeOf p₂) : p₁.height ≤ p₂.height

theorem ChomskyNormalFormGrammar.Produces.rule {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} {u : List (Symbol T g.NT)} (hnu : g.Produces [Symbol.nonterminal n] u) : ∃ r ∈ g.rules, r.input = n ∧ r.output = u

theorem ChomskyNormalFormGrammar.DerivesIn.terminal_refl {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v : List T} {m : ℕ} (huv : g.DerivesIn (List.map Symbol.terminal u) (List.map Symbol.terminal v) m) : u = v

theorem ChomskyNormalFormGrammar.Derives.yield {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : g.NT} {u : List T} (hnu : g.Derives [Symbol.nonterminal n] (List.map Symbol.terminal u)) : ∃ (p : parseTree n), p.yield = u