Partial derivation trees (fragments) for context-free grammars

@cite{odonnell-2015}

A fragment of a context-free grammar g is a partial derivation tree some of whose leaves are nonterminal "open slots" rather than terminal symbols. Fragments are the units of storage in fragment grammars (@cite{odonnell-2015} §2.3.6) and adaptor grammars (§2.3.4): a fragment-grammar analysis of an utterance partitions the full derivation tree into fragments stored in memoized Pitman–Yor tables.

This file provides the partial-tree data type and the embedding from CFGTree (which represents complete derivations only).

Main definitions

• CFGFragment T N — a derivation tree some of whose leaves are open NT slots rather than terminals. Internal nodes carry an N, leaves carry a Symbol T N.
• CFGFragment.yieldT / yieldNT — terminal yield (ignoring open slots) and open-slot list, both left-to-right.
• CFGFragment.isComplete — true iff the fragment has no open slots.
• CFGFragment.ofCFGTree — embedding of complete derivations.

Relation to CFGTree

CFGTree T N is a derivation tree where every leaf carries a terminal T. CFGFragment T N allows leaves to carry either a terminal T or an open nonterminal N. Every CFGTree embeds as a complete CFGFragment via ofCFGTree; the inverse projection (complete fragment → CFGTree) and the round-trip theorems are deferred to a Phase 3 file when fragment-grammar composition needs them.

References

• @cite{odonnell-2015} §2.3.6 (fragment grammars), §3.1.5 (DOP prefix function).
• Mathlib.Computability.ContextFreeGrammar for the Symbol T N sum type used at leaves.

inductive CFGFragment (T N : Type) : Type

A partial derivation tree of a CFG: leaves carry a Symbol T N (terminal or open nonterminal slot); internal nodes carry an N and a list of children.

• leaf {T N : Type} (s : Symbol T N) : CFGFragment T N

  Leaf carrying either a terminal or an open NT slot.

• node {T N : Type} (nt : N) (children : List (CFGFragment T N)) : CFGFragment T N

  Internal node with nonterminal label and children.

def CFGFragment.yieldT {T N : Type} : CFGFragment T N → List T

Terminal yield, ignoring open NT slots, left to right.

Equations

• (CFGFragment.leaf (Symbol.terminal t)).yieldT = [t]
• (CFGFragment.leaf (Symbol.nonterminal n)).yieldT = []
• (CFGFragment.node nt cs).yieldT = CFGFragment.yieldTList cs

def CFGFragment.yieldTList {T N : Type} : List (CFGFragment T N) → List T

Concatenated terminal yields of a list of fragments.

Equations

• CFGFragment.yieldTList [] = []
• CFGFragment.yieldTList (f :: fs) = f.yieldT ++ CFGFragment.yieldTList fs

def CFGFragment.yieldNT {T N : Type} : CFGFragment T N → List N

The list of open NT slots at the leaves, left to right.

Equations

• (CFGFragment.leaf (Symbol.terminal t)).yieldNT = []
• (CFGFragment.leaf (Symbol.nonterminal n)).yieldNT = [n]
• (CFGFragment.node nt cs).yieldNT = CFGFragment.yieldNTList cs

def CFGFragment.yieldNTList {T N : Type} : List (CFGFragment T N) → List N

Concatenated open-slot lists of a list of fragments.

Equations

• CFGFragment.yieldNTList [] = []
• CFGFragment.yieldNTList (f :: fs) = f.yieldNT ++ CFGFragment.yieldNTList fs

def CFGFragment.isComplete {T N : Type} : CFGFragment T N → Bool

true iff the fragment has no open NT slots — i.e. it is a complete derivation tree.

Equations

• (CFGFragment.leaf (Symbol.terminal t)).isComplete = true
• (CFGFragment.leaf (Symbol.nonterminal n)).isComplete = false
• (CFGFragment.node nt cs).isComplete = CFGFragment.isCompleteList cs

def CFGFragment.isCompleteList {T N : Type} : List (CFGFragment T N) → Bool

true iff every fragment in the list is complete.

Equations

• CFGFragment.isCompleteList [] = true
• CFGFragment.isCompleteList (f :: fs) = (f.isComplete && CFGFragment.isCompleteList fs)

def CFGFragment.ofCFGTree {T N : Type} : CFGTree T N → CFGFragment T N

Embed a CFGTree (which has only terminal leaves) as a complete CFGFragment.

Equations

• CFGFragment.ofCFGTree (CFGTree.leaf t) = CFGFragment.leaf (Symbol.terminal t)
• CFGFragment.ofCFGTree (CFGTree.node nt cs) = CFGFragment.node nt (CFGFragment.ofCFGTreeList cs)

def CFGFragment.ofCFGTreeList {T N : Type} : List (CFGTree T N) → List (CFGFragment T N)

Pointwise lift of ofCFGTree to lists.

Equations

• CFGFragment.ofCFGTreeList [] = []
• CFGFragment.ofCFGTreeList (t :: ts) = CFGFragment.ofCFGTree t :: CFGFragment.ofCFGTreeList ts

theorem CFGFragment.ofCFGTree_isComplete {T N : Type} (t : CFGTree T N) : (ofCFGTree t).isComplete = true

ofCFGTree always produces a complete fragment.

theorem CFGFragment.ofCFGTreeList_isCompleteList {T N : Type} (ts : List (CFGTree T N)) : isCompleteList (ofCFGTreeList ts) = true

List version of ofCFGTree_isComplete.

theorem CFGFragment.yieldT_ofCFGTree {T N : Type} (t : CFGTree T N) : (ofCFGTree t).yieldT = t.yield

Yields agree under the ofCFGTree embedding.

theorem CFGFragment.yieldTList_ofCFGTreeList {T N : Type} (ts : List (CFGTree T N)) : yieldTList (ofCFGTreeList ts) = CFGTree.yieldList ts

List version of yieldT_ofCFGTree.

theorem CFGFragment.yieldNT_ofCFGTree {T N : Type} (t : CFGTree T N) : (ofCFGTree t).yieldNT = []

The embedding produces no open slots.

theorem CFGFragment.yieldNTList_ofCFGTreeList {T N : Type} (ts : List (CFGTree T N)) : yieldNTList (ofCFGTreeList ts) = []

List version of yieldNT_ofCFGTree.