The lookup-to-query stack: eight levels of escalating interpretive machinery over the same goal, from a raw index read to full backward chaining.
Every layer the engine already has is a point on a ladder — the trie knows
nothing but paths, raw-match adds unification, matches-visible adds context
inheritance, the prover engine adds closures and rules. Naming those points and
giving them one call shape makes the cost of an answer legible: you can ask what
the cheapest machinery that answers a goal is (escalate), or watch an answer
appear as machinery is switched on (explain).
0 :raw handles at an index location — no sentence semantics at all 1 :extent one literal context, narrowed by functor; no unification 2 :local + unification and the symmetric mirror, one literal context 3 :visible + context inheritance (the genlContext up-closure) 4 :typed + predicate inheritance (the genl spec walk) 5 :closed + transitive closure for transitive predicates 6 :solved the whole prover registry — no member of it expands a rule 7 :proved + rule expansion (the recursive chainer, registry as its leaf)
Each level adds exactly one mechanism to the one below it, so a result that appears at level n and not at n-1 is attributable to that mechanism alone.
Monotonicity, and the two joints where it is not free. Levels 3-5 are wider
calls to the same matcher, and level 5 is literally level 4 ∪ the closure, so an
answer reachable at one of them is reachable at the next. Two joints are not like
that, and naming them is half of what naming the levels is for:
1 -> 2 narrows. Level 1 is candidate retrieval and never looks at the goal's
arguments; level 2 unifies. So for any goal that pins an argument level 2 is a
subset of level 1 — which is one of the two reasons escalate floors at 2.
3 -> 4 can drop an answer. Level 4 is res/matches-visible, which reads the
except visibility filter that res/raw-match does not, so a sentex a believed
(except (sentexHandle H)) hides from the view context is matched at levels 2 and
3 and gone from level 4 up. Level 4 is right and the engine agrees — ask denies
that goal too. What it costs is escalate, which will name level 2 as the
machinery sufficient for a goal the engine does not answer. No floor fixes that:
whether a level over-reports is a property of the KB, not of the level.
Level 6 delegates to the real engine (provers/solve-goal-with) and therefore
inherits its behaviour, including the short-circuit where a prover claiming
completeness 100 runs alone: for a genl goal, level 6 returns the taxonomy
closure rather than the union of closure and stored facts, which is why level 6
answers may carry no handle where level 4's did.
What does not bend is the content. Completeness 100 claims a superset of what
every other applicable prover would answer for that goal (provers, the contract at
the head of the file), and a prover bearing on a channel it cannot read reports below
100 for the goal so the union runs. So from level 4 up an answer climbing the stack
can lose its handle and never its existence.
Laziness. Every level returns a lazy seq, and each is lazy as deep as the layer under it allows, so taking one result is strictly cheaper than taking all. Where that is impossible it is inherent, not an oversight, and is noted at the site: reading a stored set is one operation whether you take one member or all of them, and a transitive closure has no partial answer. The property that does hold everywhere is that per-result work — a record fetch, an expensive prover, a rule expansion — is paid per result consumed.
The lookup-to-query stack: eight levels of escalating interpretive machinery over the same goal, from a raw index read to full backward chaining. Every layer the engine already has is a *point on a ladder* — the trie knows nothing but paths, `raw-match` adds unification, `matches-visible` adds context inheritance, the prover engine adds closures and rules. Naming those points and giving them one call shape makes the cost of an answer legible: you can ask what the cheapest machinery that answers a goal is (`escalate`), or watch an answer appear as machinery is switched on (`explain`). 0 :raw handles at an index location — no sentence semantics at all 1 :extent one literal context, narrowed by functor; no unification 2 :local + unification and the symmetric mirror, one literal context 3 :visible + context inheritance (the genlContext up-closure) 4 :typed + predicate inheritance (the genl spec walk) 5 :closed + transitive closure for transitive predicates 6 :solved the whole prover registry — no member of it expands a rule 7 :proved + rule expansion (the recursive chainer, registry as its leaf) Each level adds **exactly one** mechanism to the one below it, so a result that appears at level n and not at n-1 is attributable to that mechanism alone. **Monotonicity, and the two joints where it is not free.** Levels 3-5 are wider calls to the same matcher, and level 5 is literally `level 4 ∪ the closure`, so an answer reachable at one of them is reachable at the next. Two joints are not like that, and naming them is half of what naming the levels is for: 1 -> 2 **narrows**. Level 1 is candidate retrieval and never looks at the goal's arguments; level 2 unifies. So for any goal that pins an argument level 2 is a *subset* of level 1 — which is one of the two reasons `escalate` floors at 2. 3 -> 4 can **drop** an answer. Level 4 is `res/matches-visible`, which reads the `except` visibility filter that `res/raw-match` does not, so a sentex a believed `(except (sentexHandle H))` hides from the view context is matched at levels 2 and 3 and gone from level 4 up. Level 4 is right and the engine agrees — `ask` denies that goal too. What it costs is `escalate`, which will name level 2 as the machinery sufficient for a goal the engine does not answer. No floor fixes that: whether a level over-reports is a property of the KB, not of the level. Level 6 delegates to the real engine (`provers/solve-goal-with`) and therefore inherits its behaviour, including the short-circuit where a prover claiming completeness 100 runs *alone*: for a `genl` goal, level 6 returns the taxonomy closure rather than the union of closure and stored facts, which is why level 6 answers may carry no handle where level 4's did. What does **not** bend is the content. Completeness 100 claims a superset of what every other applicable prover would answer for that goal (`provers`, the contract at the head of the file), and a prover bearing on a channel it cannot read reports below 100 for the goal so the union runs. So from level 4 up an answer climbing the stack can lose its handle and never its existence. **Laziness.** Every level returns a lazy seq, and each is lazy as deep as the layer under it allows, so taking one result is strictly cheaper than taking all. Where that is impossible it is inherent, not an oversight, and is noted at the site: reading a stored set is one operation whether you take one member or all of them, and a transitive closure has no partial answer. The property that does hold everywhere is that per-result work — a record fetch, an expensive prover, a rule expansion — is paid per result consumed.
(escalate kb goal context)(escalate kb goal context floor)Climb the stack from floor (default query-floor, 2) and stop at the first
level that answers goal, returning {:level :name :results :tried}. :results
is the lazy seq from that level, so the climb costs one result per level tried,
not a full answer per level. Nothing answers → :level nil with every level tried.
The default floor skips the two retrieval levels, which can report a hit for a
goal they cannot verify — see query-floor. Pass 0 to include them.
Climb the stack from `floor` (default `query-floor`, 2) and stop at the first
level that answers `goal`, returning {:level :name :results :tried}. `:results`
is the lazy seq from that level, so the climb costs one result per level tried,
not a full answer per level. Nothing answers → :level nil with every level tried.
The default floor skips the two retrieval levels, which can report a hit for a
goal they cannot verify — see `query-floor`. Pass 0 to include them.(explain kb goal context)Run every level over goal and report what each yields: a seq of {:level :name
:count}. A diagnostic — it counts, so it realizes every level fully. The first
level whose count jumps is the mechanism the answer depends on.
Run every level over `goal` and report what each yields: a seq of {:level :name
:count}. A diagnostic — it counts, so it realizes every level fully. The first
level whose count jumps is the mechanism the answer depends on.The stack as data: what each level is called and the one mechanism it adds.
The stack as data: what each level is called and the one mechanism it adds.
(lookup kb level goal context)Answer goal in context using exactly the machinery of level (0-7). A lazy
seq of uniform result maps: {:level :handle :sentence :context :bindings}.
Answer `goal` in `context` using exactly the machinery of `level` (0-7). A lazy
seq of uniform result maps: {:level :handle :sentence :context :bindings}.The first level that answers a goal rather than a question about storage, and
so escalate's default floor.
Levels 0 and 1 are retrieval, not matching: level 1 ignores the goal's arguments
entirely (that is what level 2 adds), and level 0 ignores belief — a defeated
sentex still has a handle in the trie. Either will happily report a hit for a
goal it cannot actually verify: (genl dog thing) gets an answer at level 1 from
some other stored genl fact in the same context. Escalating from 0 would
therefore name the wrong mechanism. Pass an explicit floor of 0 to include them.
A floor is the coarse half of that guard and the only half a constant can supply.
Levels 2 and 3 match against the store without the except visibility filter (see
the ns docstring), so a goal whose only stored answer is excepted is reported here at
level 2 while ask denies it. That depends on the KB rather than on the level, so
no floor rules it out — read explain, where the drop at level 4 is visible.
The first level that answers a *goal* rather than a question about storage, and so `escalate`'s default floor. Levels 0 and 1 are retrieval, not matching: level 1 ignores the goal's arguments entirely (that is what level 2 adds), and level 0 ignores belief — a defeated sentex still has a handle in the trie. Either will happily report a hit for a goal it cannot actually verify: `(genl dog thing)` gets an answer at level 1 from some *other* stored genl fact in the same context. Escalating from 0 would therefore name the wrong mechanism. Pass an explicit floor of 0 to include them. A floor is the coarse half of that guard and the only half a constant can supply. Levels 2 and 3 match against the store without the `except` visibility filter (see the ns docstring), so a goal whose only stored answer is excepted is reported here at level 2 while `ask` denies it. That depends on the KB rather than on the level, so no floor rules it out — read `explain`, where the drop at level 4 is visible.
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 |