Critical scopes in indexed parse trees

For a finite set Z of small frontier words, a critical parse node is the last node on some branch whose beta word lies outside Z. Thus its own frontier is large while every proper descendant has a frontier in Z. This file locates such a node and proves Gilman's quadratic bound on its frontier length.

inductive IndexedGrammar.NFParse.AllBetaIn {T : Type} {g : IndexedGrammar T} (Z : Set (List (g.nt ⊕ T))) {A : g.nt} {sigma : List g.flag} {w : List T} : g.NFParse A sigma w → Prop

Every parse node in p, including its root, has beta word in Z.

• binary {T : Type} {g : IndexedGrammar T} {Z : Set (List (g.nt ⊕ T))} {A B C : g.nt} {sigma : List g.flag} {u v : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]) (left : g.NFParse B sigma u) (right : g.NFParse C sigma v) (root : (NFParse.binary hr hlhs hc hrhs left right).beta ∈ Z) (leftAll : AllBetaIn Z left) (rightAll : AllBetaIn Z right) : AllBetaIn Z (NFParse.binary hr hlhs hc hrhs left right)
• pop {T : Type} {g : IndexedGrammar T} {Z : Set (List (g.nt ⊕ T))} {A B : g.nt} {f : g.flag} {suffix : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = some f) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none]) (rest : g.NFParse B suffix w) (root : (NFParse.pop hr hlhs hc hrhs rest).beta ∈ Z) (restAll : AllBetaIn Z rest) : AllBetaIn Z (NFParse.pop hr hlhs hc hrhs rest)
• push {T : Type} {g : IndexedGrammar T} {Z : Set (List (g.nt ⊕ T))} {A B : g.nt} {f : g.flag} {sigma : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]) (rest : g.NFParse B (f :: sigma) w) (root : (NFParse.push hr hlhs hc hrhs rest).beta ∈ Z) (restAll : AllBetaIn Z rest) : AllBetaIn Z (NFParse.push hr hlhs hc hrhs rest)
• terminal {T : Type} {g : IndexedGrammar T} {Z : Set (List (g.nt ⊕ T))} {A : g.nt} {sigma : List g.flag} {a : T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.terminal a]) (root : (NFParse.terminal hr hlhs hc hrhs).beta ∈ Z) : AllBetaIn Z (NFParse.terminal hr hlhs hc hrhs)

def IndexedGrammar.NFParse.ProperBetaIn {T : Type} {g : IndexedGrammar T} (Z : Set (List (g.nt ⊕ T))) {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) : Prop

Every proper descendant of the root of p has beta word in Z.

Equations

• IndexedGrammar.NFParse.ProperBetaIn Z (IndexedGrammar.NFParse.binary hr hlhs hc hrhs left right) = (IndexedGrammar.NFParse.AllBetaIn Z left ∧ IndexedGrammar.NFParse.AllBetaIn Z right)
• IndexedGrammar.NFParse.ProperBetaIn Z (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest) = IndexedGrammar.NFParse.AllBetaIn Z rest
• IndexedGrammar.NFParse.ProperBetaIn Z (IndexedGrammar.NFParse.push hr hlhs hc hrhs rest) = IndexedGrammar.NFParse.AllBetaIn Z rest
• IndexedGrammar.NFParse.ProperBetaIn Z (IndexedGrammar.NFParse.terminal hr hlhs hc hrhs) = True

def IndexedGrammar.NFParse.IsCritical {T : Type} {g : IndexedGrammar T} (Z : Set (List (g.nt ⊕ T))) {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) : Prop

A node outside Z all of whose proper descendants lie in Z.

Equations

• IndexedGrammar.NFParse.IsCritical Z p = (p.beta ∉ Z ∧ IndexedGrammar.NFParse.ProperBetaIn Z p)

theorem IndexedGrammar.NFParse.beta_mem_of_allBetaIn {T : Type} {g : IndexedGrammar T} {Z : Set (List (g.nt ⊕ T))} {A : g.nt} {sigma : List g.flag} {w : List T} {p : g.NFParse A sigma w} (h : AllBetaIn Z p) : p.beta ∈ Z

theorem IndexedGrammar.NFParse.properBetaIn_of_allBetaIn {T : Type} {g : IndexedGrammar T} {Z : Set (List (g.nt ⊕ T))} {A : g.nt} {sigma : List g.flag} {w : List T} {p : g.NFParse A sigma w} (h : AllBetaIn Z p) : ProperBetaIn Z p

structure IndexedGrammar.NFParse.LocatedCritical {T : Type} (g : IndexedGrammar T) (Z : Set (List (g.nt ⊕ T))) (rootNT : g.nt) (rootStack : List g.flag) (whole : List T) : Type

A critical subparse together with its position in the surrounding yield.

• leftContext : List T
• factor : List T
• rightContext : List T
• nt : g.nt
• stack : List g.flag
• parse : g.NFParse self.nt self.stack self.factor
• whole_eq : whole = self.leftContext ++ self.factor ++ self.rightContext
• critical : IsCritical Z self.parse
• rebuild {replacement : List T} : g.NFParse self.nt self.stack replacement → g.NFParse rootNT rootStack (self.leftContext ++ replacement ++ self.rightContext)

theorem IndexedGrammar.NFParse.exists_locatedCritical_of_not_allBetaIn {T : Type} {g : IndexedGrammar T} (Z : Set (List (g.nt ⊕ T))) {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) (hout : ¬AllBetaIn Z p) : Nonempty (LocatedCritical g Z A sigma w)

Every parse tree containing a beta word outside Z contains a last such node, located as a contiguous factor of the original yield.

The quadratic critical-frontier bound

theorem IndexedGrammar.NFParse.scopeAt_succ_length_le_of_allBetaIn {T : Type} {g : IndexedGrammar T} {Z : Set (List (g.nt ⊕ T))} {C : ℕ} (hC : 1 ≤ C) (hbound : ∀ z ∈ Z, z.length ≤ C) {A : g.nt} {sigma : List g.flag} {w : List T} {p : g.NFParse A sigma w} (hall : AllBetaIn Z p) (k : ℕ) (hk : k + 1 < sigma.length) : (p.scopeAt (k + 1)).length ≤ (p.scopeAt k).length * C

Advancing the cut from one inherited flag occurrence to the next expands the frontier by at most the uniform beta-word bound.

theorem IndexedGrammar.NFParse.yield_length_le_scopeAt_mul_of_bottom {T : Type} {g : IndexedGrammar T} {Z : Set (List (g.nt ⊕ T))} {C : ℕ} (hC : 1 ≤ C) (hbound : ∀ z ∈ Z, z.length ≤ C) {A : g.nt} {sigma : List g.flag} {w : List T} {p : g.NFParse A sigma w} (hall : AllBetaIn Z p) (k : ℕ) (hk : k < sigma.length) (hbottom : List.drop (k + 1) sigma = []) : w.length ≤ (p.scopeAt k).length * C

If the cut occurrence is the bottom flag, the terminal yield is at most C times the size of its scope frontier.

theorem IndexedGrammar.NFParse.beta_length_le_sq_of_critical {T : Type} {g : IndexedGrammar T} {Z : Set (List (g.nt ⊕ T))} {C : ℕ} (hC : 2 ≤ C) (hbound : ∀ z ∈ Z, z.length ≤ C) {A : g.nt} {sigma : List g.flag} {w : List T} {p : g.NFParse A sigma w} (hcritical : IsCritical Z p) : p.beta.length ≤ C * C

Gilman's critical-scope estimate: if every proper descendant has beta length at most C, then the critical beta word has length at most C^2.