Weighted context-free grammars #
A weighted context-free grammar over G attaches a nonnegative weight to each rule of G, with
no normalisation; the normalised specialisations are PCFG, whose weights in ℝ≥0∞ sum to one at
each nonterminal, and DirichletPCFG, whose pseudo-counts are positive on the rules of the
grammar. The weight type is a parameter, as for Polynomial R, so a consumer chooses ℝ,
ℝ≥0∞ or any ordered type with a zero.
structure
WeightedCFG
{T : Type u_1}
(G : ContextFreeGrammar T)
(W : Type u_2)
[Zero W]
[LE W]
:
Type (max u_1 u_2)
A weighted context-free grammar over G with weights in W: a nonnegative weight on rules,
with no normalisation.
- weight : ContextFreeRule T G.NT → W
The weight of a rule.
- weight_nonneg (r : ContextFreeRule T G.NT) : 0 ≤ self.weight r
Weights are nonnegative.
Instances For
theorem
WeightedCFG.ext
{T : Type u_1}
{G : ContextFreeGrammar T}
{W : Type u_2}
{inst✝ : Zero W}
{inst✝¹ : LE W}
{x y : WeightedCFG G W}
(weight : x.weight = y.weight)
:
x = y
theorem
WeightedCFG.ext_iff
{T : Type u_1}
{G : ContextFreeGrammar T}
{W : Type u_2}
{inst✝ : Zero W}
{inst✝¹ : LE W}
{x y : WeightedCFG G W}
: