Probabilistic context-free grammars

A probabilistic context-free grammar (PCFG) over G is a weight on the rules of G that sums to one over the rules expanding each nonterminal. The probability of a derivation tree is the product of the weights of the rules it applies, and the probability of a corpus, a multiset of derivation trees, is the product over its trees, so the corpus probability factorises over disjoint sub-corpora. Over licensed trees it also collects into a product over the grammar's rules of the rule weight raised to the corpus count of that rule.

Main definitions

• PCFG G: a WeightedCFG G ℝ≥0∞ vanishing off the grammar and normalised at each nonterminal the grammar expands.
• PCFG.derivProb, PCFG.corpusProb: the probability of a derivation tree, a RoseTree (Symbol T G.NT), and of a corpus.
• PCFG.uniform: the uniform rule distribution at every nonterminal.

Main results

• PCFG.corpusProb_add: corpus probability is multiplicative over disjoint corpora.
• PCFG.corpusProb_eq_prod_pow_count: over licensed trees, corpus probability is the product of rule weights raised to corpus rule counts.

Implementation notes

Weights are ℝ≥0∞, the scalar of MeasureTheory.Measure, and a rule outside the grammar has weight 0, so a tree applying such a rule has probability 0. derivProb is a weight on trees; the measure it is the singleton mass of, and tightness in the sense of [BT73] and [Chi99], are in Linglib.Core.Computability.ContextFreeGrammar.Measure.

References

• [BT73]
• [Chi99]

structure PCFG {T : Type u_1} (G : ContextFreeGrammar T) [DecidableEq G.NT] extends WeightedCFG G ENNReal : Type u_1

A probabilistic context-free grammar over G is a rule weight that vanishes off the grammar and sums to one over the rules with each left-hand side the grammar expands.

• weight : ContextFreeRule T G.NT → ENNReal
• weight_nonneg (r : ContextFreeRule T G.NT) : 0 ≤ self.weight r
• weight_eq_zero_of_not_mem (r : ContextFreeRule T G.NT) : r ∉ G.rules → self.weight r = 0

  Rules outside the grammar have weight 0.

• sum_weight (a : G.NT) : a ∈ Finset.image (fun (x : ContextFreeRule T G.NT) => x.input) G.rules → ∑ r ∈ G.rules with r.input = a, self.weight r = 1

  Weights sum to one over the rules with each left-hand side the grammar expands.

theorem PCFG.ext_iff {T : Type u_1} {G : ContextFreeGrammar T} {inst✝ : DecidableEq G.NT} {x y : PCFG G} : x = y ↔ x.weight = y.weight

theorem PCFG.ext {T : Type u_1} {G : ContextFreeGrammar T} {inst✝ : DecidableEq G.NT} {x y : PCFG G} (weight : x.weight = y.weight) : x = y

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

The weight of a node, read from its symbol and the symbols of its children, is the rule weight at a nonterminal, 1 at a childless terminal and 0 at a terminal with children.

Equations

• W.symbolWeight (Symbol.nonterminal A) x✝ = W.weight { input := A, output := x✝ }
• W.symbolWeight (Symbol.terminal t) [] = 1
• W.symbolWeight (Symbol.terminal t) (head :: tail) = 0

@[simp]

theorem PCFG.symbolWeight_nonterminal {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (A : G.NT) (syms : List (Symbol T G.NT)) : W.symbolWeight (Symbol.nonterminal A) syms = W.weight { input := A, output := syms }

@[simp]

theorem PCFG.symbolWeight_terminal_nil {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (a : T) : W.symbolWeight (Symbol.terminal a) [] = 1

@[simp]

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

noncomputable def PCFG.derivProb {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (t : RoseTree (Symbol T G.NT)) : ENNReal

The probability of a derivation tree is the product over its nodes of the weight of the rule applied there.

Equations

• W.derivProb t = (List.map (fun (p : Symbol T G.NT × List (Symbol T G.NT)) => W.symbolWeight p.1 p.2) t.localTrees).prod

theorem PCFG.derivProb_node {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (s : Symbol T G.NT) (cs : List (RoseTree (Symbol T G.NT))) : W.derivProb (RoseTree.node s cs) = W.symbolWeight s (List.map RoseTree.value cs) * (List.map W.derivProb cs).prod

noncomputable def PCFG.corpusProb {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (D : Multiset (RoseTree (Symbol T G.NT))) : ENNReal

The probability of a corpus is the product of the probabilities of its derivation trees.

Equations

• W.corpusProb D = (Multiset.map W.derivProb D).prod

@[simp]

theorem PCFG.corpusProb_zero {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) : W.corpusProb 0 = 1

theorem PCFG.corpusProb_add {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (D₁ D₂ : Multiset (RoseTree (Symbol T G.NT))) : W.corpusProb (D₁ + D₂) = W.corpusProb D₁ * W.corpusProb D₂

Corpus probability is multiplicative over disjoint corpora, since derivation trees are independent under a PCFG, in contrast to DirichletPCFG.corpusProb.

theorem PCFG.sum_weight_le_one {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) (A : G.NT) : ∑ r ∈ G.rules with r.input = A, W.weight r ≤ 1

theorem PCFG.derivProb_eq_prod_pow_ruleCount {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [DecidableEq T] {t : RoseTree (Symbol T G.NT)} (ht : RoseTree.Licensed G.Licenses t) : W.derivProb t = ∏ r ∈ G.rules, W.weight r ^ RoseTree.ruleCount r t

The probability of a licensed derivation tree is the product over the grammar's rules of the rule weight raised to the number of applications of that rule in the tree.

theorem PCFG.corpusProb_eq_prod_pow_count {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] (W : PCFG G) [DecidableEq T] (D : Multiset (RoseTree (Symbol T G.NT))) (h : ∀ t ∈ D, RoseTree.Licensed G.Licenses t) : W.corpusProb D = ∏ r ∈ G.rules, W.weight r ^ RoseTree.corpusRuleCount r D

Over licensed derivation trees, corpus probability is the product over the grammar's rules of the rule weight raised to the corpus count of that rule.

noncomputable def PCFG.uniform {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] [DecidableEq T] : PCFG G

The uniform PCFG puts the uniform distribution over its rules at every nonterminal.

Equations

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

@[instance_reducible]

noncomputable instance PCFG.instInhabited {T : Type u_1} {G : ContextFreeGrammar T} [DecidableEq G.NT] [DecidableEq T] : Inhabited (PCFG G)

Equations

• PCFG.instInhabited = { default := PCFG.uniform }