The Specified half of the predAll / predExists / predInstance / predSpecified matrix (docs/predall.md, resources/kb/CxCore.txt).
Reached from outside through vaelii.core/specified-violations and
vaelii.core/all-specified-violations. This namespace sits above vaelii.core,
because auditing is asking and the audit asks through the public read path, so the
delegation runs back down through vaelii.impl.wiring.
Where the Instance relations stamp real inference and the Exists relations are
inert records beside a sanctioned placeholder functor, predAllSpecified / predSpecifiedAll are an integrity
audit: given a declaration that every instance of a collection ought to have a
determinate filler, the reader here returns the instances that do not. It is not a
stored rule and concludes nothing — it reads the declaration and the beliefs and hands
back the violations, the way a solve-time report does.
Indeterminate = the indeterminate_term category. A filler counts as determinate
unless it is a member of the extensible indeterminate_term collection (CxCore.txt).
Skolem constants are its built-in first member — a reified NAT whose expression is a
SkolemFn application (docs/skolem.md), detected structurally because a skolem's
membership is never a stored fact — and a further kind is added with
(genl NewKind indeterminate_term). Whether a non-skolem NAT is determinate by default
is punted (Pace): a plain individual, a literal and an Exists placeholder alike are
all treated as determinate here, which is what makes predAllSpecified the exact
antagonist of predAllExists.
The *Specified* half of the predAll / predExists / predInstance / predSpecified matrix (docs/predall.md, resources/kb/CxCore.txt). Reached from outside through `vaelii.core/specified-violations` and `vaelii.core/all-specified-violations`. This namespace sits **above** `vaelii.core`, because auditing is asking and the audit asks through the public read path, so the delegation runs back down through `vaelii.impl.wiring`. Where the *Instance* relations stamp real inference and the *Exists* relations are inert records beside a sanctioned placeholder functor, `predAllSpecified` / `predSpecifiedAll` are an **integrity audit**: given a declaration that every instance of a collection ought to have a *determinate* filler, the reader here returns the instances that do not. It is not a stored rule and concludes nothing — it reads the declaration and the beliefs and hands back the violations, the way a solve-time report does. **Indeterminate = the `indeterminate_term` category.** A filler counts as determinate unless it is a member of the extensible `indeterminate_term` collection (CxCore.txt). Skolem constants are its built-in first member — a reified NAT whose expression is a `SkolemFn` application (docs/skolem.md), detected structurally because a skolem's membership is never a stored fact — and a further kind is added with `(genl NewKind indeterminate_term)`. Whether a non-skolem NAT is determinate by default is punted (Pace): a plain individual, a literal and an *Exists* placeholder alike are all treated as determinate here, which is what makes `predAllSpecified` the exact antagonist of `predAllExists`.
(all-specified-violations kb ctx)Audit every predAllSpecified and predSpecifiedAll declaration visible in ctx and
return a map {[functor pred indep dep] #{violating-instances…}}, omitting the
declarations that hold. The one call an integrity sweep makes; specified-violations
is the per-declaration reader it is built from.
Audit every `predAllSpecified` and `predSpecifiedAll` declaration visible in `ctx` and
return a map `{[functor pred indep dep] #{violating-instances…}}`, omitting the
declarations that hold. The one call an integrity sweep makes; `specified-violations`
is the per-declaration reader it is built from.(indeterminate-term? kb term ctx)Is term an indeterminate filler in ctx — a member of the extensible
indeterminate_term category (CxCore.txt)? A skolem constant is the built-in first
member, read off its SkolemFn minting expression because a skolem's membership is
never a stored fact; a further kind added with (genl NewKind indeterminate_term) is
picked up through ordinary collection membership.
vaelii.impl.provers/indeterminate-term? is the implementation, so the audit and
the different prover's UNA identity exemption cannot disagree about a term. This
namespace sits above the prover registry, which is what makes the call possible; two
copies agreeing by inspection did diverge, on a membership one reader derived and the
other read as stored.
A non-skolem NAT that is not declared an indeterminate_term, a bare individual and a
literal are all determinate; the blanket non-skolem-NAT determinacy question is punted
(Pace).
Is `term` an **indeterminate** filler in `ctx` — a member of the extensible `indeterminate_term` category (CxCore.txt)? A skolem constant is the built-in first member, read off its `SkolemFn` minting expression because a skolem's membership is never a stored fact; a further kind added with `(genl NewKind indeterminate_term)` is picked up through ordinary collection membership. `vaelii.impl.provers/indeterminate-term?` **is** the implementation, so the audit and the `different` prover's UNA identity exemption cannot disagree about a term. This namespace sits above the prover registry, which is what makes the call possible; two copies agreeing by inspection did diverge, on a membership one reader derived and the other read as stored. A non-skolem NAT that is not declared an `indeterminate_term`, a bare individual and a literal are all determinate; the blanket non-skolem-NAT determinacy question is punted (Pace).
(specified-violations kb pred indep dep ctx)(specified-violations kb pred indep dep ctx arg-pos)The instances of indep that violate the (predAllSpecified pred indep dep) integrity
requirement in ctx: every member x of indep for which no believed (pred x y) has a
determinate filler y in dep. Returns a set of such x (empty when the requirement
holds).
arg-pos selects the twin: :second for predAllSpecified (the audited filler sits at
pred's second position), :first for predSpecifiedAll (the filler sits first and
the quantified instance second). Defaults to :second.
A filler is indeterminate exactly when it is an indeterminate_term — a skolem (the
built-in first member) or an extension declared with (genl NewKind indeterminate_term)
— so an Exists placeholder passes and a skolemised witness does not, which is what
makes this the antagonist of the Exists class.
The instances of `indep` that violate the `(predAllSpecified pred indep dep)` integrity requirement in `ctx`: every member x of `indep` for which no believed `(pred x y)` has a *determinate* filler y in `dep`. Returns a set of such x (empty when the requirement holds). `arg-pos` selects the twin: `:second` for `predAllSpecified` (the audited filler sits at `pred`'s second position), `:first` for `predSpecifiedAll` (the filler sits first and the quantified instance second). Defaults to `:second`. A filler is indeterminate exactly when it is an `indeterminate_term` — a skolem (the built-in first member) or an extension declared with `(genl NewKind indeterminate_term)` — so an *Exists* placeholder passes and a skolemised witness does not, which is what makes this the antagonist of the *Exists* class.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |