Agenda-based Deduction

The concrete chart implementation underlying every weighted deduction in the DSL. DeductionSystem ties an axiom injector, a rule system, a semiring, and an agenda schedule into an nn.Module; ChartView is the differentiable presheaf returned from DeductionSystem.__call__.

For the user-facing surface (fit, sample, NUTS wrap), see api/stochastic/deduction.

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.

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.

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 — 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.

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."""
    ...

insert_or_aggregate abstractmethod

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

Insert or aggregate an item's weight.

Returns 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.

    Returns ``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.

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."""
    ...

items abstractmethod

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

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

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."""
    ...

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.

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)

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.

We make this distinction observable by terminating the agenda when the per-item update falls below _tolerance. The default tolerance 0.0 recovers the original strict-equality semantics; positive tolerances expose convergent cyclic fixed points while still routing divergent systems through the agenda's max_iterations safety net.

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.

    We make this distinction observable by terminating the
    agenda when the per-item update falls below
    `_tolerance`. The default tolerance ``0.0`` recovers
    the original strict-equality semantics; positive
    tolerances expose convergent cyclic fixed points while
    still routing divergent systems through the agenda's
    ``max_iterations`` safety net.
    """
    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

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.

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.

Raises KeyError if the item was never derived. Returns a differentiable torch.Tensor.

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

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

    Raises `KeyError` if the item was never derived.
    Returns a differentiable `torch.Tensor`.
    """
    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 default (or the semiring's zero) if the item is absent.

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 ``default`` (or the
    semiring's zero) if the item is absent."""
    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. The returned weights are differentiable.

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. The returned weights are
    differentiable.
    """
    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.

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.
    """
    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 set of items derived under item in the chart's derivation forest.

For the current implementation (which records only the aggregate weight at each item), this returns the chart's item set as a flat enumeration. The full derivation forest — a tree-structured object whose leaves are axioms and whose internal nodes are rule firings — is recoverable by re-running the agenda with the derivation semiring (a follow-up upgrade); the public surface here keeps the entry point in place for that upgrade.

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

def derivations(self, item: Item) -> list[Item]:
    """Return the set of items derived under ``item`` in the
    chart's derivation forest.

    For the current implementation (which records only the
    aggregate weight at each item), this returns the chart's
    item set as a flat enumeration. The full derivation
    forest — a tree-structured object whose leaves are
    axioms and whose internal nodes are rule firings — is
    recoverable by re-running the agenda with the derivation
    semiring (a follow-up upgrade); the public surface here
    keeps the entry point in place for that upgrade.
    """
    # 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).

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).
    """
    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).

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.

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

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

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]] = []

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

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.

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

def run(self, input_value: Any) -> AgendaResult:
    """Run the deduction system on an input value."""
    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=self.goal,
        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

__call__

__call__(input_value: Any) -> ChartView

Run the deduction and return a ChartView.

Convenience for the user-facing presheaf-evaluation API: the chart's weights are differentiable tensors, and the view exposes weight, enumerate, derivations, and goal_weight methods for downstream programs.

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

def __call__(self, input_value: Any) -> ChartView:
    """Run the deduction and return a `ChartView`.

    Convenience for the user-facing presheaf-evaluation API:
    the chart's weights are differentiable tensors, and the
    view exposes ``weight``, ``enumerate``, ``derivations``,
    and ``goal_weight`` methods for downstream programs.
    """
    return ChartView(self.run(input_value))

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.

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.
    """
    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.

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."""
    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.

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

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

instantiate

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

Substitute wildcards in a pattern with their bound values.

Returns a concrete item with no wildcards. Raises KeyError if a wildcard in the pattern has no binding.

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.

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

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

    Returns a concrete item with no wildcards. Raises
    `KeyError` if a wildcard in the pattern has no binding.

    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.
    """
    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.

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."""
    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):

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.

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

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`).
    """
    semiring = semiring or LOG_PROB
    agenda = agenda or FIFOAgenda()
    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).

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).
    """
    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).

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).
    """
    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).

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).
    """
    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).

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).
    """
    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).

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).
    """

    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).

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

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

semi_naive_agenda

semi_naive_agenda() -> Agenda

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

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

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