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, which are thin delegations to the readers here.
The audit reads through the prover registry below (provers/ask) with each goal prepared
exactly as the public read prepares it (quasiquote/prepare-goal-for-read), so this
namespace sits below vaelii.core and vaelii.core requires it — no layering
inversion. The audit still answers what a user's ask answers: it passes only concrete
contexts and expands no rule, and the genlCx ancestor scoping is applied in the matching
layer below (docs/namespaces.md, "The layering").
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, contract-satisfying filler, the reader here reports the instances
with no admissible one — {:status :audited :violations #{…}} — or an explicit
{:status :gap …} declaration-contract diagnostic. 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`, which are thin delegations to the readers here.
The audit reads through the prover registry below (`provers/ask`) with each goal prepared
exactly as the public read prepares it (`quasiquote/prepare-goal-for-read`), so this
namespace sits **below** `vaelii.core` and `vaelii.core` requires it — no layering
inversion. The audit still answers what a user's `ask` answers: it passes only concrete
contexts and expands no rule, and the `genlCx` ancestor scoping is applied in the matching
layer below (docs/namespaces.md, "The layering").
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*, contract-satisfying filler, the reader here reports the instances
with no admissible one — `{:status :audited :violations #{…}}` — or an explicit
`{:status :gap …}` declaration-contract diagnostic. 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 {[functor pred indep] result …} — each result carrying a :status:
{:status :audited :violations #{…}} where the audit ran, or {:status :gap …}
for a declaration-contract diagnostic. Two gap kinds ship: :missing-slot-typing
(the predicate carries no visible slot typing at the audited position) and
:legacy-ternary-declaration (a stored pre-migration ternary sentex, reachable
through the bulk import path, which the binary audit cannot read). A legacy gap
is keyed by its whole stale argument tuple, [functor pred a b], so it collides
with neither a three-element binary key nor another stale sentex over the same
predicate: an unmigrated KB carries both spellings at once, and a key off the
first two arguments alone let the stale one replace the migrated declaration's
violation set. Declarations that hold are omitted; a gap never is, so a clean
sweep is an empty map and a gap cannot pass as one. 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 `{[functor pred indep] result …}` — each result carrying a `:status`:
`{:status :audited :violations #{…}}` where the audit ran, or `{:status :gap …}`
for a declaration-contract diagnostic. Two gap kinds ship: `:missing-slot-typing`
(the predicate carries no visible slot typing at the audited position) and
`:legacy-ternary-declaration` (a stored pre-migration ternary sentex, reachable
through the bulk import path, which the binary audit cannot read). A legacy gap
is keyed by its whole stale argument tuple, `[functor pred a b]`, so it collides
with neither a three-element binary key nor another stale sentex over the same
predicate: an unmigrated KB carries both spellings at once, and a key off the
first two arguments alone let the stale one replace the migrated declaration's
violation set. Declarations that hold are omitted; a gap never is, so a clean
sweep is an empty map and a gap cannot pass as one. 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 ctx)(specified-violations kb pred indep ctx arg-pos)Audit one binary (predAllSpecified pred indep) declaration in ctx and return a
result map that always carries a :status — {:status :audited :violations #{x …}}
where the audit ran (empty set = the requirement holds), or
{:status :gap :gap :missing-slot-typing :pred pred :position n} where pred
carries no visible denotation-typing at the audited position, a declaration-contract
gap reported explicitly rather than silently audited unconstrained. Discriminate on
:status: a gap result carries no :violations key on purpose (no violation set
pretends the audit ran), so a bare (:violations r) read nil-puns a gap into a
clean pass.
The required filler type is derived from pred's own argument contract, never
restated in the declaration: every visible (arg pred n t) requires the filler to be
a member of t, every visible (genlArg pred n t) requires it to be a subtype of
t, and multiple constraints compose conjunctively, as the assert-time checker
composes them.
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.
Audit one binary `(predAllSpecified pred indep)` declaration in `ctx` and return a
result map that always carries a `:status` — `{:status :audited :violations #{x …}}`
where the audit ran (empty set = the requirement holds), or
`{:status :gap :gap :missing-slot-typing :pred pred :position n}` where `pred`
carries no visible denotation-typing at the audited position, a declaration-contract
gap reported explicitly rather than silently audited unconstrained. Discriminate on
`:status`: a gap result carries no `:violations` key on purpose (no violation set
pretends the audit ran), so a bare `(:violations r)` read nil-puns a gap into a
clean pass.
The required filler type is **derived from `pred`'s own argument contract**, never
restated in the declaration: every visible `(arg pred n t)` requires the filler to be
a member of `t`, every visible `(genlArg pred n t)` requires it to be a subtype of
`t`, and multiple constraints compose conjunctively, as the assert-time checker
composes them.
`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 |