Module

Baskerville.Kernel

Package: purescript-baskerville-core
Repository: afcondon/purescript-baskerville

The proof-term kernel: facts with justifications, hash-consed into a derivation DAG.

A Fact is a proof term — a node of the free algebra generated by the client's rules-as-constructors over its observation axioms. Recording a claim already known keeps the first justification (hash-consing), which is what makes the free tree a shared DAG. Premises always point at strictly smaller FactIds (they cite facts that already existed), so the DAG is acyclic by construction.

Type parameters, everywhere in this library:

claim — the client's atomic statements (finite, Ord).
rule — the client's rule names, an ADT so the UI can say them.
axiom — anchors: the non-fact provenance a client threads through (event ids, timestamps, "given"), on axioms and derivations alike.
residue — the client's residue: lattice state that refines between facts (candidate sets shrinking) without itself earning FactIds. Clients on the plain powerset instance use Unit.

#FactId Source

newtype FactId

Constructors

FactId Int

Instances

#Why Source

data Why rule axiom

Constructors

Axiom axiom
ByRule { anchors :: Array axiom, premises :: Array FactId, rule :: rule, source :: axiom }

Instances

(Eq rule, Eq axiom) => Eq (Why rule axiom)

#Fact Source

type Fact claim rule axiom = { alsoWhy :: Array (Why rule axiom), claim :: claim, id :: FactId, why :: Why rule axiom }

why is the primary justification — first derivation wins — and the only one the acyclicity guarantee covers: its premises point at strictly smaller ids. alsoWhy records every other way the claim was later rederived. Those may cite facts born after this one, so they are evidence of rederivability, not independently well-founded proofs — checking an alternative for well-founded support is ATMS work (extensions catalogue #7). Recording them now is what keeps that door open, and it is what lets a UI say "X-wing sees it too".

#KB Source

newtype KB residue claim rule axiom

The knowledge base: an append-only feed of facts, the hash-consing index over their claims (doubling as the premise lookup), and the client's residue.

Instances

(Eq residue, Eq claim, Eq rule, Eq axiom) => Eq (KB residue claim rule axiom)

#emptyKB Source

emptyKB :: forall residue claim rule axiom. residue -> KB residue claim rule axiom

#assertAxiom Source

assertAxiom :: forall residue claim rule axiom. Ord claim => Eq rule => Eq axiom => axiom -> claim -> KB residue claim rule axiom -> KB residue claim rule axiom

Record an observed claim — a premise-free leaf of every derivation that later cites it.

#addFact Source

addFact :: forall residue claim rule axiom. Ord claim => Eq rule => Eq axiom => { claim :: claim, why :: Why rule axiom } -> KB residue claim rule axiom -> KB residue claim rule axiom

Record a claim. News gets a fresh fact; a claim already on the feed keeps its place and its primary justification, and the new derivation is appended to alsoWhy if it is genuinely different — so a claim rederivable six ways appears once, remembering all six.

#justificationsFor Source

justificationsFor :: forall residue claim rule axiom. Ord claim => claim -> KB residue claim rule axiom -> Array (Why rule axiom)

Every recorded justification for a claim, primary first.

#sameDerivation Source

sameDerivation :: forall rule axiom. Eq rule => Eq axiom => Why rule axiom -> Why rule axiom -> Boolean

Derivation identity: what individuates a justification is its content — the rule and what it consumed — not source, which only records when the inference was first noticed. Rederiving the same conclusion from the same premises while processing a later event is the same derivation, and addFact must not collect it twice.

#isKnown Source

isKnown :: forall residue claim rule axiom. Ord claim => claim -> KB residue claim rule axiom -> Boolean

#subsumes Source

subsumes :: forall residue claim rule axiom. Ord claim => KB residue claim rule axiom -> KB residue claim rule axiom -> Boolean

Does the first mind know everything the second does? This is the law perspectives obey in a monotone system: a mind that witnessed a superset of the observations derives a superset of the claims. Perspectives themselves are client code (observation projection is domain vocabulary — see kibitzer's Observe); the library owns the property they must satisfy, and clients pin it over random streams.

#factIdFor Source

factIdFor :: forall residue claim rule axiom. Ord claim => claim -> KB residue claim rule axiom -> Maybe FactId

The fact recording a claim — the premise lookup a rule uses to cite its inputs.

#factFor Source

factFor :: forall residue claim rule axiom. Ord claim => claim -> KB residue claim rule axiom -> Maybe (Fact claim rule axiom)

#factById Source

factById :: forall residue claim rule axiom. FactId -> KB residue claim rule axiom -> Maybe (Fact claim rule axiom)

#facts Source

facts :: forall residue claim rule axiom. KB residue claim rule axiom -> Array (Fact claim rule axiom)

#factCount Source

factCount :: forall residue claim rule axiom. KB residue claim rule axiom -> Int

#knownClaims Source

knownClaims :: forall residue claim rule axiom. KB residue claim rule axiom -> Set claim

#residue Source

residue :: forall residue claim rule axiom. KB residue claim rule axiom -> residue

#withResidue Source

withResidue :: forall residue claim rule axiom. (residue -> residue) -> KB residue claim rule axiom -> KB residue claim rule axiom

Modules: Baskerville.Conformance; Baskerville.Engine; Baskerville.Explain; Baskerville.Kernel; Baskerville.Rule