Deductive Systems, Rule Schemas, and Span Components¶

The abstract framework for weighted deductive parsing, organized into three layers:

Deductive Systems¶

Five abstract primitives for weighted deductive parsing (Shieber, Schabes & Pereira 1995; Goodman 1999). All parsing algorithms are instances of this framework.

Axiom: Creates and populates the initial chart from input.
Deduction: A weighted inference step (chart → chart).
Goal: Extracts the result from a completed chart.
Schedule: Evaluation strategy (CKY bottom-up, Earley, agenda-based).
DeductiveSystem: Ties axiom, deductions, goal, schedule, and semiring into a single nn.Module.

For the full surface, see api/stochastic/deduction. The primitives themselves are documented at api/stochastic/deduction/primitives.

Rule Schemas¶

Composable functors CategorySystem → RuleSystem. Schemas are the abstract building blocks of grammar formalisms: each schema defines a structural rule pattern, and concrete rule instances are generated by instantiating the pattern over a finite category inventory.

Schemas compose via | (union) and can carry default weights via .weighted(w). Grammar formalisms are specific compositions:

CCG = EVALUATION | HARMONIC_COMPOSITION | CROSSED_COMPOSITION
LAMBEK = EVALUATION | ADJUNCTION_UNITS | TENSOR_INTRODUCTION | TENSOR_PROJECTION
NL = EVALUATION
LP = EVALUATION | COMMUTATIVE_EVALUATION | ADJUNCTION_UNITS

The ~20 atomic schemas (e.g. ForwardApplication, BackwardApplication) compose into 13 bundled schemas (e.g. EVALUATION, HARMONIC_COMPOSITION), which compose into grammar presets (CCG, LAMBEK, NL, LP).

schema ¶

Rule schemas: composable functors from CategorySystem to RuleSystem.

A RuleSchema is a functor that maps a CategorySystem to a RuleSystem. Schemas are the abstract building blocks of grammar formalisms: each schema defines a structural rule pattern, and concrete rule instances are generated by instantiating the pattern over a finite category inventory.

The two atomic schema types are:

BinaryRuleSchema — defined by a match predicate on category pairs: match(left, right) -> result | None.
UnaryRuleSchema — defined by a match predicate on single categories: match(cat, system) -> list[result].

Schemas compose via | (union) and can carry default weights via .weighted(w). Grammar formalisms are specific compositions::

CCG = EVALUATION | HARMONIC_COMPOSITION | CROSSED_COMPOSITION
LAMBEK = EVALUATION | ADJUNCTION_UNITS | TENSOR_INTRODUCTION | TENSOR_PROJECTION

The 13 bundled schemas (EVALUATION, HARMONIC_COMPOSITION, etc.) are themselves composed from ~20 atomic schemas (ForwardApplication, BackwardApplication, etc.), giving fine-grained control::

# only forward application, no backward
MY_GRAMMAR = ForwardApplication() | ForwardComposition()

RuleSchema ¶

Bases: ABC

A functor CategorySystem -> RuleSystem.

Schemas are the abstract specification of structural rules. They compose via | (union) and + (alias for |).

call `abstractmethod` ¶

__call__(system: CategorySystem) -> RuleSystem

Instantiate this schema over a category system.

PARAMETER	DESCRIPTION
`system`	The finite category inventory. TYPE: `CategorySystem`

RETURNS	DESCRIPTION
`RuleSystem`	Concrete rules for this schema.

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

@abstractmethod
def __call__(self, system: CategorySystem) -> RuleSystem:
    """Instantiate this schema over a category system.

    Parameters
    ----------
    system : CategorySystem
        The finite category inventory.

    Returns
    -------
    RuleSystem
        Concrete rules for this schema.
    """
    ...

or ¶

__or__(other: RuleSchema) -> RuleSchema

Union of two schemas.

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

def __or__(self, other: RuleSchema) -> RuleSchema:
    """Union of two schemas."""
    return UnionSchema(self, other)

add ¶

__add__(other: RuleSchema) -> RuleSchema

Alias for union.

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

def __add__(self, other: RuleSchema) -> RuleSchema:
    """Alias for union."""
    return self | other

weighted ¶

weighted(weight: float) -> RuleSchema

Attach a default weight to all rules from this schema.

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

def weighted(self, weight: float) -> RuleSchema:
    """Attach a default weight to all rules from this schema."""
    return WeightedSchema(self, weight)

UnionSchema ¶

UnionSchema(left: RuleSchema, right: RuleSchema)

Bases: RuleSchema

Union of two schemas (composes their rule systems via +).

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

def __init__(self, left: RuleSchema, right: RuleSchema) -> None:
    self._left = left
    self._right = right

WeightedSchema ¶

WeightedSchema(inner: RuleSchema, weight: float)

Bases: RuleSchema

Schema wrapper that attaches a default weight to all rules.

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

def __init__(self, inner: RuleSchema, weight: float) -> None:
    self._inner = inner
    self._weight = weight

BinaryRuleSchema ¶

Bases: RuleSchema

Schema for binary rules, defined by a match predicate.

Subclasses implement match(left, right) -> result | None. The schema iterates over all category pairs and collects matches.

match `abstractmethod` ¶

match(left: Category, right: Category) -> Category | None

Test whether (left, right) triggers this rule.

PARAMETER	DESCRIPTION
`left`	Left antecedent. TYPE: `Category`
`right`	Right antecedent. TYPE: `Category`

RETURNS	DESCRIPTION
`Category or None`	Result category if the pair matches, else None.

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

@abstractmethod
def match(
    self,
    left: Category,
    right: Category,
) -> Category | None:
    """Test whether (left, right) triggers this rule.

    Parameters
    ----------
    left : Category
        Left antecedent.
    right : Category
        Right antecedent.

    Returns
    -------
    Category or None
        Result category if the pair matches, else None.
    """
    ...

UnaryRuleSchema ¶

Bases: RuleSchema

Schema for unary rules, defined by a match predicate.

Subclasses implement match(cat, system) -> list[result]. The schema iterates over all categories and collects matches.

match `abstractmethod` ¶

match(cat: Category, system: CategorySystem) -> list[Category]

Find all valid results for a given input category.

PARAMETER	DESCRIPTION
`cat`	Input category. TYPE: `Category`
`system`	The full category inventory (needed for some schemas that must check existence of intermediate categories). TYPE: `CategorySystem`

RETURNS	DESCRIPTION
`list[Category]`	Valid result categories.

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

@abstractmethod
def match(
    self,
    cat: Category,
    system: CategorySystem,
) -> list[Category]:
    """Find all valid results for a given input category.

    Parameters
    ----------
    cat : Category
        Input category.
    system : CategorySystem
        The full category inventory (needed for some schemas
        that must check existence of intermediate categories).

    Returns
    -------
    list[Category]
        Valid result categories.
    """
    ...

ForwardApplication ¶

Bases: BinaryRuleSchema

C/B ⊗ B → C (right evaluation / forward application).

BackwardApplication ¶

Bases: BinaryRuleSchema

A ⊗ A\C → C (left evaluation / backward application).

ForwardComposition ¶

Bases: BinaryRuleSchema

C/B ⊗ B/A → C/A (right harmonic composition).

BackwardComposition ¶

Bases: BinaryRuleSchema

A\B ⊗ B\C → A\C (left harmonic composition).

ForwardCrossedComposition ¶

Bases: BinaryRuleSchema

C/B ⊗ B\A → C\A (right-left crossed composition).

BackwardCrossedComposition ¶

Bases: BinaryRuleSchema

A/B ⊗ B\C → A/C (left-right crossed composition).

CommutativeForwardApplication ¶

Bases: BinaryRuleSchema

B ⊗ C/B → C (commutative right evaluation).

CommutativeBackwardApplication ¶

Bases: BinaryRuleSchema

A\C ⊗ A → C (commutative left evaluation).

TensorIntroduction ¶

Bases: BinaryRuleSchema

A ⊗ B → A⊗B (product formation).

LeftUnitElimination ¶

Bases: BinaryRuleSchema

I ⊗ A → A (left unitor).

RightUnitElimination ¶

Bases: BinaryRuleSchema

A ⊗ I → A (right unitor).

ModalApplication ¶

ModalApplication(modality: str = '◇')

Bases: BinaryRuleSchema

◇(C/B) ⊗ ◇B → ◇C (modal function application).

PARAMETER	DESCRIPTION
`modality`	The modality symbol (e.g. "◇", "□"). TYPE: `str` DEFAULT: `'◇'`

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

def __init__(self, modality: str = "◇") -> None:
    self._modality = modality

RightLifting ¶

Bases: UnaryRuleSchema

A → C/(A\C) (right adjunction unit / type raising).

LeftLifting ¶

Bases: UnaryRuleSchema

A → (C/A)\C (left adjunction unit / type raising).

LeftProjection ¶

Bases: UnaryRuleSchema

A⊗B → A (left tensor projection).

RightProjection ¶

Bases: UnaryRuleSchema

A⊗B → B (right tensor projection).

UnitCoercion ¶

Bases: UnaryRuleSchema

A → I (unit elimination / weakening).

ModalInjection ¶

ModalInjection(modality: str = '◇')

Bases: UnaryRuleSchema

A → ◇A (modal introduction).

PARAMETER	DESCRIPTION
`modality`	The modality symbol (e.g. "◇", "□"). TYPE: `str` DEFAULT: `'◇'`

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

def __init__(self, modality: str = "◇") -> None:
    self._modality = modality

ModalProjection ¶

ModalProjection(modality: str = '◇')

Bases: UnaryRuleSchema

◇A → A (modal elimination).

PARAMETER	DESCRIPTION
`modality`	The modality symbol (e.g. "◇", "□"). TYPE: `str` DEFAULT: `'◇'`

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

def __init__(self, modality: str = "◇") -> None:
    self._modality = modality

GeneralizedComposition ¶

GeneralizedComposition(max_depth: int = 2)

Bases: RuleSchema

Generalized composition through nested slashes (B^n).

C/B ⊗ (B|₁Z₁)|₂Z₂...|ₙZₙ → (C|₁Z₁)|₂Z₂...|ₙZₙ

This is a special schema because the match recurses into nested slash structure. At depth 1 it is ordinary harmonic composition; this schema only generates rules for depth >= 2.

PARAMETER	DESCRIPTION
`max_depth`	Maximum nesting depth to traverse. TYPE: `int` DEFAULT: `2`

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

def __init__(self, max_depth: int = 2) -> None:
    self._max_depth = max_depth

PatternBinarySchema ¶

PatternBinarySchema(left_pattern, right_pattern, conclusion_pattern, variables: frozenset[str], name: str = '')

Bases: BinaryRuleSchema

Binary rule schema from a DSL rule declaration.

Matches category pairs against two premise patterns and instantiates the conclusion pattern with bound variables.

PARAMETER	DESCRIPTION
`left_pattern`	Category pattern for the left antecedent.
`right_pattern`	Category pattern for the right antecedent.
`conclusion_pattern`	Category pattern for the consequent.
`variables`	Universally quantified pattern variables. TYPE: `frozenset of str`
`name`	The rule's name (for description). TYPE: `str` DEFAULT: `''`

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

def __init__(
    self,
    left_pattern,
    right_pattern,
    conclusion_pattern,
    variables: frozenset[str],
    name: str = "",
) -> None:
    self._left = left_pattern
    self._right = right_pattern
    self._conclusion = conclusion_pattern
    self._variables = variables
    self._name = name

PatternUnarySchema ¶

PatternUnarySchema(premise_pattern, conclusion_pattern, variables: frozenset[str], name: str = '')

Bases: UnaryRuleSchema

Unary rule schema from a DSL rule declaration.

Matches a single category against a premise pattern and instantiates the conclusion pattern with bound variables.

PARAMETER	DESCRIPTION
`premise_pattern`	Category pattern for the antecedent.
`conclusion_pattern`	Category pattern for the consequent.
`variables`	Universally quantified pattern variables. TYPE: `frozenset of str`
`name`	The rule's name (for description). TYPE: `str` DEFAULT: `''`

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

def __init__(
    self,
    premise_pattern,
    conclusion_pattern,
    variables: frozenset[str],
    name: str = "",
) -> None:
    self._premise = premise_pattern
    self._conclusion = conclusion_pattern
    self._variables = variables
    self._name = name

generalized_composition ¶

generalized_composition(max_depth: int = 2) -> RuleSchema

Create a generalized composition schema.

PARAMETER	DESCRIPTION
`max_depth`	Maximum nesting depth. TYPE: `int` DEFAULT: `2`

RETURNS	DESCRIPTION
`RuleSchema`	The generalized composition schema.

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

def generalized_composition(max_depth: int = 2) -> RuleSchema:
    """Create a generalized composition schema.

    Parameters
    ----------
    max_depth : int
        Maximum nesting depth.

    Returns
    -------
    RuleSchema
        The generalized composition schema.
    """
    return GeneralizedComposition(max_depth)

Span-Based CKY Components¶

Span-based instantiation of the abstract deductive framework for CKY chart parsing:

LexicalAxiom: Populates length-1 spans from a learnable lexicon.
BinarySpanDeduction: Applies binary structural rules with learnable weights.
UnarySpanDeduction: Applies unary rules to convergence.
SpanGoal: Extracts the start-symbol score for the full span.
CKYSchedule: Bottom-up evaluation by span length.

span ¶

Span-based CKY components for the deductive system framework.

This module instantiates the abstract deduction primitives (Axiom, Deduction, Goal, Schedule) for span-indexed chart parsing (CKY). Items are indexed by (i, j, A) where [i, j) is a string span and A is a category index.

The chart tensor has shape (batch, n_categories, seq_len, seq_len+1) (categories-first for efficient indexing of the start symbol).

Components

LexicalAxiom Populates length-1 spans from a learnable lexicon. BinarySpanDeduction Applies binary rules: chart[i,k,L] ⊗ chart[k,j,R] → chart[i,j,A]. UnarySpanDeduction Applies unary rules iteratively to convergence. SpanGoal Extracts chart[start_cat, 0, seq_len]. CKYSchedule Bottom-up evaluation by span length.

LexicalAxiom ¶

LexicalAxiom(n_terminals: int, n_categories: int)

Bases: Axiom

Populate length-1 spans from a learnable lexicon.

Creates the chart tensor and fills chart[b, :, i, i+1] = log_softmax(lexicon[tokens[b, i]]).

PARAMETER	DESCRIPTION
`n_terminals`	Vocabulary size. TYPE: `int`
`n_categories`	Number of category types. TYPE: `int`

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

def __init__(self, n_terminals: int, n_categories: int) -> None:
    super().__init__()
    self._n_cat = n_categories
    self.lexicon_logits = nn.Parameter(torch.randn(n_terminals, n_categories) * 0.1)

log_lexicon `property` ¶

log_lexicon: Tensor

Log-probability lexicon, shape (n_terminals, n_categories).

BinarySpanDeduction ¶

BinarySpanDeduction(rule_system: RuleSystem, learnable: bool = True)

Bases: Deduction

Binary rule application over span items.

For each split point k in [i+1, j), combines chart[i, k, lefts] and chart[k, j, rights] to produce chart[i, j, results].

PARAMETER	DESCRIPTION
`rule_system`	The structural rules. TYPE: `RuleSystem`
`learnable`	Whether rule weights are learnable. TYPE: `bool` DEFAULT: `True`

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

def __init__(
    self,
    rule_system: RuleSystem,
    learnable: bool = True,
) -> None:
    super().__init__()

    results, lefts, rights = rule_system.binary_tensors()
    self.register_buffer("_results", results)
    self.register_buffer("_lefts", lefts)
    self.register_buffer("_rights", rights)
    self._n_rules = rule_system.n_binary

    weights = rule_system.binary_weight_tensor()

    if learnable and self._n_rules > 0:
        self.weights = nn.Parameter(weights)

    else:
        self.register_buffer("weights", weights)

forward ¶

forward(chart, semiring, **context)

Apply binary rules for one span cell (i, j).

Expected context keys: i, j, chart_cells. Returns the (batch, C) tensor for cell (i, j).

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

def forward(self, chart, semiring, **context):
    """Apply binary rules for one span cell (i, j).

    Expected context keys: ``i``, ``j``, ``chart_cells``.
    Returns the (batch, C) tensor for cell (i, j).
    """
    i = context["i"]
    j = context["j"]
    chart_cells = context["chart_cells"]
    n_categories = context["n_categories"]

    _results = cast(torch.Tensor, self._results)
    _lefts = cast(torch.Tensor, self._lefts)
    _rights = cast(torch.Tensor, self._rights)

    if self._n_rules == 0:
        return torch.full(
            (chart_cells[(i, i + 1)].shape[0], n_categories),
            semiring.zero,
            device=_results.device,
        )

    parts = []

    for k in range(i + 1, j):
        left_cell = chart_cells[(i, k)]
        right_cell = chart_cells[(k, j)]

        left_scores = left_cell[:, _lefts]
        right_scores = right_cell[:, _rights]
        combined = semiring.times(left_scores, right_scores)

        if self._n_rules > 0:
            combined = semiring.times(
                combined,
                self.weights.unsqueeze(0),
            )

        parts.append(combined)

    stacked = torch.stack(parts, dim=0)
    split_scores = semiring.plus(stacked, dim=0)

    return _scatter_semiring(
        split_scores,
        _results,
        n_categories,
        split_scores.shape[0],
        device=_results.device,
        semiring=semiring,
    )

UnarySpanDeduction ¶

UnarySpanDeduction(rule_system: RuleSystem, learnable: bool = True, iterations: int = 3)

Bases: Deduction

Unary rule application, iterated to approximate fixpoint.

PARAMETER	DESCRIPTION
`rule_system`	The structural rules. TYPE: `RuleSystem`
`learnable`	Whether rule weights are learnable. TYPE: `bool` DEFAULT: `True`
`iterations`	Number of fixpoint iterations. TYPE: `int` DEFAULT: `3`

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

def __init__(
    self,
    rule_system: RuleSystem,
    learnable: bool = True,
    iterations: int = 3,
) -> None:
    super().__init__()

    unary = rule_system.unary_tensors()

    if unary is not None:
        self.register_buffer("_results", unary[0])
        self.register_buffer("_inputs", unary[1])

    else:
        self.register_buffer(
            "_results",
            torch.zeros(0, dtype=torch.long),
        )
        self.register_buffer(
            "_inputs",
            torch.zeros(0, dtype=torch.long),
        )

    self._n_rules = rule_system.n_unary
    self._iterations = iterations

    weights = rule_system.unary_weight_tensor()

    if learnable and self._n_rules > 0:
        self.weights = nn.Parameter(weights)

    else:
        self.register_buffer("weights", weights)

has_rules `property` ¶

has_rules: bool

Whether this deduction has any unary rules.

forward ¶

forward(chart, semiring, **context)

Apply unary rules to a cell tensor.

Expects chart to be a (batch, C) cell tensor. Returns updated (batch, C) tensor.

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

def forward(self, chart, semiring, **context):
    """Apply unary rules to a cell tensor.

    Expects ``chart`` to be a (batch, C) cell tensor.
    Returns updated (batch, C) tensor.
    """
    cell = chart

    if not self.has_rules:
        return cell

    _results = cast(torch.Tensor, self._results)
    _inputs = cast(torch.Tensor, self._inputs)
    n_categories = cell.shape[1]

    for _ in range(self._iterations):
        input_scores = cell[:, _inputs]

        if self._n_rules > 0:
            input_scores = semiring.times(
                input_scores,
                self.weights.unsqueeze(0),
            )

        additions = _scatter_semiring(
            input_scores,
            _results,
            n_categories,
            cell.shape[0],
            device=cell.device,
            semiring=semiring,
        )

        cell = semiring.plus_pair(cell, additions)

    return cell

SpanGoal ¶

SpanGoal(start_idx: int)

Bases: Goal

Extract chart[start_cat, 0, seq_len].

PARAMETER	DESCRIPTION
`start_idx`	Index of the start category. TYPE: `int`

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

def __init__(self, start_idx: int) -> None:
    super().__init__()
    self._start_idx = start_idx

CKYSchedule ¶

Bases: Schedule

Bottom-up CKY: process spans in increasing length order.

For each span length 2..n: 1. Apply binary deductions for each cell (i, i+span_len). 2. Apply unary deductions to the resulting cell.

Deductive Systems, Rule Schemas, and Span Components¶