Flag scopes in normal-form indexed parse trees

This file formalizes the scope construction used in Gilman's shrinking lemma. For one occurrence in the root flag stack, NFParse.scopeAt follows every branch until that occurrence is consumed. Its ordered frontier consists of terminals and of the continuation parses immediately below the consuming pop. Carrying those continuation parses makes both the frontier derivation and the corresponding factorization of the terminal yield explicit.

Reference

• R. H. Gilman, "A shrinking lemma for indexed languages", Theoretical Computer Science 163 (1996), 277--281.

inductive IndexedGrammar.ScopePiece {T : Type} (g : IndexedGrammar T) (suffix : List g.flag) : Type

One leaf of a flag scope. A pending leaf remembers the complete parse below the pop which consumed the distinguished flag occurrence.

• terminal {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (a : T) : g.ScopePiece suffix
• pending {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} {A : g.nt} {w : List T} (parse : g.NFParse A suffix w) : g.ScopePiece suffix

def IndexedGrammar.ScopePiece.word {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} : g.ScopePiece suffix → List T

The terminal factor contributed by one scope-frontier leaf.

Equations

• (IndexedGrammar.ScopePiece.terminal a).word = [a]
• (IndexedGrammar.ScopePiece.pending parse).word = w

def IndexedGrammar.ScopePiece.symbol {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} : g.ScopePiece suffix → g.nt ⊕ T

The unstacked sentential symbol displayed by a scope-frontier leaf.

Equations

• (IndexedGrammar.ScopePiece.terminal a).symbol = Sum.inr a
• (IndexedGrammar.ScopePiece.pending parse).symbol = Sum.inl A

def IndexedGrammar.ScopePiece.asISym {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} : g.ScopePiece suffix → g.ISym

Interpret a scope piece as an indexed-grammar sentential symbol.

Equations

• (IndexedGrammar.ScopePiece.terminal a).asISym = IndexedGrammar.ISym.terminal a
• (IndexedGrammar.ScopePiece.pending parse).asISym = IndexedGrammar.ISym.indexed A suffix

@[simp]

theorem IndexedGrammar.ScopePiece.word_terminal {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (a : T) : (terminal a).word = [a]

@[simp]

theorem IndexedGrammar.ScopePiece.word_pending {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} {A : g.nt} {w : List T} (p : g.NFParse A suffix w) : (pending p).word = w

@[simp]

theorem IndexedGrammar.ScopePiece.symbol_terminal {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (a : T) : (terminal a).symbol = Sum.inr a

@[simp]

theorem IndexedGrammar.ScopePiece.symbol_pending {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} {A : g.nt} {w : List T} (p : g.NFParse A suffix w) : (pending p).symbol = Sum.inl A

@[simp]

theorem IndexedGrammar.ScopePiece.asISym_terminal {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (a : T) : (terminal a).asISym = ISym.terminal a

@[simp]

theorem IndexedGrammar.ScopePiece.asISym_pending {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} {A : g.nt} {w : List T} (p : g.NFParse A suffix w) : (pending p).asISym = ISym.indexed A suffix

theorem IndexedGrammar.ScopePiece.word_ne_nil {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (piece : g.ScopePiece suffix) : piece.word ≠ []

def IndexedGrammar.NFParse.scopeAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) (k : ℕ) : List (g.ScopePiece (List.drop (k + 1) sigma))

Cut a concrete parse at the first consumption of the root-stack occurrence numbered k. The remaining stack below that occurrence is sigma.drop (k + 1), which is exactly the stack carried by pending frontier leaves.

Equations

• (IndexedGrammar.NFParse.binary hr hlhs hc hrhs left right).scopeAt k = left.scopeAt k ++ right.scopeAt k
• (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest).scopeAt 0 = [IndexedGrammar.ScopePiece.pending rest]
• (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest).scopeAt k_2.succ = rest.scopeAt k_2
• (IndexedGrammar.NFParse.push hr hlhs hc hrhs rest).scopeAt k = rest.scopeAt (k + 1)
• (IndexedGrammar.NFParse.terminal hr hlhs hc hrhs).scopeAt k = [IndexedGrammar.ScopePiece.terminal a]

def IndexedGrammar.NFParse.scopeWord {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (pieces : List (g.ScopePiece suffix)) : List T

Concatenate the terminal factors represented by a scope frontier.

Equations

• IndexedGrammar.NFParse.scopeWord pieces = List.flatMap IndexedGrammar.ScopePiece.word pieces

def IndexedGrammar.NFParse.scopeSymbols {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (pieces : List (g.ScopePiece suffix)) : List (g.nt ⊕ T)

Forget continuation certificates and retain the unstacked frontier word.

Equations

• IndexedGrammar.NFParse.scopeSymbols pieces = List.map IndexedGrammar.ScopePiece.symbol pieces

def IndexedGrammar.NFParse.unstackedForm {T : Type} {g : IndexedGrammar T} (beta : List (g.nt ⊕ T)) : List g.ISym

Interpret an unstacked frontier word as a sentential form.

Equations

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

def IndexedGrammar.NFParse.scopeForm {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (pieces : List (g.ScopePiece suffix)) : List g.ISym

Interpret a scope frontier at the concrete suffix carried by its pieces.

Equations

• IndexedGrammar.NFParse.scopeForm pieces = List.map IndexedGrammar.ScopePiece.asISym pieces

@[simp]

theorem IndexedGrammar.NFParse.scopeWord_nil {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} : scopeWord [] = []

@[simp]

theorem IndexedGrammar.NFParse.scopeWord_cons {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (piece : g.ScopePiece suffix) (pieces : List (g.ScopePiece suffix)) : scopeWord (piece :: pieces) = piece.word ++ scopeWord pieces

@[simp]

theorem IndexedGrammar.NFParse.scopeWord_append {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (left right : List (g.ScopePiece suffix)) : scopeWord (left ++ right) = scopeWord left ++ scopeWord right

@[simp]

theorem IndexedGrammar.NFParse.scopeSymbols_length {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (pieces : List (g.ScopePiece suffix)) : (scopeSymbols pieces).length = pieces.length

@[simp]

theorem IndexedGrammar.NFParse.scopeForm_eq_appendStackSuffixes_unstackedForm {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (pieces : List (g.ScopePiece suffix)) : scopeForm pieces = appendStackSuffixes suffix (unstackedForm (scopeSymbols pieces))

theorem IndexedGrammar.NFParse.scopeWord_scopeAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) (k : ℕ) : scopeWord (p.scopeAt k) = w

Cutting a scope partitions, but never changes, the terminal yield.

theorem IndexedGrammar.NFParse.derives_scopeWord {T : Type} {g : IndexedGrammar T} {suffix : List g.flag} (pieces : List (g.ScopePiece suffix)) : g.Derives (scopeForm pieces) (List.map (fun (a : T) => ISym.terminal a) (scopeWord pieces))

Independently finish every pending scope piece.

theorem IndexedGrammar.NFParse.derives_scopeForm_scopeAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) (k : ℕ) : g.Derives [ISym.indexed A sigma] (scopeForm (p.scopeAt k))

The concrete parse derives its scope frontier at the suffix below the distinguished occurrence.

theorem IndexedGrammar.NFParse.derives_unstackedForm_scopeAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) (k : ℕ) : g.Derives [ISym.indexed A (List.take (k + 1) sigma)] (unstackedForm (scopeSymbols (p.scopeAt k)))

Remove the common suffix below a scope. The same rule certificates derive the unstacked frontier from the prefix ending at the distinguished occurrence.

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

Gilman's beta(p): the full terminal yield at an empty stack, and the unstacked frontier of the top flag scope at a nonempty stack.

Equations

• p_2.beta = List.map Sum.inr w
• p_2.beta = IndexedGrammar.NFParse.scopeSymbols (p_2.scopeAt 0)

def IndexedGrammar.NFParse.betaPieces {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) : List (g.ScopePiece sigma.tail)

The concrete scope pieces whose symbol word is beta. At an empty stack the pieces are the individual terminal leaves.

Equations

• p_2.betaPieces = List.map IndexedGrammar.ScopePiece.terminal w
• p_2.betaPieces = p_2.scopeAt 0

@[simp]

theorem IndexedGrammar.NFParse.scopeSymbols_betaPieces {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) : scopeSymbols p.betaPieces = p.beta

@[simp]

theorem IndexedGrammar.NFParse.scopeWord_betaPieces {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) : scopeWord p.betaPieces = w

@[simp]

theorem IndexedGrammar.NFParse.betaPieces_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) : p.betaPieces.length = p.beta.length

def IndexedGrammar.NFParse.betaSource {T : Type} {g : IndexedGrammar T} (A : g.nt) (sigma : List g.flag) : List g.ISym

The one-symbol source from which beta is derived.

Equations

• IndexedGrammar.NFParse.betaSource A [] = [IndexedGrammar.ISym.indexed A []]
• IndexedGrammar.NFParse.betaSource A (f :: tail) = [IndexedGrammar.ISym.indexed A [f]]

@[simp]

theorem IndexedGrammar.NFParse.appendStackSuffixes_tail_betaSource {T : Type} {g : IndexedGrammar T} (A : g.nt) (sigma : List g.flag) : appendStackSuffixes sigma.tail (betaSource A sigma) = [ISym.indexed A sigma]

theorem IndexedGrammar.NFParse.derives_beta {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) : g.Derives (betaSource A sigma) (unstackedForm p.beta)

Every parse-tree beta word is derivable from its unstacked source.

theorem IndexedGrammar.NFParse.derives_scopeWord_of_derives_unstacked {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {x : List (g.nt ⊕ T)} (hder : g.Derives (betaSource A sigma) (unstackedForm x)) (kept : List (g.ScopePiece sigma.tail)) (hkept : scopeSymbols kept = x) : g.Derives [ISym.indexed A sigma] (List.map (fun (a : T) => ISym.terminal a) (scopeWord kept))

A derivable unstacked subfrontier can be reattached to the concrete suffix and its surviving pieces can then finish their original parses.

@[simp]

theorem IndexedGrammar.NFParse.beta_length_of_empty {T : Type} {g : IndexedGrammar T} {A : g.nt} {w : List T} (p : g.NFParse A [] w) : p.beta.length = w.length

theorem IndexedGrammar.NFParse.beta_length_eq_yield_of_stack_eq_nil {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) (hstack : sigma = []) : p.beta.length = w.length

@[simp]

theorem IndexedGrammar.NFParse.beta_length_of_nonempty {T : Type} {g : IndexedGrammar T} {A : g.nt} {f : g.flag} {suffix : List g.flag} {w : List T} (p : g.NFParse A (f :: suffix) w) : p.beta.length = (p.scopeAt 0).length

theorem IndexedGrammar.NFParse.beta_length_eq_scopeAt_zero_of_stack_ne_nil {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) (hstack : sigma ≠ []) : p.beta.length = (p.scopeAt 0).length

@[simp]

theorem IndexedGrammar.NFParse.beta_binary {T : Type} {g : IndexedGrammar 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) : (binary hr hlhs hc hrhs left right).beta = left.beta ++ right.beta

@[simp]

theorem IndexedGrammar.NFParse.beta_pop {T : Type} {g : IndexedGrammar 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) : (pop hr hlhs hc hrhs rest).beta = [Sum.inl B]

@[simp]

theorem IndexedGrammar.NFParse.beta_terminal {T : Type} {g : IndexedGrammar 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]) : (terminal hr hlhs hc hrhs).beta = [Sum.inr a]

@[simp]

theorem IndexedGrammar.NFParse.beta_length_push_empty {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : 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] w) : (push hr hlhs hc hrhs rest).beta.length = w.length

@[simp]

theorem IndexedGrammar.NFParse.beta_length_push_nonempty {T : Type} {g : IndexedGrammar T} {A B : g.nt} {pushed top : 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 = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some pushed)]) (rest : g.NFParse B (pushed :: top :: suffix) w) : (push hr hlhs hc hrhs rest).beta.length = (rest.scopeAt 1).length