The audits of the predAll / predExists / predInstance / predSpecified matrix: the Specified pair's and the Exists four's (docs/predall.md, resources/kb/upper/core.txt).
Reached from outside through vaelii.core/specified-violations,
vaelii.core/exists-violations and vaelii.core/all-specified-violations, which are
thin delegations to the readers here.
The audit reads through vaelii.core/ask's per-context step (quasiquote/ask-prepared),
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 generate real inference and the Exists relations are
records beside a sanctioned placeholder functor, audited for existence alone
(exists-violations), 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.
typeAllSpecified is the counterpart for a classification: type-specified-violations
reports the instances of a collection no member of a classifier is believed to hold,
and kb-integrity folds its declaration stream as its own category (docs/integrity.md).
Indeterminate = the indeterminate_term category. A filler counts as determinate
unless it is a member of the extensible indeterminate_term collection (core.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 not decided: 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 audits of the predAll / predExists / predInstance / predSpecified matrix: the
*Specified* pair's and the *Exists* four's (docs/predall.md, resources/kb/upper/core.txt).
Reached from outside through `vaelii.core/specified-violations`,
`vaelii.core/exists-violations` and `vaelii.core/all-specified-violations`, which are
thin delegations to the readers here.
The audit reads through `vaelii.core/ask`'s per-context step (`quasiquote/ask-prepared`),
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 generate real inference and the *Exists* relations are
records beside a sanctioned placeholder functor, audited for existence alone
(`exists-violations`), `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.
`typeAllSpecified` is the counterpart for a classification: `type-specified-violations`
reports the instances of a collection no member of a classifier is believed to hold,
and `kb-integrity` folds its declaration stream as its own category (docs/integrity.md).
**Indeterminate = the `indeterminate_term` category.** A filler counts as determinate
unless it is a member of the extensible `indeterminate_term` collection (core.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 not decided: 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 visible Specified and Exists declarations as {declaration result …}.
Binary keys are [functor pred indep]; Exists and legacy-ternary keys keep all
arguments. Results are {:status :audited :violations #{…}} or explicit :gap
diagnostics. Omit satisfied declarations, never gaps; an empty map is clean.
Specified audits every eligible defining reader, exempts only proved skeletal-only
instances, and reports incomplete support. No-home/native answers retain the actual
reader. Uses the same declaration stream as kb-integrity; see docs/integrity.md.
Audit visible Specified and Exists declarations as `{declaration result …}`.
Binary keys are `[functor pred indep]`; Exists and legacy-ternary keys keep all
arguments. Results are `{:status :audited :violations #{…}}` or explicit `:gap`
diagnostics. Omit satisfied declarations, never gaps; an empty map is clean.
Specified audits every eligible defining reader, exempts only proved skeletal-only
instances, and reports incomplete support. No-home/native answers retain the actual
reader. Uses the same declaration stream as `kb-integrity`; see docs/integrity.md.(exists-violations kb declaration ctx)Audit one Exists declaration (functor pred a b) in ctx, functor one of
predAllExists, predExistsAll, predExistsInstance and predInstanceExists, and
return {:status :audited :violations #{x …}}: each member of the universal collection,
or the fixed term of a pure existential, with no believed tuple of pred relating it to
a member of the filler collection or to the cell's placeholder for it. Any member
counts, an indeterminate one (a skolem) included, since the declaration asks for
existence only. Throws :bad-args for any other functor.
Audit one *Exists* declaration `(functor pred a b)` in `ctx`, `functor` one of
`predAllExists`, `predExistsAll`, `predExistsInstance` and `predInstanceExists`, and
return `{:status :audited :violations #{x …}}`: each member of the universal collection,
or the fixed term of a pure existential, with no believed tuple of `pred` relating it to
a member of the filler collection or to the cell's placeholder for it. Any member
counts, an indeterminate one (a skolem) included, since the declaration asks for
existence only. Throws `:bad-args` for any other functor.(indeterminate-term? kb term ctx)Is term an indeterminate filler in ctx — a member of the extensible
indeterminate_term category (core.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 not
decided.
Is `term` an **indeterminate** filler in `ctx` — a member of the extensible `indeterminate_term` category (core.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 not decided.
(specified-declaration-audits kb ctx)Every declaration audit as a lazy stream of [declaration result] entries.
A stored Specified declaration audits every known reader seeing that requirement and an ordinary defining home of an instance, each with its own population, contracts and fillers, and the results combine under one canonical key. Native-only registry answers retain the supplied context, since their binding maps carry no defining context.
The open reads are only the unavoidable declaration censuses. Each expensive audit after that is focused on one declared predicate and independent collection. Keeping the units lazy lets the integrity sweep checkpoint and retain progress between them.
Every declaration audit as a lazy stream of `[declaration result]` entries. A stored Specified declaration audits every known reader seeing that requirement and an ordinary defining home of an instance, each with its own population, contracts and fillers, and the results combine under one canonical key. Native-only registry answers retain the supplied context, since their binding maps carry no defining context. The open reads are only the unavoidable declaration censuses. Each expensive audit after that is focused on one declared predicate and independent collection. Keeping the units lazy lets the integrity sweep checkpoint and retain progress between them.
(specified-violations kb pred indep ctx)(specified-violations kb pred indep ctx arg-pos)(specified-violations kb pred indep ctx arg-pos eligible?)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.(type-specified-declaration-audits kb ctx)Every typeAllSpecified declaration visible in ctx, audited, as a lazy stream of
[[typeAllSpecified classifier indep] result] entries in content order.
As for specified-declaration-audits, each stored declaration audits every known reader
seeing it and an instance's ordinary defining home. Each reader supplies its own
population and classifier memberships; cumulative findings share one declaration key.
Native-only declaration answers retain ctx.
Every `typeAllSpecified` declaration visible in `ctx`, audited, as a lazy stream of `[[typeAllSpecified classifier indep] result]` entries in content order. As for `specified-declaration-audits`, each stored declaration audits every known reader seeing it and an instance's ordinary defining home. Each reader supplies its own population and classifier memberships; cumulative findings share one declaration key. Native-only declaration answers retain `ctx`.
(type-specified-violations kb classifier indep ctx)(type-specified-violations kb classifier indep ctx eligible?)Audit (typeAllSpecified classifier indep) in ctx using believed memberships.
Return {:status :audited :violations #{…}}, or :gap for an empty classifier or
incomplete defining support. Ordinary defining-home eligibility exempts only proved
skeletal-only instances; no-home instances remain audited in the actual reader.
The five-argument arm accepts a stored declaration's reader eligibility.
Membership derived by genl or argument preservation counts. See docs/integrity.md.
Audit `(typeAllSpecified classifier indep)` in `ctx` using believed memberships.
Return `{:status :audited :violations #{…}}`, or `:gap` for an empty classifier or
incomplete defining support. Ordinary defining-home eligibility exempts only proved
skeletal-only instances; no-home instances remain audited in the actual reader.
The five-argument arm accepts a stored declaration's reader eligibility.
Membership derived by genl or argument preservation counts. See docs/integrity.md.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 |