Deduction elaboration¶
Elaboration of deduction declarations into QIEC families, handlers, and
computations.
Internal module
This module is an implementation detail of the compiler and its
tooling. Its __all__ is empty, so none of the names below are
part of the public API, and they may change without notice.
Elaborate deduction declarations into kernel computations.
A weighted deductive system is a closed data family of items, a
computation enumerating its derivations, and a pair of handlers
aggregating them. The family declares one nullary constructor per atom
and one constructor per applied symbol the rules and lexicon mention,
with a slot typed Int where the system uses it as a position and
Item otherwise. Rules become branches of a recursive computation
that performs choose on the deduction's Search instance to pick
an axiom or a rule, derives each premise by recursion, matches the
derived item against the premise pattern by case analysis (a shared
pattern variable is checked by the family's structural equality
computation), instantiates the conclusion, and adds the rule's weight
on the deduction's Weight[K] instance, where K is the carrier of
the declared semiring. A failed match performs an empty choice, which
the search handler answers by resuming nobody.
The entry computation handles the Weight instance with a collecting
handler and the Search instance with a handler that resumes once per
alternative and combines the shots by the semiring's addition, so the
answer is the semiring sum over derivations of the goal of the product
of the weights along each: the inside weight of the goal. Learned
weights are read through the module's params instance of Param,
under names the classic engine keys its parameters by, so a program
that calls the deduction and scores its answer leaves params in its
row for the run to serve.
A system whose rules all relate span items enumerates by span: the
derivation of span(i, j, ...) chooses split positions for the
premise positions the conclusion leaves free and derives each premise
over its own span, so the search is bounded by the sentence, and only a
unary rule, which keeps the span, needs the declaration's depth
option to bound it. Any other system takes its axioms and their weights
as input and enumerates derivations of any item to the depth the
option declares, or to the number of axioms and rules together without
one. The agenda engine tabulates the same derivations; the two agree on
every system whose derivations of the goal fit the bound.