The derivation measure of a probabilistic context-free grammar

A PCFG is a multitype Galton–Watson process whose types are the symbols: a terminal has no offspring, and a nonterminal's offspring is the right-hand side of a rule at it chosen with its weight. The law of the family tree is the law of the derivation tree, and the product of rule weights PCFG.derivProb is the Galton–Watson weight of the tree, so it is derived from the generation process rather than stipulated. Total mass one is tightness in the sense of [BT73] and [Chi99], consistency in older terminology: the grammar almost surely produces a finite derivation from every symbol.

Main definitions

• PCFG.galtonWatson: the offspring kernel of a PCFG.
• PCFG.derivationMeasure: the law of the derivation tree at each symbol, as a kernel.
• PCFG.IsTight: total mass one at every symbol.

Main results

• PCFG.galtonWatson_weight: the Galton–Watson weight of a tree is derivProb.
• PCFG.isMarkovKernel_galtonWatson: when every nonterminal has a rule, the offspring kernel is Markov.
• PCFG.derivationMeasure_singleton: a tree rooted at s has probability derivProb under the derivation measure at s, and trees rooted elsewhere have probability 0.
• PCFG.derivationMeasure_apply_univ_le_one: the derivation measure is a sub-probability kernel; PCFG.isTight_iff says it is Markov exactly when the grammar is tight.

References

• [BT73]
• [Chi99]
• [Koz81]

@[instance_reducible]

instance instMeasurableSpaceContextFreeRule_linglib {T : Type u_1} {N : Type u_2} : MeasurableSpace (ContextFreeRule T N)

Equations

• instMeasurableSpaceContextFreeRule_linglib = ⊤

@[instance_reducible]

instance instMeasurableSpaceSymbol_linglib {T : Type u_1} {N : Type u_2} : MeasurableSpace (Symbol T N)

Equations

• instMeasurableSpaceSymbol_linglib = ⊤

noncomputable def PCFG.ruleMeasure {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (A : G.NT) : MeasureTheory.Measure (ContextFreeRule T G.NT)

The rule distribution at nonterminal A, as a measure on rules.

Equations

• W.ruleMeasure A = ∑ r ∈ G.rules with r.input = A, W.weight r • MeasureTheory.Measure.dirac r

theorem PCFG.ruleMeasure_apply {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (A : G.NT) (s : Set (ContextFreeRule T G.NT)) : (W.ruleMeasure A) s = ∑ r ∈ G.rules with r.input = A, W.weight r * s.indicator 1 r

noncomputable def PCFG.offspring {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) : Symbol T G.NT → MeasureTheory.Measure (List (Symbol T G.NT))

The offspring of a symbol: none at a terminal, and at a nonterminal the right-hand side of a rule chosen with its weight.

Equations

• W.offspring (Symbol.terminal t) = MeasureTheory.Measure.dirac []
• W.offspring (Symbol.nonterminal A) = MeasureTheory.Measure.map ContextFreeRule.output (W.ruleMeasure A)

theorem PCFG.offspring_singleton {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (s : Symbol T G.NT) (syms : List (Symbol T G.NT)) : (W.offspring s) {syms} = W.symbolWeight s syms

theorem PCFG.offspring_nonterminal_univ {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (A : G.NT) : (W.offspring (Symbol.nonterminal A)) Set.univ = ∑ r ∈ G.rules with r.input = A, W.weight r

theorem PCFG.offspring_univ_le_one {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (s : Symbol T G.NT) : (W.offspring s) Set.univ ≤ 1

noncomputable def PCFG.galtonWatson {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] : ProbabilityTheory.Kernel (Symbol T G.NT) (List (Symbol T G.NT))

The branching process of a PCFG: the offspring kernel on symbols.

Equations

• W.galtonWatson = ProbabilityTheory.Kernel.ofFunOfCountable W.offspring

@[simp]

theorem PCFG.galtonWatson_apply {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] (s : Symbol T G.NT) : W.galtonWatson s = W.offspring s

theorem PCFG.isMarkovKernel_galtonWatson {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] (h : ∀ (A : G.NT), A ∈ Finset.image (fun (x : ContextFreeRule T G.NT) => x.input) G.rules) : ProbabilityTheory.IsMarkovKernel W.galtonWatson

A grammar with a rule at every nonterminal has a Markov offspring kernel.

theorem PCFG.galtonWatson_weight {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] (t : RoseTree (Symbol T G.NT)) : ProbabilityTheory.GaltonWatson.weight W.galtonWatson t = W.derivProb t

The Galton–Watson weight of a derivation tree is the product of its rule weights.

noncomputable def PCFG.derivationMeasure {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] : ProbabilityTheory.Kernel (Symbol T G.NT) (RoseTree (Symbol T G.NT))

The law of the derivation tree at each symbol: the law of the family tree of the grammar's branching process.

Equations

• W.derivationMeasure = ProbabilityTheory.GaltonWatson.law W.galtonWatson

theorem PCFG.derivationMeasure_singleton_value {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] (t : RoseTree (Symbol T G.NT)) : (W.derivationMeasure t.value) {t} = W.derivProb t

theorem PCFG.derivationMeasure_singleton_of_ne {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] {t : RoseTree (Symbol T G.NT)} {s : Symbol T G.NT} (h : t.value ≠ s) : (W.derivationMeasure s) {t} = 0

theorem PCFG.derivationMeasure_singleton {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] (t : RoseTree (Symbol T G.NT)) (s : Symbol T G.NT) : (W.derivationMeasure s) {t} = if t.value = s then W.derivProb t else 0

Under the derivation measure at s, a tree has probability derivProb when rooted at s and 0 otherwise.

theorem PCFG.derivationMeasure_apply_univ_le_one {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] (s : Symbol T G.NT) : (W.derivationMeasure s) Set.univ ≤ 1

The derivation measure is a sub-probability measure at every symbol.

instance PCFG.instIsFiniteKernelSymbolNTRoseTreeDerivationMeasure {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] : ProbabilityTheory.IsFiniteKernel W.derivationMeasure

def PCFG.IsTight {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] : Prop

A PCFG is tight when the derivation measure has total mass one at every symbol: the grammar almost surely produces a finite derivation from every nonterminal. Booth and Thompson call this consistency.

Equations

• W.IsTight = ∀ (s : Symbol T G.NT), ProbabilityTheory.GaltonWatson.extinctionProb W.galtonWatson s = 1

theorem PCFG.isTight_iff {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [Countable T] [Countable G.NT] : W.IsTight ↔ ProbabilityTheory.IsMarkovKernel W.derivationMeasure