Deduction Library¶
Pre-registered DeductionSystem instances for the standard
specializations of agenda-driven weighted deduction: categorial
grammar recognition, type checking, Datalog closure, shortest paths,
hidden Markov models, and edit distance. A DSL parse(NAME)
expression resolves NAME against STDLIB_DEDUCTIONS before any
user-declared deduction.
Pre-registered library of weighted deduction systems.
Ships agenda-engine DeductionSystem instances for the
canonical algorithmic specializations enumerated in the
semiring-parsing / agenda-driven-deduction literature
(Shieber-Schabes-Pereira 1995; Goodman 1999; Klein-Manning 2001;
Nederhof 2003; Eisner-Blatz 2007; Vieira et al. on Dyna).
Each entry is a DeductionSystem constructed from the
seven irreducible parameters (item algebra, rule set, semiring,
axiom injector, goal predicate, agenda factory, chart factory)
of the underlying agenda engine. Users invoke them as
.. code-block:: python
from quivers.stochastic.stdlib import CCG, Lambek, MLTT, Datalog
view = CCG(input_token_axioms)
weight = view.weight(some_item)
Categorically, each system is a section of the dependent kernel
:math:\Pi(p \in P).\ \mathbf{Kern}(\mathrm{In}(p), \mathbf{Set}^{I(p)^{\mathrm{op}}}_K)
indexed by the agenda strategy and the semiring.
module-attribute
¶
CCG = DeductionSystem(rules=tuple(_ccg_rules()), semiring=LOG_PROB, axiom_injector=lambda axioms: list(axioms), goal=lambda item: isinstance(item, tuple) and item[0] == 'span' and item[1] == 'S', agenda_factory=cky_agenda)
Combinatory categorial grammar recognition: forward and backward application over slash items, log-probability semiring, CKY agenda.
module-attribute
¶
Lambek = DeductionSystem(rules=tuple(_lambek_rules()), semiring=LOG_PROB, axiom_injector=lambda axioms: list(axioms), goal=lambda item: isinstance(item, tuple) and item[0] == 'span' and item[1] == 'S', agenda_factory=cky_agenda)
Lambek calculus recognition: forward and backward application, log-probability semiring, CKY agenda.
module-attribute
¶
STLC = DeductionSystem(rules=tuple(_stlc_rules()), semiring=BOOLEAN, axiom_injector=lambda axioms: list(axioms), goal=lambda item: isinstance(item, tuple) and item[0] in ('synth', 'check'), agenda_factory=depth_first_agenda)
Bidirectional type checking for the simply-typed lambda calculus, Boolean semiring.
module-attribute
¶
MLTT = DeductionSystem(rules=tuple(_mltt_rules()), semiring=BOOLEAN, axiom_injector=lambda axioms: list(axioms), goal=lambda item: isinstance(item, tuple) and item[0] == 'judges', agenda_factory=depth_first_agenda, max_iterations=10000)
Bidirectional type checking for a fragment of Martin-Löf dependent type theory, Boolean semiring, with a bound on term depth.
module-attribute
¶
Datalog = DeductionSystem(rules=tuple(_datalog_transitive_closure_rules()), semiring=BOOLEAN, axiom_injector=lambda axioms: list(axioms), goal=lambda item: isinstance(item, tuple) and item[0] == 'reach', agenda_factory=semi_naive_agenda)
Transitive closure of an edge relation by semi-naive Datalog evaluation, Boolean semiring.
module-attribute
¶
Dijkstra = DeductionSystem(rules=tuple(_dijkstra_rules()), semiring=VITERBI, axiom_injector=lambda axioms: list(axioms), goal=lambda item: isinstance(item, tuple) and item[0] == 'dist', agenda_factory=knuth_agenda)
Single-source shortest paths by Knuth's generalization of Dijkstra's algorithm, Viterbi semiring.
module-attribute
¶
HMM = DeductionSystem(rules=tuple(_hmm_forward_rules()), semiring=LOG_PROB, axiom_injector=lambda axioms: list(axioms), goal=lambda item: isinstance(item, tuple) and item[0] == 'alpha', agenda_factory=cky_agenda)
The hidden Markov model forward algorithm over alpha items, log-probability semiring.
module-attribute
¶
ViterbiHMM = DeductionSystem(rules=tuple(_hmm_forward_rules()), semiring=VITERBI, axiom_injector=lambda axioms: list(axioms), goal=lambda item: isinstance(item, tuple) and item[0] == 'alpha', agenda_factory=cky_agenda)
The hidden Markov model Viterbi algorithm: the HMM rules under the Viterbi semiring.
module-attribute
¶
EditDistance = DeductionSystem(rules=tuple(_edit_distance_rules()), semiring=VITERBI, axiom_injector=lambda axioms: list(axioms), goal=lambda item: isinstance(item, tuple) and item[0] == 'dist', agenda_factory=cky_agenda)
Levenshtein edit distance over dist alignment items, Viterbi semiring.
module-attribute
¶
STDLIB_DEDUCTIONS: dict[str, DeductionSystem] = {'CCG': CCG, 'Lambek': Lambek, 'STLC': STLC, 'MLTT': MLTT, 'Datalog': Datalog, 'Dijkstra': Dijkstra, 'HMM': HMM, 'ViterbiHMM': ViterbiHMM, 'EditDistance': EditDistance}
Mapping from name to pre-registered deduction system.
Compilation of a parse(NAME) expression in the DSL, or a
direct call from Python, resolves the name against this dict
first, then against any user-declared deductions in the
compiler's environment.