A finite common basis for indexed-grammar scope frontiers

Gilman's marked Higman argument is applied separately to the finitely many sources A and Af. This file takes their finite union, adds all words of length at most one, and chooses one common length bound.

@[reducible, inline]

abbrev IndexedGrammar.NFParse.BetaKey {T : Type} (g : IndexedGrammar T) : Type

A source relevant to a beta word: either A or Af.

Equations

• IndexedGrammar.NFParse.BetaKey g = (g.nt × Option g.flag)

def IndexedGrammar.NFParse.betaKeyForm {T : Type} (g : IndexedGrammar T) (key : BetaKey g) : List g.ISym

Sentential form represented by a beta source key.

Equations

• IndexedGrammar.NFParse.betaKeyForm g key = match key.2 with | none => [IndexedGrammar.ISym.indexed key.1 []] | some f => [IndexedGrammar.ISym.indexed key.1 [f]]

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

The source key of a concrete parse node.

Equations

• IndexedGrammar.NFParse.betaKeyOf A sigma = (A, sigma.head?)

def IndexedGrammar.NFParse.frontierLanguage {T : Type} (g : IndexedGrammar T) (key : BetaKey g) : Set (List (g.nt ⊕ T))

All unstacked frontier words derivable from one source.

Equations

• IndexedGrammar.NFParse.frontierLanguage g key = {beta : List (g.nt ⊕ T) | g.Derives (IndexedGrammar.NFParse.betaKeyForm g key) (IndexedGrammar.NFParse.unstackedForm beta)}

@[simp]

theorem IndexedGrammar.NFParse.betaKeyForm_betaKeyOf {T : Type} {g : IndexedGrammar T} (A : g.nt) (sigma : List g.flag) : betaKeyForm g (betaKeyOf A sigma) = betaSource A sigma

theorem IndexedGrammar.NFParse.beta_mem_frontierLanguage {T : Type} {g : IndexedGrammar T} {A : g.nt} {sigma : List g.flag} {w : List T} (p : g.NFParse A sigma w) : p.beta ∈ frontierLanguage g (betaKeyOf A sigma)

theorem IndexedGrammar.NFParse.exists_globalRetainingBasis {T : Type} (g : IndexedGrammar T) [Fintype T] [Fintype g.nt] [Fintype g.flag] : ∃ (Z : Finset (List (g.nt ⊕ T))) (C : ℕ), 2 ≤ C ∧ (∀ z ∈ Z, z.length ≤ C) ∧ (∀ (z : List (g.nt ⊕ T)), z.length ≤ 1 → z ∈ Z) ∧ ∀ (key : BetaKey g), ∀ y ∈ frontierLanguage g key, y ∉ Z → ∀ (i : Fin y.length), ∃ x ∈ Z, x.length < y.length ∧ MarkedHigman.RetainsAt x y i ∧ x ∈ frontierLanguage g key

A common finite retaining basis for every source A and Af, together with a common bound C ≥ 2.