Agenda-based Deduction¶

The concrete chart implementation used for DSL-compiled weighted deductions. DeductionSystem combines an axiom injector, a rule system, a semiring, and an agenda schedule in an nn.Module. DeductionSystem.__call__ returns the differentiable ChartView presheaf.

For fitting, sampling, and the NUTS wrapper, see api/stochastic/deduction.

Item algebra¶

Items, patterns, and bindings are plain tuples and dictionaries; these aliases name their roles in the signatures below.

Stochastic morphisms: Markov kernels over finite sets.

This module provides the probabilistic layer for quivers, implementing the category FinStoch of finite sets and stochastic maps (Markov kernels). This is the Kleisli category of the Giry monad restricted to finite sets, where:

Objects are finite sets (same as the base category).
Morphisms A -> B are stochastic matrices: tensors of shape (|A|, |B|) whose rows sum to 1.
Composition is standard matrix multiplication.
Identity is the Kronecker delta.

The package also re-exports MarkovAlgebra and its singleton MARKOV from quivers.core.algebras, the algebra these morphisms compose under.

Submodules

morphisms : StochasticMorphism, CategoricalMorphism families : Discretized distribution families transforms : condition, mix, factor, normalize queries : prob, marginal_prob, expectation giry : GiryMonad, FinStoch categories : Category types including atoms, slashes, products, unit, modals semiring : Chart semiring abstractions (LogProb, Viterbi, Boolean, Counting) schema : Composable rule schemas (functors CategorySystem -> RuleSystem) rules : Rule systems and the CCG / Lambek presets span : Span-based CKY components (LexicalAxiom, BinarySpanDeduction, etc.) parsers, ccg, lambek : Chart parsers inside : The inside algorithm over a rule system agenda : The agenda-driven weighted-deduction engine effect_lifts : Effect-lifted rule schemas for deduction systems deduction : Abstract weighted deductive system framework and its operations stdlib : Pre-registered deduction systems

Item `module-attribute` ¶

Item = tuple[Any, ...]

An item is a tuple of (constructor_name, *arguments).

The constructor name disambiguates item shapes; the remaining slots are the item's payload. Arguments may be other items (structural), strings (atoms), integers (positions / cardinals), or Wildcard placeholders in patterns.

Pattern `module-attribute` ¶

Pattern = tuple[Any, ...]

A pattern is an item-shaped tuple that may contain Wildcard positions. A pattern matches an item if (a) the constructor name matches, (b) the arities match, (c) each non-wildcard slot is structurally equal to the corresponding item slot, and (d) all wildcards with the same name bind to equal values.

Bindings `module-attribute` ¶

Bindings = dict[str, Any]

A bindings environment maps wildcard variable names to the values they captured during pattern-matching.

agenda ¶

Agenda-based weighted-deduction engine.

A general framework for evaluating weighted deductive systems by agenda-driven semi-naïve enumeration. Subsumes CKY, Earley, Viterbi, A* parsing, Knuth's algorithm, semi-naïve Datalog evaluation, and bidirectional MLTT type-checking under one runtime, parameterized by an Item algebra, a list of arity-n InferenceRule hyperedges, a ChartSemiring, an Agenda data structure, a priority function, and a goal predicate.

Categorical denotation: the chart is the least pre-fixed point of the rule-system functor

.. math::

F : \mathbf{Set}^{I^{\mathrm{op}}}_{K} \to \mathbf{Set}^{I^{\mathrm{op}}}_{K}

in the :math:K-enriched lattice of charts (Tarski-Knaster). The chart is the :math:K-presheaf :math:I^{\mathrm{op}} \to K assigning the aggregate inside weight to each item. The agenda is an operational realisation of the fixed-point computation; the strategy-independence theorem (Goodman 1999 §3) guarantees that the chart's final value is independent of the agenda discipline when the semiring is idempotent.

References

Shieber, Schabes & Pereira (1995) "Principles and Implementation of Deductive Parsing." Journal of Logic Programming 24(1-2):3-36. doi:10.1016/0743-1066(95)00035-I
Pereira & Warren (1983) "Parsing as Deduction." Proceedings of the 21st Annual Meeting of the ACL, pp. 137-144. doi:10.3115/981311.981338
Knuth (1977) "A Generalization of Dijkstra's Algorithm." Information Processing Letters 6(1):1-5. doi:10.1016/0020-0190(77)90002-3
Goodman (1999) "Semiring Parsing." Computational Linguistics 25(4):573-605. https://aclanthology.org/J99-4004/
Klein & Manning (2001) "Parsing and Hypergraphs." Proceedings of IWPT, pp. 123-134. doi:10.1007/1-4020-2295-6_18
McAllester (2002) "On the Complexity Analysis of Static Analyses." Journal of the ACM 49(4):512-537. doi:10.1145/581771.581774
Nederhof (2003) "Weighted Deductive Parsing and Knuth's Algorithm." Computational Linguistics 29(1):135-143. doi:10.1162/089120103321337467
Eisner, Goldlust & Smith (2005) "Compiling Comp Ling: Practical Weighted Dynamic Programming and the Dyna Language." Proceedings of HLT-EMNLP, pp. 281-290. https://aclanthology.org/H05-1036/
Eisner & Blatz (2007) "Program Transformations for Optimization of Parsing Algorithms and other Weighted Logic Programs." Proceedings of the 11th Conference on Formal Grammar.

Wildcard `dataclass` ¶

Wildcard(name: str)

Pattern-position wildcard.

A wildcard matches any value in the corresponding slot and binds it to name for use in the conclusion. Two wildcards with the same name in a single rule's premise list must bind to equal values (variable-sharing).

InferenceRule `dataclass` ¶

InferenceRule(name: str, premises: tuple[Pattern, ...], conclusion: Pattern, weight_fn: Callable[[Bindings, tuple, ChartSemiring], Any] | None = None, side_condition: Callable[[Bindings], bool] | None = None)

A weighted inference rule, that is, an arity-n hyperedge.

PARAMETER	DESCRIPTION
`name`	Rule identifier (used for diagnostics and provenance). TYPE: `str`
`premises`	Patterns the rule's antecedents must match. TYPE: `tuple of Pattern`
`conclusion`	Pattern of the item the rule produces. Wildcards must appear in the premises (so they are bound by the time the conclusion is constructed). TYPE: `Pattern`
`weight_fn`	Function `(bindings, premise_weights, semiring) -> Weight` producing the conclusion's weight from the matched premises. Defaults to the semiring product of premise weights (the standard semiring-parsing aggregation). TYPE: `Callable` DEFAULT: `None`
`side_condition`	Predicate `bindings -> bool`. The rule fires only when this returns `True`. Used for guards like adjacency `i < k < j` in CKY-style rules. TYPE: `Callable` DEFAULT: `None`

Chart ¶

Bases: ABC

A K-valued presheaf on the item algebra.

Categorically, a chart is the K-presheaf :math:C : I^{\mathrm{op}} \to K produced by the deduction system on an input. The chart is the least pre-fixed point of the rule-system functor; operationally, the agenda engine populates it bottom-up.

Concrete subclasses choose a storage strategy: dense tensor-indexed (for CKY-style spans), sparse hash-indexed (for Datalog atoms), or term-structural (for MLTT judgments).

lookup `abstractmethod` ¶

lookup(pattern: Pattern) -> Iterable[tuple[Item, Tensor]]

Enumerate (item, weight) pairs matching a pattern.

PARAMETER	DESCRIPTION
`pattern`	The pattern to match stored items against. TYPE: `Pattern`

RETURNS	DESCRIPTION
`Iterable of (Item, torch.Tensor)`	The matching items with their weights.

Source code in src/quivers/stochastic/agenda.py

@abstractmethod
def lookup(self, pattern: Pattern) -> Iterable[tuple[Item, torch.Tensor]]:
    """Enumerate (item, weight) pairs matching a pattern.

    Parameters
    ----------
    pattern : Pattern
        The pattern to match stored items against.

    Returns
    -------
    Iterable of (Item, torch.Tensor)
        The matching items with their weights.
    """
    ...

insert_or_aggregate `abstractmethod` ¶

insert_or_aggregate(item: Item, weight: Tensor, semiring: ChartSemiring) -> bool

Insert or aggregate an item's weight.

PARAMETER	DESCRIPTION
`item`	The item to store. TYPE: `Item`
`weight`	The weight to insert, or to aggregate with the stored weight under `semiring.plus`. TYPE: `Tensor`
`semiring`	The semiring whose `plus` aggregates weights. TYPE: `ChartSemiring`

RETURNS	DESCRIPTION
`bool`	`True` if the item's stored weight changed (so it should be re-enqueued for downstream firings); `False` if the weight was unchanged (the inference was redundant under the semiring's idempotent join).

Source code in src/quivers/stochastic/agenda.py

@abstractmethod
def insert_or_aggregate(
    self,
    item: Item,
    weight: torch.Tensor,
    semiring: ChartSemiring,
) -> bool:
    """Insert or aggregate an item's weight.

    Parameters
    ----------
    item : Item
        The item to store.
    weight : torch.Tensor
        The weight to insert, or to aggregate with the stored
        weight under ``semiring.plus``.
    semiring : ChartSemiring
        The semiring whose ``plus`` aggregates weights.

    Returns
    -------
    bool
        ``True`` if the item's stored weight changed (so it
        should be re-enqueued for downstream firings);
        ``False`` if the weight was unchanged (the inference was
        redundant under the semiring's idempotent join).
    """
    ...

get `abstractmethod` ¶

get(item: Item) -> Tensor | None

Return the chart's weight at an item, or None if absent.

PARAMETER	DESCRIPTION
`item`	The item to look up. TYPE: `Item`

RETURNS	DESCRIPTION
`Tensor or None`	The stored weight, or `None` if the item is absent.

Source code in src/quivers/stochastic/agenda.py

@abstractmethod
def get(self, item: Item) -> torch.Tensor | None:
    """Return the chart's weight at an item, or ``None`` if absent.

    Parameters
    ----------
    item : Item
        The item to look up.

    Returns
    -------
    torch.Tensor or None
        The stored weight, or ``None`` if the item is absent.
    """
    ...

items `abstractmethod` ¶

items() -> Iterable[tuple[Item, Tensor]]

Enumerate all (item, weight) pairs in the chart.

RETURNS	DESCRIPTION
`Iterable of (Item, torch.Tensor)`	Every stored item with its weight.

Source code in src/quivers/stochastic/agenda.py

@abstractmethod
def items(self) -> Iterable[tuple[Item, torch.Tensor]]:
    """Enumerate all (item, weight) pairs in the chart.

    Returns
    -------
    Iterable of (Item, torch.Tensor)
        Every stored item with its weight.
    """
    ...

HashChart ¶

HashChart(tolerance: float = 0.0)

Bases: Chart

Dictionary-backed chart for arbitrary item algebras.

Stores items as keys in a Python dict; supports linear-scan pattern matching. Suitable for Datalog atoms, MLTT judgments, and any deduction whose items don't have a dense integer encoding. Falls back to O(|chart| · |pattern|) match cost per lookup; faster specializations should override lookup with an indexed structure.

Weights are stored as torch.Tensor values; autograd flows through insert_or_aggregate's semiring.plus(torch.stack([…])) reduction, so the chart's final values carry gradients with respect to any requires_grad=True rule-weight parameters that fed into the agenda.

PARAMETER	DESCRIPTION
`tolerance`	The smallest change in an item's weight that counts as an update; `0.0` treats any change as an update. TYPE: `float` DEFAULT: `0.0`

Source code in src/quivers/stochastic/agenda.py

def __init__(self, tolerance: float = 0.0) -> None:
    self._store: dict[Item, torch.Tensor] = {}
    self._tolerance: float = float(tolerance)

lookup ¶

lookup(pattern: Pattern) -> Iterable[tuple[Item, Tensor]]

Scan the stored items for those matching a pattern.

PARAMETER	DESCRIPTION
`pattern`	The pattern to match stored items against. TYPE: `Pattern`

RETURNS	DESCRIPTION
`Iterable of (Item, torch.Tensor)`	The matching items with their weights.

Source code in src/quivers/stochastic/agenda.py

def lookup(self, pattern: Pattern) -> Iterable[tuple[Item, torch.Tensor]]:
    """Scan the stored items for those matching a pattern.

    Parameters
    ----------
    pattern : Pattern
        The pattern to match stored items against.

    Returns
    -------
    Iterable of (Item, torch.Tensor)
        The matching items with their weights.
    """
    for item, w in self._store.items():
        b = match(pattern, item)
        if b is not None:
            yield item, w

insert_or_aggregate ¶

insert_or_aggregate(item: Item, weight: Tensor, semiring: ChartSemiring) -> bool

Aggregate weight into the chart at item.

For non-idempotent semirings (LogProb, Counting, Inside) with cyclic rule graphs, every re-derivation of an item via a new path increases its weight via semiring.plus, even when the item itself is already in the chart. With an unconstrained cycle weight, this sequence is unbounded: either the cycle is contractive (cycle log-weight :math:< 0), in which case the chart's weight converges to a finite Kleene-star limit; or the cycle is non-contractive (:math:\ge 0), in which case the chart total is :math:+ \infty and the model is mathematically ill-posed.

The chart makes this distinction observable by terminating the agenda when the per-item update falls below the tolerance. The default tolerance 0.0 treats any change as an update; positive tolerances expose convergent cyclic fixed points while still routing divergent systems through the agenda's max_iterations safety net.

PARAMETER	DESCRIPTION
`item`	The item to store. TYPE: `Item`
`weight`	The weight to insert or aggregate. TYPE: `Tensor`
`semiring`	The semiring whose `plus` aggregates weights. TYPE: `ChartSemiring`

RETURNS	DESCRIPTION
`bool`	`True` if the stored weight changed by more than the tolerance (or the item is new).

Source code in src/quivers/stochastic/agenda.py

def insert_or_aggregate(
    self,
    item: Item,
    weight: torch.Tensor,
    semiring: ChartSemiring,
) -> bool:
    """Aggregate ``weight`` into the chart at ``item``.

    For non-idempotent semirings (LogProb, Counting, Inside)
    with cyclic rule graphs, every re-derivation of an item via
    a new path increases its weight via `semiring.plus`,
    even when the item itself is already in the chart. With an
    unconstrained cycle weight, this sequence is unbounded:
    either the cycle is contractive (cycle log-weight :math:`<
    0`), in which case the chart's weight converges to a
    finite Kleene-star limit; or the cycle is non-contractive
    (:math:`\\ge 0`), in which case the chart total is :math:`+
    \\infty` and the model is mathematically ill-posed.

    The chart makes this distinction observable by terminating
    the agenda when the per-item update falls below the
    tolerance. The default tolerance ``0.0`` treats any change
    as an update; positive tolerances expose convergent cyclic
    fixed points while still routing divergent systems through
    the agenda's ``max_iterations`` safety net.

    Parameters
    ----------
    item : Item
        The item to store.
    weight : torch.Tensor
        The weight to insert or aggregate.
    semiring : ChartSemiring
        The semiring whose ``plus`` aggregates weights.

    Returns
    -------
    bool
        ``True`` if the stored weight changed by more than the
        tolerance (or the item is new).
    """
    if item not in self._store:
        self._store[item] = weight
        return True
    existing = self._store[item]
    stacked = torch.stack([existing, weight])
    merged = semiring.plus(stacked, dim=0)
    if self._tolerance > 0.0:
        delta = (merged.detach() - existing.detach()).abs().max()
        changed = bool(float(delta) > self._tolerance)
    else:
        changed = not torch.equal(merged, existing)
    self._store[item] = merged
    return changed

get ¶

get(item: Item) -> Tensor | None

Return the stored weight at an item.

PARAMETER	DESCRIPTION
`item`	The item to look up. TYPE: `Item`

RETURNS	DESCRIPTION
`Tensor or None`	The stored weight, or `None` if the item is absent.

Source code in src/quivers/stochastic/agenda.py

def get(self, item: Item) -> torch.Tensor | None:
    """Return the stored weight at an item.

    Parameters
    ----------
    item : Item
        The item to look up.

    Returns
    -------
    torch.Tensor or None
        The stored weight, or ``None`` if the item is absent.
    """
    return self._store.get(item)

items ¶

items() -> Iterable[tuple[Item, Tensor]]

Enumerate all stored (item, weight) pairs.

RETURNS	DESCRIPTION
`Iterable of (Item, torch.Tensor)`	Every stored item with its weight.

Source code in src/quivers/stochastic/agenda.py

def items(self) -> Iterable[tuple[Item, torch.Tensor]]:
    """Enumerate all stored (item, weight) pairs.

    Returns
    -------
    Iterable of (Item, torch.Tensor)
        Every stored item with its weight.
    """
    return self._store.items()

ChartView ¶

ChartView(result: 'AgendaResult')

A first-class, differentiable view onto a chart.

Wraps a Chart produced by an agenda run and exposes the user-facing presheaf-evaluation operations:

weight: query the aggregated weight at a single ground item; returns a differentiable torch.Tensor.
enumerate: enumerate items matching a pattern with their weights.
derivations: extract the derivation forest at an item (under the derivation semiring; for the basic Boolean / LOG_PROB / Viterbi semirings, returns the flat list of matched derivations as a placeholder).
goal_weight: return the weight at the goal items identified at run time.

Categorically, the chart is the K-presheaf :math:I^{\mathrm{op}} \to K produced by the deduction system; ChartView's methods are presheaf evaluations. Gradients flow through these operations because the underlying tensors carry requires_grad from the rule weights.

PARAMETER	DESCRIPTION
`result`	The agenda run to view. TYPE: `AgendaResult`

Source code in src/quivers/stochastic/agenda.py

def __init__(self, result: "AgendaResult") -> None:
    self._result = result

chart `property` ¶

chart: Chart

The underlying K-presheaf.

attached_loss `property` ¶

attached_loss: Tensor | None

The sum of rule-attached and chart-attached loss values fired during this deduction's run, or None if no losses were declared at those sites.

semiring `property` ¶

semiring: ChartSemiring

The semiring the chart was computed over.

goal_items `property` ¶

goal_items: list[tuple[Item, Tensor]]

List of (item, weight) pairs matching the goal predicate.

weight ¶

weight(item: Item) -> Tensor

Return the aggregated weight at a concrete item.

PARAMETER	DESCRIPTION
`item`	A ground item. TYPE: `Item`

RETURNS	DESCRIPTION
`Tensor`	The item's differentiable weight.

RAISES	DESCRIPTION
`KeyError`	If the item was never derived.

Source code in src/quivers/stochastic/agenda.py

def weight(self, item: Item) -> torch.Tensor:
    """Return the aggregated weight at a concrete ``item``.

    Parameters
    ----------
    item : Item
        A ground item.

    Returns
    -------
    torch.Tensor
        The item's differentiable weight.

    Raises
    ------
    KeyError
        If the item was never derived.
    """
    w = self._result.chart.get(item)
    if w is None:
        raise KeyError(f"item {item!r} not in chart")
    return w

try_weight ¶

try_weight(item: Item, default: Tensor | None = None) -> Tensor

Return the weight at item, or a fallback if it is absent.

PARAMETER	DESCRIPTION
`item`	A ground item. TYPE: `Item`
`default`	The value to return for an absent item; `None` means the semiring's zero. TYPE: `Tensor or None` DEFAULT: `None`

RETURNS	DESCRIPTION
`Tensor`	The item's weight, `default`, or the semiring's zero.

Source code in src/quivers/stochastic/agenda.py

def try_weight(
    self,
    item: Item,
    default: torch.Tensor | None = None,
) -> torch.Tensor:
    """Return the weight at ``item``, or a fallback if it is absent.

    Parameters
    ----------
    item : Item
        A ground item.
    default : torch.Tensor or None
        The value to return for an absent item; ``None`` means
        the semiring's zero.

    Returns
    -------
    torch.Tensor
        The item's weight, ``default``, or the semiring's zero.
    """
    w = self._result.chart.get(item)
    if w is not None:
        return w
    if default is not None:
        return default
    return torch.tensor(
        float(self.semiring.zero)
        if hasattr(self.semiring.zero, "__float__")
        else 0.0,
        dtype=torch.get_default_dtype(),
    )

enumerate ¶

enumerate(pattern: Pattern) -> list[tuple[Item, Tensor]]

Enumerate (item, weight) pairs matching pattern.

Wildcards in pattern (instances of Wildcard) match any slot value.

PARAMETER	DESCRIPTION
`pattern`	The pattern to match. TYPE: `Pattern`

RETURNS	DESCRIPTION
`list of (Item, torch.Tensor)`	The matching items with their differentiable weights.

Source code in src/quivers/stochastic/agenda.py

def enumerate(self, pattern: Pattern) -> list[tuple[Item, torch.Tensor]]:
    """Enumerate (item, weight) pairs matching ``pattern``.

    Wildcards in ``pattern`` (instances of `Wildcard`)
    match any slot value.

    Parameters
    ----------
    pattern : Pattern
        The pattern to match.

    Returns
    -------
    list of (Item, torch.Tensor)
        The matching items with their differentiable weights.
    """
    return list(self._result.chart.lookup(pattern))

embedding ¶

embedding(item: Item) -> Tensor

Return the vector embedding of item under the deduction's attached encoder.

Requires the originating DeductionSystem to carry an _item_encoder attribute (set by the DSL compiler when the deduction's body declares encoder C). Items are converted to quivers.structural.Term form on the fly.

PARAMETER	DESCRIPTION
`item`	The item to embed. TYPE: `Item`

RETURNS	DESCRIPTION
`Tensor`	The encoder's embedding of the item.

RAISES	DESCRIPTION
`RuntimeError`	If the run carries no encoder.

Source code in src/quivers/stochastic/agenda.py

def embedding(self, item: Item) -> torch.Tensor:
    """Return the vector embedding of ``item`` under the deduction's
    attached encoder.

    Requires the originating `DeductionSystem` to carry an
    ``_item_encoder`` attribute (set by the DSL compiler when
    the deduction's body declares ``encoder C``). Items are
    converted to [`quivers.structural.Term`][quivers.structural.Term] form on the fly.

    Parameters
    ----------
    item : Item
        The item to embed.

    Returns
    -------
    torch.Tensor
        The encoder's embedding of the item.

    Raises
    ------
    RuntimeError
        If the run carries no encoder.
    """
    encoder = getattr(self._result, "encoder", None)
    if encoder is None:
        raise RuntimeError(
            "chart has no attached encoder; declare "
            "`signature ... encoder ...` in the deduction block"
        )
    return encoder(item)

derivations ¶

derivations(item: Item) -> list[Item]

Return the items of the chart in which item was derived.

The chart records only the aggregate weight at each item, so this returns the chart's item set as a flat enumeration when item is in the chart. The full derivation forest (a tree-structured object whose leaves are axioms and whose internal nodes are rule firings) is recoverable by running the agenda with a derivation semiring.

PARAMETER	DESCRIPTION
`item`	The item whose derivations to return. TYPE: `Item`

RETURNS	DESCRIPTION
`list of Item`	Every item in the chart, or an empty list when `item` was never derived.

Source code in src/quivers/stochastic/agenda.py

def derivations(self, item: Item) -> list[Item]:
    """Return the items of the chart in which ``item`` was derived.

    The chart records only the aggregate weight at each item,
    so this returns the chart's item set as a flat enumeration
    when ``item`` is in the chart. The full derivation forest
    (a tree-structured object whose leaves are axioms and whose
    internal nodes are rule firings) is recoverable by running
    the agenda with a derivation semiring.

    Parameters
    ----------
    item : Item
        The item whose derivations to return.

    Returns
    -------
    list of Item
        Every item in the chart, or an empty list when ``item``
        was never derived.
    """
    # In the current implementation we expose the set of
    # items that contributed to the item's weight; a
    # derivation-semiring run is required for the full tree.
    # For the common case where the user wants "every item
    # in the chart," returning the item list is the closest
    # correct answer.
    if item not in (it for it, _ in self._result.chart.items()):
        return []
    return [it for it, _ in self._result.chart.items()]

goal_weight ¶

goal_weight() -> Tensor

Aggregate weight over all goal items.

If a single goal item was identified, returns its weight directly; otherwise aggregates via the semiring's plus reduction (the standard parse-as-marginal computation).

RETURNS	DESCRIPTION
`Tensor`	The aggregated goal weight, or the semiring's zero when no goal item was derived.

Source code in src/quivers/stochastic/agenda.py

def goal_weight(self) -> torch.Tensor:
    """Aggregate weight over all goal items.

    If a single goal item was identified, returns its weight
    directly; otherwise aggregates via the semiring's
    ``plus`` reduction (the standard parse-as-marginal
    computation).

    Returns
    -------
    torch.Tensor
        The aggregated goal weight, or the semiring's zero when
        no goal item was derived.
    """
    if not self._result.goal_items:
        return torch.tensor(
            float(self.semiring.zero)
            if hasattr(self.semiring.zero, "__float__")
            else 0.0,
            dtype=torch.get_default_dtype(),
        )
    if len(self._result.goal_items) == 1:
        return self._result.goal_items[0][1]
    weights = torch.stack([w for _, w in self._result.goal_items])
    return self.semiring.plus(weights, dim=0)

Agenda ¶

Bases: ABC

A queue of items pending further inference.

The agenda discipline (FIFO / LIFO / priority) determines the evaluation order; correctness is independent of discipline for idempotent semirings (Goodman 1999 §3) but efficiency depends on it (McAllester 2002).

push `abstractmethod` ¶

push(item: Item, weight: Tensor) -> None

Add an item and its weight to the agenda.

PARAMETER	DESCRIPTION
`item`	The derived item. TYPE: `Item`
`weight`	The weight contributed by this derivation. TYPE: `Tensor`

Source code in src/quivers/stochastic/agenda.py

@abstractmethod
def push(self, item: Item, weight: torch.Tensor) -> None:
    """Add an item and its weight to the agenda.

    Parameters
    ----------
    item : Item
        The derived item.
    weight : torch.Tensor
        The weight contributed by this derivation.
    """

pop `abstractmethod` ¶

pop() -> tuple[Item, Tensor]

Remove and return the next item under this discipline.

RETURNS	DESCRIPTION
`tuple of (Item, torch.Tensor)`	The next item and its pending weight.

Source code in src/quivers/stochastic/agenda.py

@abstractmethod
def pop(self) -> tuple[Item, torch.Tensor]:
    """Remove and return the next item under this discipline.

    Returns
    -------
    tuple of (Item, torch.Tensor)
        The next item and its pending weight.
    """

empty `abstractmethod` ¶

empty() -> bool

Whether no items are pending.

RETURNS	DESCRIPTION
`bool`	`True` when the agenda holds no items.

Source code in src/quivers/stochastic/agenda.py

@abstractmethod
def empty(self) -> bool:
    """Whether no items are pending.

    Returns
    -------
    bool
        ``True`` when the agenda holds no items.
    """

bind_semiring ¶

bind_semiring(semiring: ChartSemiring) -> None

Give the agenda access to the engine's semiring.

run_agenda calls this once, before pushing the axioms. Disciplines that can exploit the binding override it; for instance, FIFOAgenda merges pending contributions to the same item via semiring.plus. The default ignores the binding.

PARAMETER	DESCRIPTION
`semiring`	The engine's semiring. TYPE: `ChartSemiring`

Source code in src/quivers/stochastic/agenda.py

def bind_semiring(self, semiring: ChartSemiring) -> None:
    """Give the agenda access to the engine's semiring.

    `run_agenda` calls this once, before pushing the axioms.
    Disciplines that can exploit the binding override it; for
    instance, `FIFOAgenda` merges pending contributions
    to the same item via ``semiring.plus``. The default ignores
    the binding.

    Parameters
    ----------
    semiring : ChartSemiring
        The engine's semiring.
    """

FIFOAgenda ¶

FIFOAgenda()

Bases: Agenda

First-in-first-out agenda (semi-naïve Datalog discipline).

The agenda processes items in the order they were derived. Correct for any monotone semiring; the canonical choice for Datalog and Earley parsing.

Once a semiring is bound (bind_semiring, which the engine does on entry), a contribution pushed for an item that is already pending merges into that item's single queue entry via semiring.plus. Semiring distributivity makes the merge exact: firing a rule once on the merged contribution pushes the same total mass downstream as firing it once per contribution. Without merging, a cyclic rule graph re-enqueues every contribution separately, and the number of pending entries grows geometrically with derivation depth even when the weighted fixed point converges.

Source code in src/quivers/stochastic/agenda.py

def __init__(self) -> None:
    self._queue: deque[tuple[Item, torch.Tensor]] = deque()
    self._order: deque[Item] = deque()
    self._pending: dict[Item, torch.Tensor] = {}
    self._semiring: ChartSemiring | None = None

bind_semiring ¶

bind_semiring(semiring: ChartSemiring) -> None

Bind the semiring that merges pending contributions.

PARAMETER	DESCRIPTION
`semiring`	The engine's semiring. TYPE: `ChartSemiring`

Source code in src/quivers/stochastic/agenda.py

def bind_semiring(self, semiring: ChartSemiring) -> None:
    """Bind the semiring that merges pending contributions.

    Parameters
    ----------
    semiring : ChartSemiring
        The engine's semiring.
    """
    self._semiring = semiring

push ¶

push(item: Item, weight: Tensor) -> None

Add an item and its weight to the agenda.

PARAMETER	DESCRIPTION
`item`	The derived item. TYPE: `Item`
`weight`	The weight contributed by this derivation. TYPE: `Tensor`

Source code in src/quivers/stochastic/agenda.py

def push(self, item: Item, weight: torch.Tensor) -> None:
    """Add an item and its weight to the agenda.

    Parameters
    ----------
    item : Item
        The derived item.
    weight : torch.Tensor
        The weight contributed by this derivation.
    """
    if self._semiring is None:
        self._queue.append((item, weight))
        return
    existing = self._pending.get(item)
    if existing is None:
        self._pending[item] = weight
        self._order.append(item)
        return
    stacked = torch.stack([existing, weight])
    self._pending[item] = self._semiring.plus(stacked, dim=0)

pop ¶

pop() -> tuple[Item, Tensor]

Remove and return the next item under this discipline.

RETURNS	DESCRIPTION
`tuple of (Item, torch.Tensor)`	The next item and its pending weight.

Source code in src/quivers/stochastic/agenda.py

def pop(self) -> tuple[Item, torch.Tensor]:
    """Remove and return the next item under this discipline.

    Returns
    -------
    tuple of (Item, torch.Tensor)
        The next item and its pending weight.
    """
    # Entries pushed before a semiring was bound drain first;
    # they were pushed earliest, so this preserves FIFO order.
    if self._queue:
        return self._queue.popleft()
    item = self._order.popleft()
    return item, self._pending.pop(item)

empty ¶

empty() -> bool

Whether no items are pending.

RETURNS	DESCRIPTION
`bool`	`True` when the agenda holds no items.

Source code in src/quivers/stochastic/agenda.py

def empty(self) -> bool:
    """Whether no items are pending.

    Returns
    -------
    bool
        ``True`` when the agenda holds no items.
    """
    return not self._queue and not self._order

LIFOAgenda ¶

LIFOAgenda()

Bases: Agenda

Last-in-first-out agenda (depth-first proof-search discipline).

The agenda processes items in reverse-derivation order. Suitable for goal-directed search like Agda elaboration and Twelf-style MLTT type-checking, where depth-first proof construction is the natural strategy.

Source code in src/quivers/stochastic/agenda.py

def __init__(self) -> None:
    self._stack: list[tuple[Item, torch.Tensor]] = []

push ¶

push(item: Item, weight: Tensor) -> None

Add an item and its weight to the agenda.

PARAMETER	DESCRIPTION
`item`	The derived item. TYPE: `Item`
`weight`	The weight contributed by this derivation. TYPE: `Tensor`

Source code in src/quivers/stochastic/agenda.py

def push(self, item: Item, weight: torch.Tensor) -> None:
    """Add an item and its weight to the agenda.

    Parameters
    ----------
    item : Item
        The derived item.
    weight : torch.Tensor
        The weight contributed by this derivation.
    """
    self._stack.append((item, weight))

pop ¶

pop() -> tuple[Item, Tensor]

Remove and return the next item under this discipline.

RETURNS	DESCRIPTION
`tuple of (Item, torch.Tensor)`	The next item and its pending weight.

Source code in src/quivers/stochastic/agenda.py

def pop(self) -> tuple[Item, torch.Tensor]:
    """Remove and return the next item under this discipline.

    Returns
    -------
    tuple of (Item, torch.Tensor)
        The next item and its pending weight.
    """
    return self._stack.pop()

empty ¶

empty() -> bool

Whether no items are pending.

RETURNS	DESCRIPTION
`bool`	`True` when the agenda holds no items.

Source code in src/quivers/stochastic/agenda.py

def empty(self) -> bool:
    """Whether no items are pending.

    Returns
    -------
    bool
        ``True`` when the agenda holds no items.
    """
    return not self._stack

PriorityQueueAgenda ¶

PriorityQueueAgenda(priority_fn: Callable[[Item, Tensor], float])

Bases: Agenda

Priority-queue agenda parameterized by a priority function.

Items are processed in decreasing priority order. Used by Knuth's algorithm (priority = current best score), A* parsing (priority = g + h with admissible h), and any best-first chart algorithm.

PARAMETER	DESCRIPTION
`priority_fn`	`(item, weight) -> float`. Higher priorities are processed first. The chart's monotone-priority property (Nederhof 2003) ensures correctness when the semiring is superior. TYPE: `Callable`

Source code in src/quivers/stochastic/agenda.py

def __init__(self, priority_fn: Callable[[Item, torch.Tensor], float]) -> None:
    self._priority_fn = priority_fn
    self._heap: list[tuple[float, int, Item, torch.Tensor]] = []
    self._counter = 0  # tie-breaker for deterministic ordering

push ¶

push(item: Item, weight: Tensor) -> None

Add an item and its weight to the agenda.

PARAMETER	DESCRIPTION
`item`	The derived item. TYPE: `Item`
`weight`	The weight contributed by this derivation. TYPE: `Tensor`

Source code in src/quivers/stochastic/agenda.py

def push(self, item: Item, weight: torch.Tensor) -> None:
    """Add an item and its weight to the agenda.

    Parameters
    ----------
    item : Item
        The derived item.
    weight : torch.Tensor
        The weight contributed by this derivation.
    """
    # heapq is a min-heap; negate priority for max-heap behavior.
    priority = -float(self._priority_fn(item, weight))
    self._counter += 1
    heapq.heappush(self._heap, (priority, self._counter, item, weight))

pop ¶

pop() -> tuple[Item, Tensor]

Remove and return the next item under this discipline.

RETURNS	DESCRIPTION
`tuple of (Item, torch.Tensor)`	The next item and its pending weight.

Source code in src/quivers/stochastic/agenda.py

def pop(self) -> tuple[Item, torch.Tensor]:
    """Remove and return the next item under this discipline.

    Returns
    -------
    tuple of (Item, torch.Tensor)
        The next item and its pending weight.
    """
    _, _, item, weight = heapq.heappop(self._heap)
    return item, weight

empty ¶

empty() -> bool

Whether no items are pending.

RETURNS	DESCRIPTION
`bool`	`True` when the agenda holds no items.

Source code in src/quivers/stochastic/agenda.py

def empty(self) -> bool:
    """Whether no items are pending.

    Returns
    -------
    bool
        ``True`` when the agenda holds no items.
    """
    return not self._heap

AgendaResult `dataclass` ¶

AgendaResult(chart: Chart, semiring: ChartSemiring, goal_items: list[tuple[Item, Tensor]] = list(), iterations: int = 0, encoder: Encoder | None = None, attached_loss: Tensor | None = None)

The chart produced by an agenda-driven deduction.

ATTRIBUTE	DESCRIPTION
`chart`	The final K-presheaf on the item algebra. TYPE: `Chart`
`semiring`	The semiring used for weight aggregation. TYPE: `ChartSemiring`
`goal_items`	Items in the chart matching the goal predicate, with their final aggregated weights. TYPE: `list of (Item, torch.Tensor)`
`iterations`	Number of agenda steps consumed (diagnostic). TYPE: `int`

DeductionSystem `dataclass` ¶

DeductionSystem(rules: tuple[InferenceRule, ...], semiring: ChartSemiring, axiom_injector: Callable[[Any], list[tuple[Item, Tensor]]], goal: Callable[[Item], bool], agenda_factory: Callable[[], Agenda] = FIFOAgenda, chart_factory: Callable[[], Chart] = HashChart, max_iterations: int = 100000, tolerance: float = 0.0)

A weighted deductive system parameterized over its components.

The system is parameterized by:

An item algebra (implicit in the patterns the rules use).
A list of arity-n InferenceRule hyperedges.
A ChartSemiring for weight aggregation.
An axiom injector In -> [(Item, Weight)] producing the input's lexical / boundary items.
A goal predicate Item -> bool selecting the result items.
(Optional) a chart constructor and an agenda strategy.

The same data structure subsumes CKY (FIFO agenda, span items, Boolean / inside semiring), Viterbi (priority agenda with the current weight as priority, max-times semiring), A* parsing (priority agenda with an admissible heuristic, tropical semiring), MLTT type-checking (LIFO agenda, judgment items, Boolean semiring), and weighted Datalog (FIFO, atoms, any naturally-ordered semiring).

run ¶

run(input_value: Any) -> AgendaResult

Run the deduction system on an input value.

Injects the input's axioms, runs the agenda to fixed point, attaches the item encoder when one is set, and sums any rule-attached and chart-attached losses.

PARAMETER	DESCRIPTION
`input_value`	The input the axiom injector reads. TYPE: `Any`

RETURNS	DESCRIPTION
`AgendaResult`	The completed chart, its goal items, and any attached loss.

Source code in src/quivers/stochastic/agenda.py

def run(self, input_value: Any) -> AgendaResult:
    """Run the deduction system on an input value.

    Injects the input's axioms, runs the agenda to fixed point,
    attaches the item encoder when one is set, and sums any
    rule-attached and chart-attached losses.

    Parameters
    ----------
    input_value : Any
        The input the axiom injector reads.

    Returns
    -------
    AgendaResult
        The completed chart, its goal items, and any attached
        loss.
    """
    axioms = self.axiom_injector(input_value)
    registry = getattr(self, "_loss_registry", None)
    deduction_name = getattr(self, "_deduction_name", None)
    rule_loss_acc: list[torch.Tensor] = []

    def _rule_callback(
        rule_name: str,
        antecedents: list[tuple[Item, torch.Tensor]],
        conclusion: Item,
        conclusion_w: torch.Tensor,
    ) -> None:
        if registry is None or deduction_name is None:
            return
        env = {
            "rule": rule_name,
            "deduction": deduction_name,
            "antecedents": list(antecedents),
            "conclusion": conclusion,
            "weight": conclusion_w,
        }
        val = registry.evaluate_on(
            "rule",
            target=rule_name,
            env=env,
            rule_deduction=deduction_name,
        )
        rule_loss_acc.append(val)

    # If the user supplied a positive ``tolerance``, propagate
    # it to the chart so its aggregation step terminates on
    # convergence. The default chart_factory is ``HashChart``,
    # whose constructor accepts the tolerance; user-supplied
    # alternative chart factories can ignore the argument.
    try:
        chart_inst = self.chart_factory(tolerance=self.tolerance)
    except TypeError:
        chart_inst = self.chart_factory()
    result = run_agenda(
        axioms=axioms,
        rules=self.rules,
        semiring=self.semiring,
        agenda=self.agenda_factory(),
        goal=_full_extent_goal(self.goal, input_value),
        max_iterations=self.max_iterations,
        chart=chart_inst,
        rule_callback=(_rule_callback if registry is not None else None),
    )
    # Propagate any attached item-encoder to the result.
    comp = getattr(self, "_item_encoder", None)
    if comp is not None:
        result.encoder = comp
    # Evaluate chart-attached losses on the completed chart.
    if registry is not None and deduction_name is not None:
        chart_env = {
            "deduction": deduction_name,
            "chart": result.chart,
            "goal_items": result.goal_items,
        }
        chart_loss = registry.evaluate_on(
            "chart",
            target=deduction_name,
            env=chart_env,
        )
        losses = rule_loss_acc + [chart_loss]
    else:
        losses = rule_loss_acc
    if losses:
        total = losses[0]
        for v in losses[1:]:
            total = total + v
        result.attached_loss = total
    return result

parameters ¶

parameters(recurse: bool = True) -> Iterable[Parameter]

Yield every learnable parameter owned by this system.

Walks the optional _axiom_module (lexicon log-weights) and _rule_module (per-rule, per-binding log-weights) submodules attached by the compiler. The recurse flag is the standard torch.nn.Module.parameters signature so user code can pass a DeductionSystem anywhere a nn.Module parameter iterator is expected.

PARAMETER	DESCRIPTION
`recurse`	Whether to include parameters of nested submodules. TYPE: `bool` DEFAULT: `True`

RETURNS	DESCRIPTION
`Iterable of torch.nn.Parameter`	The learnable parameters.

Source code in src/quivers/stochastic/agenda.py

def parameters(self, recurse: bool = True) -> Iterable[torch.nn.Parameter]:
    """Yield every learnable parameter owned by this system.

    Walks the optional ``_axiom_module`` (lexicon log-weights)
    and ``_rule_module`` (per-rule, per-binding log-weights)
    submodules attached by the compiler. The ``recurse`` flag
    is the standard `torch.nn.Module.parameters` signature
    so user code can pass a ``DeductionSystem`` anywhere a
    ``nn.Module`` parameter iterator is expected.

    Parameters
    ----------
    recurse : bool
        Whether to include parameters of nested submodules.

    Returns
    -------
    Iterable of torch.nn.Parameter
        The learnable parameters.
    """
    for attr in ("_axiom_module", "_rule_module"):
        mod = getattr(self, attr, None)
        if mod is not None and hasattr(mod, "parameters"):
            yield from mod.parameters(recurse=recurse)

named_parameters ¶

named_parameters(prefix: str = '', recurse: bool = True) -> Iterable[tuple[str, Parameter]]

Yield (name, parameter) pairs over all learnable parameters.

PARAMETER	DESCRIPTION
`prefix`	A prefix prepended to every parameter name. TYPE: `str` DEFAULT: `''`
`recurse`	Whether to include parameters of nested submodules. TYPE: `bool` DEFAULT: `True`

RETURNS	DESCRIPTION
`Iterable of (str, torch.nn.Parameter)`	The named learnable parameters.

Source code in src/quivers/stochastic/agenda.py

def named_parameters(
    self,
    prefix: str = "",
    recurse: bool = True,
) -> Iterable[tuple[str, torch.nn.Parameter]]:
    """Yield ``(name, parameter)`` pairs over all learnable parameters.

    Parameters
    ----------
    prefix : str
        A prefix prepended to every parameter name.
    recurse : bool
        Whether to include parameters of nested submodules.

    Returns
    -------
    Iterable of (str, torch.nn.Parameter)
        The named learnable parameters.
    """
    for attr in ("_axiom_module", "_rule_module"):
        mod = getattr(self, attr, None)
        if mod is not None and hasattr(mod, "named_parameters"):
            sub_prefix = f"{prefix}.{attr}" if prefix else attr
            for n, p in mod.named_parameters(
                prefix=sub_prefix,
                recurse=recurse,
            ):
                yield n, p

make_wildcard ¶

make_wildcard(name: str) -> Wildcard

Build a fresh wildcard with the given variable name.

PARAMETER	DESCRIPTION
`name`	The pattern variable the wildcard binds. TYPE: `str`

RETURNS	DESCRIPTION
`Wildcard`	The wildcard.

Source code in src/quivers/stochastic/agenda.py

def make_wildcard(name: str) -> Wildcard:
    """Build a fresh wildcard with the given variable name.

    Parameters
    ----------
    name : str
        The pattern variable the wildcard binds.

    Returns
    -------
    Wildcard
        The wildcard.
    """
    return Wildcard(name)

instantiate ¶

instantiate(pattern: Pattern, bindings: Bindings) -> Item

Substitute wildcards in a pattern with their bound values.

The pattern may be a bare Wildcard (treated as "the entire item is the wildcard"), a structural tuple, or a leaf value (returned unchanged). Recursion runs over tuple children.

PARAMETER	DESCRIPTION
`pattern`	The pattern to instantiate. TYPE: `Pattern`
`bindings`	Values for the pattern's wildcards. TYPE: `Bindings`

RETURNS	DESCRIPTION
`Item`	A concrete item with no wildcards.

RAISES	DESCRIPTION
`KeyError`	If a wildcard in the pattern has no binding.

Source code in src/quivers/stochastic/agenda.py

def instantiate(pattern: Pattern, bindings: Bindings) -> Item:
    """Substitute wildcards in a pattern with their bound values.

    The pattern may be a bare `Wildcard` (treated as "the
    entire item is the wildcard"), a structural tuple, or a leaf
    value (returned unchanged). Recursion runs over tuple
    children.

    Parameters
    ----------
    pattern : Pattern
        The pattern to instantiate.
    bindings : Bindings
        Values for the pattern's wildcards.

    Returns
    -------
    Item
        A concrete item with no wildcards.

    Raises
    ------
    KeyError
        If a wildcard in the pattern has no binding.
    """
    if isinstance(pattern, Wildcard):
        return bindings[pattern.name]
    if not isinstance(pattern, tuple):
        return pattern
    out: list[Any] = []
    for p in pattern:
        if isinstance(p, Wildcard):
            out.append(bindings[p.name])
        elif isinstance(p, tuple):
            out.append(instantiate(p, bindings))
        else:
            out.append(p)
    return tuple(out)

match ¶

match(pattern: Pattern, item: Item, bindings: Bindings | None = None) -> Bindings | None

Match an item against a pattern.

Wildcards bind the values at their positions; a wildcard already bound in bindings (or earlier in the pattern) must see an equal value. Tuples match slot by slot when their lengths agree, and other values match by equality.

PARAMETER	DESCRIPTION
`pattern`	The pattern to match. TYPE: `Pattern`
`item`	The item to match against. TYPE: `Item`
`bindings`	Bindings to extend; `None` starts from no bindings. TYPE: `Bindings or None` DEFAULT: `None`

RETURNS	DESCRIPTION
`Bindings or None`	The extended bindings, or `None` when the item does not match.

Source code in src/quivers/stochastic/agenda.py

def match(
    pattern: Pattern, item: Item, bindings: Bindings | None = None
) -> Bindings | None:
    """Match an item against a pattern.

    Wildcards bind the values at their positions; a wildcard
    already bound in ``bindings`` (or earlier in the pattern) must
    see an equal value. Tuples match slot by slot when their
    lengths agree, and other values match by equality.

    Parameters
    ----------
    pattern : Pattern
        The pattern to match.
    item : Item
        The item to match against.
    bindings : Bindings or None
        Bindings to extend; ``None`` starts from no bindings.

    Returns
    -------
    Bindings or None
        The extended bindings, or ``None`` when the item does not
        match.
    """
    if bindings is None:
        bindings = {}
    if isinstance(pattern, Wildcard):
        existing = bindings.get(pattern.name)
        if existing is None:
            return {**bindings, pattern.name: item}
        if existing == item:
            return bindings
        return None
    if not isinstance(pattern, tuple) or not isinstance(item, tuple):
        if pattern == item:
            return bindings
        return None
    if len(pattern) != len(item):
        return None
    out = dict(bindings)
    for p, v in zip(pattern, item):
        if isinstance(p, Wildcard):
            existing = out.get(p.name)
            if existing is None:
                out[p.name] = v
            elif existing != v:
                return None
        elif isinstance(p, tuple) and isinstance(v, tuple):
            sub = match(p, v, out)
            if sub is None:
                return None
            out = sub
        elif p != v:
            return None
    return out

run_agenda ¶

run_agenda(axioms: Iterable[tuple[Item, Tensor]], rules: Iterable[InferenceRule], semiring: ChartSemiring | None = None, agenda: Agenda | None = None, goal: Callable[[Item], bool] | None = None, max_iterations: int = 100000, chart: Chart | None = None, rule_callback: Callable[[str, list[tuple[Item, Tensor]], Item, Tensor], None] | None = None) -> AgendaResult

Run the agenda-driven deduction engine to fixed point.

Categorical denotation: returns the least pre-fixed point of the rule-system functor on the input axioms. The strategy-independence theorem (Goodman 1999) guarantees that the chart's final value is independent of the agenda discipline when semiring is idempotent.

Algorithm (Shieber-Schabes-Pereira 1995, Fig. 2 with semiring-weighted aggregation per Goodman 1999):

Push every axiom onto the agenda.
While the agenda is non-empty: a. Pop an item. b. Insert-or-aggregate into the chart. c. If the chart's weight changed, fire every rule for which the popped item is a premise: scan the chart for matching siblings, compute the conclusion's weight via the rule's weight_fn, and push the conclusion onto the agenda.
Return the chart with all items that match goal.

PARAMETER	DESCRIPTION
`axioms`	Initial items with their input-derived weights. TYPE: `iterable of (Item, weight)`
`rules`	The deduction system's hyperedges. TYPE: `iterable of InferenceRule`
`semiring`	Weight aggregation. Defaults to log-prob. TYPE: `ChartSemiring` DEFAULT: `None`
`agenda`	Evaluation strategy. Defaults to FIFO (semi-naïve). TYPE: `Agenda` DEFAULT: `None`
`goal`	Predicate selecting result items. Defaults to "every item". TYPE: `callable` DEFAULT: `None`
`max_iterations`	Safety bound on agenda steps; raises if exceeded. TYPE: `int` DEFAULT: `100000`
`chart`	Initial chart (defaults to empty `HashChart`). TYPE: `Chart` DEFAULT: `None`
`rule_callback`	Called as `(rule_name, antecedents, conclusion, weight)` after each rule firing. TYPE: `callable` DEFAULT: `None`

RETURNS	DESCRIPTION
`AgendaResult`	The final chart, the goal items, and the step count.

RAISES	DESCRIPTION
`RuntimeError`	If the agenda runs for more than `max_iterations` steps.

Source code in src/quivers/stochastic/agenda.py

def run_agenda(
    axioms: Iterable[tuple[Item, torch.Tensor]],
    rules: Iterable[InferenceRule],
    semiring: ChartSemiring | None = None,
    agenda: Agenda | None = None,
    goal: Callable[[Item], bool] | None = None,
    max_iterations: int = 100_000,
    chart: Chart | None = None,
    rule_callback: (
        Callable[
            [str, list[tuple[Item, torch.Tensor]], Item, torch.Tensor],
            None,
        ]
        | None
    ) = None,
) -> AgendaResult:
    """Run the agenda-driven deduction engine to fixed point.

    Categorical denotation: returns the least pre-fixed point of
    the rule-system functor on the input axioms. The
    strategy-independence theorem (Goodman 1999) guarantees that
    the chart's final value is independent of the ``agenda``
    discipline when ``semiring`` is idempotent.

    Algorithm (Shieber-Schabes-Pereira 1995, Fig. 2 with
    semiring-weighted aggregation per Goodman 1999):

    1. Push every axiom onto the agenda.
    2. While the agenda is non-empty:
       a. Pop an item.
       b. Insert-or-aggregate into the chart.
       c. If the chart's weight changed, fire every rule for which
          the popped item is a premise: scan the chart for matching
          siblings, compute the conclusion's weight via the rule's
          ``weight_fn``, and push the conclusion onto the agenda.
    3. Return the chart with all items that match ``goal``.

    Parameters
    ----------
    axioms : iterable of (Item, weight)
        Initial items with their input-derived weights.
    rules : iterable of InferenceRule
        The deduction system's hyperedges.
    semiring : ChartSemiring, optional
        Weight aggregation. Defaults to log-prob.
    agenda : Agenda, optional
        Evaluation strategy. Defaults to FIFO (semi-naïve).
    goal : callable, optional
        Predicate selecting result items. Defaults to "every item".
    max_iterations : int, optional
        Safety bound on agenda steps; raises if exceeded.
    chart : Chart, optional
        Initial chart (defaults to empty `HashChart`).
    rule_callback : callable, optional
        Called as ``(rule_name, antecedents, conclusion, weight)``
        after each rule firing.

    Returns
    -------
    AgendaResult
        The final chart, the goal items, and the step count.

    Raises
    ------
    RuntimeError
        If the agenda runs for more than ``max_iterations`` steps.
    """
    semiring = semiring or LOG_PROB
    agenda = agenda or FIFOAgenda()
    agenda.bind_semiring(semiring)
    chart = chart or HashChart()
    rules = tuple(rules)

    for item, w in axioms:
        agenda.push(item, w)

    iterations = 0
    while not agenda.empty():
        if iterations >= max_iterations:
            raise RuntimeError(
                f"agenda exceeded max_iterations={max_iterations}; "
                f"likely a non-terminating deduction"
            )
        iterations += 1
        item, weight = agenda.pop()
        changed = chart.insert_or_aggregate(item, weight, semiring)
        if not changed:
            continue
        # Fire every rule for which this item could be a premise.
        for rule in rules:
            for premise_idx, premise_pattern in enumerate(rule.premises):
                bindings = match(premise_pattern, item)
                if bindings is None:
                    continue
                # Collect all sibling premises by matching the
                # remaining premise patterns against the chart.
                _fire_rule_with_premise(
                    rule,
                    premise_idx,
                    item,
                    weight,
                    bindings,
                    chart,
                    semiring,
                    agenda,
                    rule_callback,
                )

    goal_items: list[tuple[Item, torch.Tensor]] = []
    if goal is not None:
        for item, w in chart.items():
            if goal(item):
                goal_items.append((item, w))
    else:
        goal_items = list(chart.items())

    return AgendaResult(
        chart=chart,
        semiring=semiring,
        goal_items=goal_items,
        iterations=iterations,
    )

cky_agenda ¶

cky_agenda() -> Agenda

The CKY (bottom-up sweep) agenda: semi-naïve FIFO.

For context-free + Boolean / inside semirings, FIFO order suffices to reach the chart's fixed point in :math:O(n^3 \cdot |R|) time (McAllester 2002).

RETURNS	DESCRIPTION
`Agenda`	A fresh `FIFOAgenda`.

Source code in src/quivers/stochastic/agenda.py

def cky_agenda() -> Agenda:
    """The CKY (bottom-up sweep) agenda: semi-naïve FIFO.

    For context-free + Boolean / inside semirings, FIFO order
    suffices to reach the chart's fixed point in
    :math:`O(n^3 \\cdot |R|)` time (McAllester 2002).

    Returns
    -------
    Agenda
        A fresh `FIFOAgenda`.
    """
    return FIFOAgenda()

earley_agenda ¶

earley_agenda() -> Agenda

The Earley (predict / scan / complete) agenda: FIFO.

Earley's algorithm is identical to FIFO agenda-driven deduction over the predict / scan / complete items (Pereira & Warren 1983).

RETURNS	DESCRIPTION
`Agenda`	A fresh `FIFOAgenda`.

Source code in src/quivers/stochastic/agenda.py

def earley_agenda() -> Agenda:
    """The Earley (predict / scan / complete) agenda: FIFO.

    Earley's algorithm is identical to FIFO agenda-driven
    deduction over the predict / scan / complete items
    (Pereira & Warren 1983).

    Returns
    -------
    Agenda
        A fresh `FIFOAgenda`.
    """
    return FIFOAgenda()

viterbi_agenda ¶

viterbi_agenda(priority_fn: Callable[[Item, Tensor], float]) -> Agenda

Viterbi-style best-first agenda.

Priorities are the current best weight in the :math:(\max, \times) semiring; the agenda is a priority queue. Equivalent to Knuth's algorithm when the semiring is superior (Nederhof 2003).

PARAMETER	DESCRIPTION
`priority_fn`	The priority of an item given its weight; higher pops first. TYPE: `Callable[[Item, Tensor], float]`

RETURNS	DESCRIPTION
`Agenda`	A `PriorityQueueAgenda` ordered by `priority_fn`.

Source code in src/quivers/stochastic/agenda.py

def viterbi_agenda(priority_fn: Callable[[Item, torch.Tensor], float]) -> Agenda:
    """Viterbi-style best-first agenda.

    Priorities are the current best weight in the
    :math:`(\\max, \\times)` semiring; the agenda is a priority
    queue. Equivalent to Knuth's algorithm when the semiring is
    superior (Nederhof 2003).

    Parameters
    ----------
    priority_fn : Callable[[Item, torch.Tensor], float]
        The priority of an item given its weight; higher pops first.

    Returns
    -------
    Agenda
        A `PriorityQueueAgenda` ordered by ``priority_fn``.
    """
    return PriorityQueueAgenda(priority_fn)

astar_agenda ¶

astar_agenda(g_plus_h: Callable[[Item, Tensor], float]) -> Agenda

A* parsing agenda (Klein & Manning 2003).

Priority is :math:g + h where :math:g is the current accumulated cost and :math:h is an admissible heuristic on the remaining cost. With an admissible :math:h, the agenda enumerates items in optimal order (Knuth 1977).

PARAMETER	DESCRIPTION
`g_plus_h`	The priority `g + h` of an item given its weight; higher pops first. TYPE: `Callable[[Item, Tensor], float]`

RETURNS	DESCRIPTION
`Agenda`	A `PriorityQueueAgenda` ordered by `g_plus_h`.

Source code in src/quivers/stochastic/agenda.py

def astar_agenda(
    g_plus_h: Callable[[Item, torch.Tensor], float],
) -> Agenda:
    """A* parsing agenda (Klein & Manning 2003).

    Priority is :math:`g + h` where :math:`g` is the current
    accumulated cost and :math:`h` is an admissible heuristic on
    the remaining cost. With an admissible :math:`h`, the agenda
    enumerates items in optimal order (Knuth 1977).

    Parameters
    ----------
    g_plus_h : Callable[[Item, torch.Tensor], float]
        The priority ``g + h`` of an item given its weight; higher pops first.

    Returns
    -------
    Agenda
        A `PriorityQueueAgenda` ordered by ``g_plus_h``.
    """
    return PriorityQueueAgenda(g_plus_h)

knuth_agenda ¶

knuth_agenda() -> Agenda

Knuth's best-first hyperpath search.

Priority is the current chart weight (the item's best-so-far score). For a superior semiring, this is Dijkstra's algorithm on AND-OR hypergraphs (Knuth 1977; Nederhof 2003).

RETURNS	DESCRIPTION
`Agenda`	A `PriorityQueueAgenda` ordered by the item's weight.

Source code in src/quivers/stochastic/agenda.py

def knuth_agenda() -> Agenda:
    """Knuth's best-first hyperpath search.

    Priority is the current chart weight (the item's best-so-far
    score). For a superior semiring, this is Dijkstra's algorithm
    on AND-OR hypergraphs (Knuth 1977; Nederhof 2003).

    Returns
    -------
    Agenda
        A `PriorityQueueAgenda` ordered by the item's weight.
    """

    def _priority(_item: Item, weight: torch.Tensor) -> float:
        return float(weight) if weight.numel() == 1 else float(weight.sum())

    return PriorityQueueAgenda(_priority)

depth_first_agenda ¶

depth_first_agenda() -> Agenda

LIFO agenda: depth-first proof search (Agda / Twelf style).

RETURNS	DESCRIPTION
`Agenda`	A fresh `LIFOAgenda`.

Source code in src/quivers/stochastic/agenda.py

def depth_first_agenda() -> Agenda:
    """LIFO agenda: depth-first proof search (Agda / Twelf style).

    Returns
    -------
    Agenda
        A fresh `LIFOAgenda`.
    """
    return LIFOAgenda()

semi_naive_agenda ¶

semi_naive_agenda() -> Agenda

Semi-naïve Datalog evaluation (McAllester 2002): FIFO.

RETURNS	DESCRIPTION
`Agenda`	A fresh `FIFOAgenda`.

Source code in src/quivers/stochastic/agenda.py

def semi_naive_agenda() -> Agenda:
    """Semi-naïve Datalog evaluation (McAllester 2002): FIFO.

    Returns
    -------
    Agenda
        A fresh `FIFOAgenda`.
    """
    return FIFOAgenda()

Agenda-based Deduction¶

Item algebra¶

Item module-attribute ¶

Pattern module-attribute ¶

Bindings module-attribute ¶

agenda ¶

Wildcard dataclass ¶

InferenceRule dataclass ¶

Chart ¶

lookup abstractmethod ¶

insert_or_aggregate abstractmethod ¶

get abstractmethod ¶

items abstractmethod ¶

HashChart ¶

lookup ¶

insert_or_aggregate ¶

get ¶

items ¶

ChartView ¶

chart property ¶

attached_loss property ¶

semiring property ¶

goal_items property ¶

weight ¶

try_weight ¶

enumerate ¶

embedding ¶

derivations ¶

goal_weight ¶

Agenda ¶

push abstractmethod ¶

pop abstractmethod ¶

empty abstractmethod ¶

bind_semiring ¶

FIFOAgenda ¶

bind_semiring ¶

push ¶

pop ¶

empty ¶

LIFOAgenda ¶

push ¶

pop ¶

empty ¶

PriorityQueueAgenda ¶

push ¶

pop ¶

empty ¶

AgendaResult dataclass ¶

DeductionSystem dataclass ¶

run ¶

parameters ¶

named_parameters ¶

make_wildcard ¶

instantiate ¶

match ¶

run_agenda ¶

cky_agenda ¶

earley_agenda ¶

viterbi_agenda ¶

astar_agenda ¶

knuth_agenda ¶

depth_first_agenda ¶

semi_naive_agenda ¶

Item `module-attribute` ¶

Pattern `module-attribute` ¶

Bindings `module-attribute` ¶

Wildcard `dataclass` ¶

InferenceRule `dataclass` ¶

lookup `abstractmethod` ¶

insert_or_aggregate `abstractmethod` ¶

get `abstractmethod` ¶

items `abstractmethod` ¶

chart `property` ¶

attached_loss `property` ¶

semiring `property` ¶

goal_items `property` ¶

push `abstractmethod` ¶

pop `abstractmethod` ¶

empty `abstractmethod` ¶

AgendaResult `dataclass` ¶

DeductionSystem `dataclass` ¶