Head existentials: the deterministic constant a rule head (exists ?y C) fires to.
A rule head (exists ?y C) (docs/skolem.md) leaves ?y unbound after the antecedent
substitution. Forward firing replaces it with a deterministic skolem constant so the
semi-naive fixpoint terminates: the same (rule, antecedent-binding) must produce the
same constant, or a re-derivation would mint a new one each round and never converge.
The constant is a NAT (SkolemFn <rule-handle> <exist-index> <frontier-values…>) routed
through the ordinary reify path — nat/reify-or-mint-nat dedups it against
termOfUnit, so re-firing on the same binding resolves to the one constant. A single
skolem function reified per-argument (rather than a per-rule function name) means one
lazy reifiableFunction declaration turns the whole mechanism on, and the frontier
values in the arguments key determinism.
A namespace of its own because it has two callers on two layers and belongs to
neither. The write path asks has-existential-head? when a rule is asserted, and
declares the reifiable function then, so a rule that fires during its own assert already
finds it; the forward chainer (vaelii.impl.chain) calls skolemize-conclusion at each
firing. Its own vocabulary is rules and firings — rule handles, frontier variables, a
substituted conclusion — so it is not part of vaelii.impl.nat, which knows about
reified terms and nothing about rules; minting is only how it makes the constant.
The mint itself is a full assert, one layer above this one, reached through
vaelii.impl.wiring — which is where the reason it cannot be a require is written down.
Head existentials: the deterministic constant a rule head `(exists ?y C)` fires to. A rule head `(exists ?y C)` (docs/skolem.md) leaves `?y` unbound after the antecedent substitution. Forward firing replaces it with a *deterministic* skolem constant so the semi-naive fixpoint terminates: the same `(rule, antecedent-binding)` must produce the same constant, or a re-derivation would mint a new one each round and never converge. The constant is a NAT `(SkolemFn <rule-handle> <exist-index> <frontier-values…>)` routed through the ordinary reify path — `nat/reify-or-mint-nat` dedups it against `termOfUnit`, so re-firing on the same binding resolves to the one constant. A single skolem function reified per-argument (rather than a per-rule function name) means one lazy `reifiableFunction` declaration turns the whole mechanism on, and the frontier values in the arguments key determinism. A namespace of its own because it has **two callers on two layers** and belongs to neither. The write path asks `has-existential-head?` when a rule is asserted, and declares the reifiable function then, so a rule that fires during its own assert already finds it; the forward chainer (`vaelii.impl.chain`) calls `skolemize-conclusion` at each firing. Its own vocabulary is rules and firings — rule handles, frontier variables, a substituted conclusion — so it is not part of `vaelii.impl.nat`, which knows about reified terms and nothing about rules; minting is only *how* it makes the constant. The mint itself is a full assert, one layer above this one, reached through `vaelii.impl.wiring` — which is where the reason it cannot be a require is written down.
(ensure-skolem-function kb)Declare SkolemFn a reifiableFunction if it is not already — so skolem NATs reify to
nat/ constants and the NAT orphan-cleanup gate (nat/any-reifiable-functions?) is on
for retraction. Idempotent, and asserted without chaining or settling since it is pure
metadata.
Declare `SkolemFn` a `reifiableFunction` if it is not already — so skolem NATs reify to `nat/` constants and the NAT orphan-cleanup gate (`nat/any-reifiable-functions?`) is on for retraction. Idempotent, and asserted without chaining or settling since it is pure metadata.
(has-existential-head? sentence)Does sentence assert a rule whose consequent is a head existential (exists ?y C)?
Read past any set/*Rule / exceptWhen wrapper.
Does `sentence` assert a rule whose consequent is a head existential `(exists ?y C)`? Read past any `set/*Rule` / `exceptWhen` wrapper.
The one reifiable function every skolem constant is an application of. A NAT
(SkolemFn <rule-handle> <exist-index> <frontier-values…>) reifies to a stable nat/
constant; the rule handle and frontier values in the arguments are what make it a
function of the (rule, binding), so no per-rule function name is needed.
The one reifiable function every skolem constant is an application of. A NAT `(SkolemFn <rule-handle> <exist-index> <frontier-values…>)` reifies to a stable `nat/` constant; the rule handle and frontier values in the arguments are what make it a function of the `(rule, binding)`, so no per-rule function name is needed.
(skolemize-conclusion kb rule raw bindings free)Replace each still-unbound (existential) variable free in a rule's substituted
conclusion raw with its deterministic skolem constant, and return the ground
conclusion.
The skolem for the i-th existential variable (existentials sorted, so i is stable) is
the NAT (SkolemFn <rule-handle> i <frontier-values…>) reified to a nat/ constant.
Because the arguments are a function of the rule and this firing's frontier values, two
firings on the same antecedent binding reify to the same constant
(reify-or-mint-nat dedups via termOfUnit) — which is what lets the fixpoint
converge — and the conjuncts of one head share it, since one rule head is one
rule-handle and one existential index.
Replace each still-unbound (existential) variable `free` in a rule's substituted conclusion `raw` with its deterministic skolem constant, and return the ground conclusion. The skolem for the i-th existential variable (existentials sorted, so `i` is stable) is the NAT `(SkolemFn <rule-handle> i <frontier-values…>)` reified to a `nat/` constant. Because the arguments are a function of the rule and this firing's frontier values, two firings on the same antecedent binding reify to the *same* constant (`reify-or-mint-nat` dedups via `termOfUnit`) — which is what lets the fixpoint converge — and the conjuncts of one head share it, since one rule head is one `rule-handle` and one existential index.
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 |