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, 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`. 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*, 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 |