Canonical variable names for a solution cache keyed by a literal, and the translation back into the caller's names.
A backward proof asks the same question many times. Two sibling branches that both
need (parentOf Tom ?y) each solve it in full, and a diamond-shaped rule set pays for
the shared literal once per path through the diamond — the per-path :seen guards in
res/prove-from's per-path guard stops a goal from re-expanding itself on one
path, and say nothing about the same goal being re-solved on another. Keying an
answer by the literal is what collects that sharing, and the key has to be blind to
what the caller happened to name its variables: (P ?x) and (P ?y) are one question.
Why res/goal-key is not that key. It collapses every variable to ?, so
(P ?x ?x) and (P ?x ?y) share a key. That is sound for a loop guard, which only
has to be conservative — over-matching prunes a branch that was going to be pruned —
and unsound for a solution cache, where the second goal's answers include the pairs
the first excludes. Serving one for the other invents solutions. So the renaming
here is repetition-preserving: distinct variables get distinct names and a
repeated variable keeps its repetition.
Why sentex/alpha-rename is not it either. That one builds an index key, where
a variable means "anything in this position" and each anonymous _ is therefore
fresh and unshared. unify does not read _ that way — variable? admits it and
unify-var chases its binding, so (P _ _) fails against (P A B) exactly as
(P ?x ?x) does. A cache keyed on retrieval semantics would hand (P _ _) the
answers of (P ?0 ?1), so _ is renamed here as the ordinary variable it is.
What is cached, and why there. The unit is one literal's visible matches
(res/matches-visible), not one literal's solutions (provers/solve-goal). That
is where the repetition measurably is — a rule-heavy query re-asks a handful of
metadata literals ((argIsa P n ?t), read per believed sentex per argument position
by provers/inferred-types) hundreds of times, while its rule subgoals arrive
already substituted and so are mostly distinct. It is also the only layer at which
the answer is a function of the KB alone. solve-goal is tier-dependent, because
ask-capped drops provers above a cost tier, and scope-dependent, because provers
underneath it read the taxonomy closures and the resident networks through
observe/cached — so inside a pinned scope they answer from the view that scope froze.
An answer cached at that layer would therefore have to carry the tier and the scope
that produced it. matches-visible carries neither and reads nothing through
observe/cached, so a pinned scope cannot hand it a view the clock has left.
There is one layer, not two. A per-query memo would be redundant: a query performs no mutation, so the change clock cannot move while one runs, and every repeat a per-query memo would catch is a repeat this cache already serves under an unmoved stamp.
Canonical variable names for a **solution** cache keyed by a literal, and the translation back into the caller's names. A backward proof asks the same question many times. Two sibling branches that both need `(parentOf Tom ?y)` each solve it in full, and a diamond-shaped rule set pays for the shared literal once per path through the diamond — the per-path `:seen` guards in `res/prove-from`'s per-path guard stops a goal from re-*expanding* itself on one path, and say nothing about the same goal being re-*solved* on another. Keying an answer by the literal is what collects that sharing, and the key has to be blind to what the caller happened to name its variables: `(P ?x)` and `(P ?y)` are one question. **Why `res/goal-key` is not that key.** It collapses *every* variable to `?`, so `(P ?x ?x)` and `(P ?x ?y)` share a key. That is sound for a loop guard, which only has to be conservative — over-matching prunes a branch that was going to be pruned — and unsound for a solution cache, where the second goal's answers include the pairs the first excludes. Serving one for the other invents solutions. So the renaming here is **repetition-preserving**: distinct variables get distinct names and a repeated variable keeps its repetition. **Why `sentex/alpha-rename` is not it either.** That one builds an *index* key, where a variable means "anything in this position" and each anonymous `_` is therefore fresh and unshared. `unify` does not read `_` that way — `variable?` admits it and `unify-var` chases its binding, so `(P _ _)` fails against `(P A B)` exactly as `(P ?x ?x)` does. A cache keyed on retrieval semantics would hand `(P _ _)` the answers of `(P ?0 ?1)`, so `_` is renamed here as the ordinary variable it is. **What is cached, and why there.** The unit is one literal's *visible matches* (`res/matches-visible`), not one literal's *solutions* (`provers/solve-goal`). That is where the repetition measurably is — a rule-heavy query re-asks a handful of metadata literals (`(argIsa P n ?t)`, read per believed sentex per argument position by `provers/inferred-types`) hundreds of times, while its rule subgoals arrive already substituted and so are mostly distinct. It is also the only layer at which the answer is a function of the KB alone. `solve-goal` is **tier**-dependent, because `ask-capped` drops provers above a cost tier, and **scope**-dependent, because provers underneath it read the taxonomy closures and the resident networks through `observe/cached` — so inside a pinned scope they answer from the view that scope froze. An answer cached at that layer would therefore have to carry the tier and the scope that produced it. `matches-visible` carries neither and reads nothing through `observe/cached`, so a pinned scope cannot hand it a view the clock has left. There is **one layer, not two**. A per-query memo would be redundant: a query performs no mutation, so the change clock cannot move while one runs, and every repeat a per-query memo would catch is a repeat this cache already serves under an unmoved stamp.
Whether a cached lookup is consulted at all. Bound false, matches-visible is
byte-for-byte the uncached path — no key built, no atom read, nothing allocated —
which is what makes the off state genuinely free rather than merely cheap.
A toggle that changes cost and not results, in the spirit of plan/*enabled*.
Whether a cached lookup is consulted at all. Bound false, `matches-visible` is byte-for-byte the uncached path — no key built, no atom read, nothing allocated — which is what makes the off state genuinely free rather than merely cheap. A toggle that changes cost and not results, in the spirit of `plan/*enabled*`.
(canonicalize form)[canonical rename] for form: its variables renamed to ?0 ?1 … in
first-occurrence order, and the map from each canonical name back to the caller's.
First occurrence, not sorted — the order is a function of the literal's own shape, so
two spellings of one question converge without either of them being consulted about
the other. Shape is preserved (a vector stays a vector), as sentex/alpha-rename
preserves it and for the same reason: a conjunction is a vector and a literal a list.
rename is empty for a ground literal, which is the common post-substitution case —
and one this returns unchanged, without rebuilding it. That fast path is not a
micro-optimization: canonicalizing sits in front of every cached lookup, so it is
charged to the calls that hit as much as to the ones that miss, and rebuilding a
ground literal to discover it had nothing to rename is the whole cost of the lookup it
was meant to save. A java.util.HashMap for the scratch numbering, for the same
reason — the map is thrown away at the end of the call and never escapes.
`[canonical rename]` for `form`: its variables renamed to `?0 ?1 …` in first-occurrence order, and the map from each canonical name back to the caller's. First occurrence, not sorted — the order is a function of the literal's own shape, so two spellings of one question converge without either of them being consulted about the other. Shape is preserved (a vector stays a vector), as `sentex/alpha-rename` preserves it and for the same reason: a conjunction is a vector and a literal a list. `rename` is empty for a ground literal, which is the common post-substitution case — and one this returns **unchanged**, without rebuilding it. That fast path is not a micro-optimization: canonicalizing sits in front of every cached lookup, so it is charged to the calls that *hit* as much as to the ones that miss, and rebuilding a ground literal to discover it had nothing to rename is the whole cost of the lookup it was meant to save. A `java.util.HashMap` for the scratch numbering, for the same reason — the map is thrown away at the end of the call and never escapes.
(clear-cache kb)Drop everything kb has cached, and reset the counters. Not !: it destroys no
knowledge — every entry is derived, and the next read recomputes it.
Drop everything `kb` has cached, and reset the counters. Not `!`: it destroys no knowledge — every entry is derived, and the next read recomputes it.
(lookup cache k compute)The cached value of k in the per-KB cache atom, or compute's answer on the way
into it. A nil cache computes every time.
The stamp is read before compute runs, and the entry is stored only if the clock
has not moved by the time it is complete. Both halves matter. Stamping afterwards
would claim the value describes a state it was never computed from; storing across a
moved clock would keep a value the mutation invalidated. Together they mean a stored
entry describes exactly the state its stamp names — and that a scope which writes
while it reads (forward chaining, chain/process-datum) fills the cache with
nothing, since its own conclusions move the clock under it. A backward query moves
the clock never, so it stores everything it completes.
The correctness argument is observe/note-change's, unrestated: any mutation moves
the clock, so a hit is served only across a stretch in which the engine performed no
mutation at all — which is the stretch a query spends reading.
The cached value of `k` in the per-KB `cache` atom, or `compute`'s answer on the way into it. A nil `cache` computes every time. **The stamp is read before `compute` runs, and the entry is stored only if the clock has not moved by the time it is complete.** Both halves matter. Stamping afterwards would claim the value describes a state it was never computed from; storing across a moved clock would keep a value the mutation invalidated. Together they mean a stored entry describes exactly the state its stamp names — and that a scope which *writes while it reads* (forward chaining, `chain/process-datum`) fills the cache with nothing, since its own conclusions move the clock under it. A backward query moves the clock never, so it stores everything it completes. The correctness argument is `observe/note-change`'s, unrestated: any mutation moves the clock, so a hit is served only across a stretch in which the engine performed no mutation at all — which is the stretch a query spends reading.
(rename-bindings rename bindings)A canonical-space solution binding map translated back into the caller's variable
names. Identity when rename is empty (a ground literal).
Values as well as keys. A solution can bind one goal variable to another — a
literal whose two variables unify carries ?1 in the value slot — so a rename that
touched only the keys would let a ?0 escape into an answer. Nothing downstream
ever sees a canonical name.
A canonical-space solution binding map translated back into the caller's variable names. Identity when `rename` is empty (a ground literal). **Values as well as keys.** A solution can bind one goal variable to another — a literal whose two variables unify carries `?1` in the value slot — so a rename that touched only the keys would let a `?0` escape into an answer. Nothing downstream ever sees a canonical name.
(rename-matches rename ms)A seq of matches-visible results translated out of canonical space. A result is
[handle bindings …] — some carry a third slot — so only slot 1 is touched and the
rest is passed through. Lazy: a consumer taking one match renames one.
A seq of `matches-visible` results translated out of canonical space. A result is `[handle bindings …]` — some carry a third slot — so only slot 1 is touched and the rest is passed through. Lazy: a consumer taking one match renames one.
(stats kb){:size :hits :misses :clock} — entries held for kb, the hit/miss counters (global,
across every KB, since they measure the mechanism rather than a store), and the change
clock a fresh lookup would stamp with.
`{:size :hits :misses :clock}` — entries held for `kb`, the hit/miss counters (global,
across every KB, since they measure the mechanism rather than a store), and the change
clock a fresh lookup would stamp with.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 |