Module

Baskerville.Conformance

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

The ⊨ side of the seam: measure a rule system (⊢) against a model enumeration.

The client supplies the Oracle — the finite set of worlds consistent with its observations (not with the engine's conclusions: the oracle must be independent of the thing it judges), a satisfaction relation, and the finite claim universe. Everything else is counting, which is the lesson the bettor taught: for finite universes the semantic side needs no solver.

The instruments:

unsound — claims the engine believes that some world refutes. Always empty for a sound rule set; a non-empty result is a bug (or contradictory observations, which worlds == [] exposes).
gap — claims true in every world that the engine has not derived: the completeness gap, the honest number kibitzer measured against Z3 and any client can now measure natively.
explainOr — the seam made into a function: a proof, or a countermodel, or Underived (the gap, pointed at one claim).

#Oracle Source

type Oracle world claim = { holds :: world -> claim -> Boolean, universe :: Array claim, worlds :: Array world }

#entailed Source

entailed :: forall world claim. Oracle world claim -> claim -> Boolean

True in every world. An empty world set entails nothing (rather than everything): contradictory observations should read as "no possible world", not as universal truth.

#countermodel Source

countermodel :: forall world claim. Oracle world claim -> claim -> Maybe world

A world where the claim fails, if one survives.

#unsound Source

unsound :: forall residue world claim rule axiom. Ord claim => Oracle world claim -> KB residue claim rule axiom -> Array claim

Claims the engine believes that the oracle refutes. Soundness means this is empty, on every stream, at every position.

#gap Source

gap :: forall residue world claim rule axiom. Ord claim => Oracle world claim -> KB residue claim rule axiom -> Array claim

Claims true in every world that the engine has not derived — the completeness gap.

#Refutation Source

data Refutation world

Constructors

Countermodel world
Underived
Entailed by every world, underivable by the rules: the gap, pointed at one claim.
NoWorlds
No world survives the observations at all — they contradict.

#explainOr Source

explainOr :: forall residue world claim rule axiom. Ord claim => Oracle world claim -> KB residue claim rule axiom -> claim -> Either (Refutation world) (DerivationDag claim rule axiom)

The seam: ⊢ if the engine can, else what ⊨ has to say about it.

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