Baskerville.Engine
- Package
- purescript-baskerville-core
- Repository
- afcondon/purescript-baskerville
The saturation engine: a Kleene least fixpoint of monotone rules over the knowledge base.
Rules here are in prim form — plain functions from the KB to derived claims. (The analyzable eDSL over a Match functor, and the semi-naive scheduling its read-sets enable, layer on top of this; the naive fixpoint below is the semantics they must agree with.)
Termination is by monotonicity: rules only add claims to a finite
universe, refine only moves the residue down its (finite) lattice,
and no fact is ever retracted — so a pass that changes nothing is the
fixpoint and one must come.
Rule order within a pass is part of the observable spec: it decides which justification a multiply-derivable fact receives, and clients pin their feeds with golden tests.
#Derivation Source
type Derivation claim rule axiom = { anchors :: Array axiom, claim :: claim, premises :: Array FactId, rule :: rule }What a single rule may emit: a claim, under the rule's name, citing the prior facts it consumed and any non-fact anchors it drew on.
#Rule Source
type Rule residue claim rule axiom = KB residue claim rule axiom -> Array (Derivation claim rule axiom)#Engine Source
type Engine residue claim rule axiom = { refine :: KB residue claim rule axiom -> residue -> residue, rules :: Array (Rule residue claim rule axiom) }A client's inference system: its rules, and its residue refinement —
the step that moves lattice state (candidate sets shrinking) between
fact derivations. Clients with no residue pass refine: \_ -> identity.
#saturate Source
saturate :: forall residue claim rule axiom. Ord claim => Eq rule => Eq axiom => Eq residue => Engine residue claim rule axiom -> axiom -> KB residue claim rule axiom -> KB residue claim rule axiomRun the rules to fixpoint. source stamps every fact derived during
this saturation with the processing context that triggered it — for
stream clients, the event whose avalanche this is.
#learn Source
learn :: forall residue claim rule axiom. Ord claim => Eq rule => Eq axiom => Eq residue => Engine residue claim rule axiom -> KB residue claim rule axiom -> { claims :: Array claim, source :: axiom } -> KB residue claim rule axiomRecord one observation's axioms, then saturate: the fold step that
makes a mind from a stream. foldl (learn engine) kb observations.