CxInference — which readers can answer a goal, and the two ways of working that out.
A variable context reads "in some context", and it reads it per literal: the
join carries the literal's own bindings forward but hands every conjunct the same
wildcard, so two facts no single context sees are joined anyway (docs/contexts.md).
CxInference is that reading made joint — an answer survives only if some one reader's
genlCx cone covers the whole derivation — and the reader that covered it is handed
back as the answer's witness.
Two implementations, because they are worth comparing and must not disagree:
:fan (the reference) enumerates the readers and asks each one the ordinary
scoped question. Sound by construction — every answer is one a real vantage really
gives — and it inherits except, retired-spelling and closure scoping for free,
since each reader runs the same path a named context runs.:post-hoc asks once, unscoped, carrying what each answer rested on, and places
the result with tax/maximal-common-descendant-contexts — the backward twin of what a
forward firing does (vaelii.impl.chain). One pass instead of |readers|.Post-hoc is the one that can be wrong, because an unscoped pass sees a KB with three filters off and has to put them back by reasoning about the placement instead of the read. Each was a real divergence before it was a paragraph:
genl edge it
was matched over does not have the answer (subsumption-support).matches-visible at '?ctx runs where the hidden set is empty by
construction, so an answer can be placed in the very context that excepts one of its
facts (placements).retires-an-ingredient?).And what it cannot do is declared rather than guessed: a computed answer — a closure
walk, an evaluable, an inferred argument type — names no context to place by, so
placeable? asks the registry whether the stored-fact prover is the only one that
applies, and answers hands anything else back to the fan and says so. A narrowing that
does not announce itself reads as a covered case.
The two must return the same answers, witnesses included. query_context_test pins the
cases one at a time; vantage_differential_test compares them over generated lattices,
and each of the five things above turns it red when removed.
`CxInference` — which readers can answer a goal, and the two ways of working that out. A **variable** context reads "in some context", and it reads it *per literal*: the join carries the literal's own bindings forward but hands every conjunct the same wildcard, so two facts no single context sees are joined anyway (docs/contexts.md). `CxInference` is that reading made joint — an answer survives only if some one reader's `genlCx` cone covers the whole derivation — and the reader that covered it is handed back as the answer's **witness**. Two implementations, because they are worth comparing and must not disagree: - **`:fan`** (the reference) enumerates the readers and asks each one the ordinary scoped question. Sound by construction — every answer is one a real vantage really gives — and it inherits `except`, retired-spelling and closure scoping for free, since each reader runs the same path a named context runs. - **`:post-hoc`** asks once, unscoped, carrying what each answer *rested on*, and places the result with `tax/maximal-common-descendant-contexts` — the backward twin of what a forward firing does (`vaelii.impl.chain`). One pass instead of |readers|. Post-hoc is the one that can be wrong, because an unscoped pass sees a KB with three filters off and has to put them back by reasoning about the *placement* instead of the read. Each was a real divergence before it was a paragraph: - **the subsumption edges.** Retrieval is type-aware, so a matched fact is not the only ingredient of its own match — a reader that sees the fact but not the `genl` edge it was matched over does not have the answer (`subsumption-support`). - **the exceptions.** `matches-visible` at `'?ctx` runs where the hidden set is empty by construction, so an answer can be placed in the very context that `except`s one of its facts (`placements`). - **the retired spellings.** Supersession is per reader, so a placement below an equality merge sees both a fact and its twin and retires one spelling an unscoped pass keeps (`retires-an-ingredient?`). And what it cannot do is **declared rather than guessed**: a computed answer — a closure walk, an evaluable, an inferred argument type — names no context to place by, so `placeable?` asks the registry whether the stored-fact prover is the only one that applies, and `answers` hands anything else back to the fan and says so. A narrowing that does not announce itself reads as a covered case. The two must return the same answers, witnesses included. `query_context_test` pins the cases one at a time; `vantage_differential_test` compares them over generated lattices, and each of the five things above turns it red when removed.
How many join rows post-hoc may build per reader before it gives up and lets the fan answer.
The two strategies do not dominate each other and which wins is a fact about the data, not about the lattice, so there is nothing cheap to predict from. Post-hoc reads once and places afterwards, which is far cheaper when the join stays inside contexts that see each other. When it does not — a wide flat lattice whose siblings hold facts about the same individuals, which is an ordinary way to model per-source or per-period knowledge — every cross-sibling pair matches on the join key and dies at placement, so post-hoc does O(readers²) work for O(readers) answers while the fan does O(readers). Fitting a predictor to the lattice's shape got it right five times in fourteen.
What the measurements do say is that post-hoc's edge is on small joins. It loses on large ones two different ways — a wide flat lattice discards most of what it builds, and a deep one discards nothing but still loses, because a quadratic join costs less partitioned across readers than done whole. Only the first is visible as waste, so the meter counts rows built rather than rows discarded: size is the signal both failures share.
So it is measured rather than predicted: the join counts what it builds, and a run that
passes lattice contexts × this has demonstrated the blowup and is abandoned. Wasted
work is bounded by the budget, the fan then answers, and no answer can change — this
is a cost decision in the shape res/*hierarchical-retrieval* already establishes. 20
puts the bail well above what an ordinary join builds and well below the quadratic case.
The lattice rather than readers, because readers costs O(the goal's match set),
and paying that to pick a row count would put the scan back on the one path that never
needs it. A KB whose contexts are all islands has no lattice nodes at all, hence the
floor of one: the budget is a row count for a cost decision, not a claim about the
reader set.
How many join rows post-hoc may build per reader before it gives up and lets the fan answer. The two strategies do not dominate each other and **which wins is a fact about the data, not about the lattice**, so there is nothing cheap to predict from. Post-hoc reads once and places afterwards, which is far cheaper when the join stays inside contexts that see each other. When it does not — a wide flat lattice whose siblings hold facts about the same individuals, which is an ordinary way to model per-source or per-period knowledge — every cross-sibling pair matches on the join key and dies at placement, so post-hoc does O(readers²) work for O(readers) answers while the fan does O(readers). Fitting a predictor to the lattice's shape got it right five times in fourteen. **What the measurements do say is that post-hoc's edge is on *small* joins.** It loses on large ones two different ways — a wide flat lattice discards most of what it builds, and a deep one discards nothing but still loses, because a quadratic join costs less partitioned across readers than done whole. Only the first is visible as waste, so the meter counts rows built rather than rows discarded: size is the signal both failures share. So it is measured rather than predicted: the join counts what it builds, and a run that passes `lattice contexts × this` has demonstrated the blowup and is abandoned. Wasted work is bounded by the budget, the fan then answers, and **no answer can change** — this is a cost decision in the shape `res/*hierarchical-retrieval*` already establishes. 20 puts the bail well above what an ordinary join builds and well below the quadratic case. The **lattice** rather than `readers`, because `readers` costs O(the goal's match set), and paying that to pick a row count would put the scan back on the one path that never needs it. A KB whose contexts are all islands has no lattice nodes at all, hence the floor of one: the budget is a row count for a cost decision, not a claim about the reader set.
Which implementation answers a CxInference read: :fan (the reference) or
:post-hoc.
A pure cost decision that must not change the answer set, in the shape
res/*hierarchical-retrieval* already establishes for retrieval — so it is a var to
rebind in a benchmark or a differential test, not an option on the read doors. Outside
post-hoc's declared domain the fan answers whatever this says.
:post-hoc by default, because it is bounded rather than because it is faster. On
its own it is the riskier of the two: it wins by many multiples where the join stays
inside contexts that see each other, and loses by several where it does not. bail
removes the tail — a run that outgrows its budget is abandoned and the fan answers — so
what is left is a strategy that wins 1.5x to 17x in its regime and costs at most about
1.5x outside it, the extra being the bounded probe. On a store large enough that every
join outgrows the budget, this is the fan, reached after a probe of lattice contexts × 20 rows.
Which implementation answers a `CxInference` read: `:fan` (the reference) or `:post-hoc`. A pure cost decision that **must not change the answer set**, in the shape `res/*hierarchical-retrieval*` already establishes for retrieval — so it is a var to rebind in a benchmark or a differential test, not an option on the read doors. Outside post-hoc's declared domain the fan answers whatever this says. **`:post-hoc` by default, because it is bounded rather than because it is faster.** On its own it is the riskier of the two: it wins by many multiples where the join stays inside contexts that see each other, and loses by several where it does not. `bail` removes the tail — a run that outgrows its budget is abandoned and the fan answers — so what is left is a strategy that wins 1.5x to 17x in its regime and costs at most about 1.5x outside it, the extra being the bounded probe. On a store large enough that every join outgrows the budget, this *is* the fan, reached after a probe of `lattice contexts × 20` rows.
(answers kb goals run-at {:keys [expands-rules? witness prepared-at]})goals answered as CxInference reads them: one binding map per answer per maximal
witness, the witness bound to ?ctx.
run-at answers the goal from one named context, and is what the fan calls per reader.
:expands-rules? says a rule may be expanded under this read, which puts it outside
post-hoc's domain whatever the literals look like — an antecedent fact is not one of
goals, so its context never reaches the placement.
Returns {:answers [...] :strategy :fan|:post-hoc}; the strategy is reported rather
than assumed because it may not be the one *strategy* asked for.
`goals` answered as `CxInference` reads them: one binding map per answer per maximal
witness, the witness bound to `?ctx`.
`run-at` answers the goal from one named context, and is what the fan calls per reader.
`:expands-rules?` says a rule may be expanded under this read, which puts it outside
post-hoc's domain whatever the literals look like — an antecedent fact is not one of
`goals`, so its context never reaches the placement.
Returns `{:answers [...] :strategy :fan|:post-hoc}`; the strategy is reported rather
than assumed because it may not be the one `*strategy*` asked for.(fan kb goals witness run-at)Ask every reader the ordinary scoped question, and keep what a reader really answered.
run-at is the read itself, as a function of the context to run it in — the seam that
keeps this namespace out of vaelii.core's way, and that lets one implementation serve
query, prove, ask and sentexes-matching alike.
Ask every reader the ordinary scoped question, and keep what a reader really answered. `run-at` is the read itself, as a function of the context to run it in — the seam that keeps this namespace out of `vaelii.core`'s way, and that lets one implementation serve `query`, `prove`, `ask` and `sentexes-matching` alike.
(fan-distinct kb goals run-at)The fan for a read that answers with records rather than bindings —
sentexes-matching, whose maps already carry the :context a binding needs a witness
for.
So there is no witness to attach and nothing to place: a single sentence has no
derivation to hold together, and the joint reading only bites where a join does. What
the fan still contributes is the per-reader filtering a wildcard skips — a sentex
excepted from every context that can see it is hidden here and visible at '?ctx,
which is the difference between asking the KB and asking a vantage.
The fan for a read that answers with **records** rather than bindings — `sentexes-matching`, whose maps already carry the `:context` a binding needs a witness for. So there is no witness to attach and nothing to place: a single sentence has no derivation to hold together, and the joint reading only bites where a join does. What the fan still contributes is the per-reader filtering a wildcard skips — a sentex `except`ed from every context that can see it is hidden here and visible at `'?ctx`, which is the difference between asking the KB and asking a vantage.
(placeable? kb goals)Is goals inside post-hoc's domain — is every literal one that only the stored-fact
prover answers?
Post-hoc places an answer by the contexts of what it rested on, so it can only answer
where everything it rests on has a context. A stored match does: it names a sentex,
and the genl edges it subsumed through name supporters. A computed answer does not — a
closure walk two hops long, an evaluable, an inferred argument type — and there is no
honest context to place it by. Guessing one would place an answer where the edges it
rests on are not visible, which is the failure this whole namespace exists to avoid.
Asked of the registry rather than of the literal's shape, because the shape does not
say: (gp0 ?a ?b) and (genl aa_t ?x) are the same shape and only the second walks a
closure. provers/applicable-provers is what the dispatch itself asks, so the domain
cannot drift from what actually runs. A deferred literal is excluded by the same test
— its prover is not the fact prover — and cheaply, since applicable? is designed to be
the cheap question.
This is the gate at the door, and it is not the whole of it: applicable? gates on
groundness, so a literal can leave the domain once a join binds it. fact-only? is
re-asked of each substituted literal for that reason, and the join abandons where the
answer changes.
Is `goals` inside post-hoc's domain — is every literal one that **only the stored-fact prover** answers? Post-hoc places an answer by the contexts of what it rested on, so it can only answer where everything it rests on *has* a context. A stored match does: it names a sentex, and the `genl` edges it subsumed through name supporters. A computed answer does not — a closure walk two hops long, an evaluable, an inferred argument type — and there is no honest context to place it by. Guessing one would place an answer where the edges it rests on are not visible, which is the failure this whole namespace exists to avoid. Asked of the **registry** rather than of the literal's shape, because the shape does not say: `(gp0 ?a ?b)` and `(genl aa_t ?x)` are the same shape and only the second walks a closure. `provers/applicable-provers` is what the dispatch itself asks, so the domain cannot drift from what actually runs. A `deferred` literal is excluded by the same test — its prover is not the fact prover — and cheaply, since `applicable?` is designed to be the cheap question. This is the gate at the **door**, and it is not the whole of it: `applicable?` gates on groundness, so a literal can leave the domain once a join binds it. `fact-only?` is re-asked of each substituted literal for that reason, and the join abandons where the answer changes.
(post-hoc kb goals witness budget prepared-at)Answer unscoped, then keep only what some reader could have seen whole.
The placement is tax/maximal-common-descendant-contexts of the contexts the answer's
own facts came from — empty when they have no common view, which is exactly the case
the unscoped default answers and should not.
Bindings are projected onto the goal's own variables first, and that is not cosmetic.
Matching runs at '?ctx, and match-one unifies the context slot too, so every raw
binding carries a ?ctx naming the context its match came from. Left in, two derivations
of one binding — a fact and the twin an equality merge migrated below it — are two
different keys, they never group, and each keeps a witness the other would have collapsed.
query projects for its own reasons and the fan inherits it; post-hoc has to do it
deliberately.
Answer unscoped, then keep only what some reader could have seen whole. The placement is `tax/maximal-common-descendant-contexts` of the contexts the answer's own facts came from — empty when they have no common view, which is exactly the case the unscoped default answers and should not. **Bindings are projected onto the goal's own variables first**, and that is not cosmetic. Matching runs at `'?ctx`, and `match-one` unifies the *context slot* too, so every raw binding carries a `?ctx` naming the context its match came from. Left in, two derivations of one binding — a fact and the twin an equality merge migrated below it — are two different keys, they never group, and each keeps a witness the other would have collapsed. `query` projects for its own reasons and the fan inherits it; post-hoc has to do it deliberately.
(readers kb goals)Every context that could be the vantage a CxInference answer is witnessed by: the
genlCx lattice, plus any context outside it holding a fact the goal could match.
The closure runs only when the seed adds something. meet-closure is O(pairs), each pair
a maximal-common-descendant-contexts, and over the lattice's own nodes it cannot add a
member: a common descendant is drawn from the context-down closures, so it is a node
already. Running it anyway cost more than a whole post-hoc read on a 24-context KB, to
return the set it was handed.
Every context that could be the vantage a `CxInference` answer is witnessed by: the `genlCx` lattice, plus any context outside it holding a fact the goal could match. The closure runs only when the seed adds something. `meet-closure` is O(pairs), each pair a `maximal-common-descendant-contexts`, and over the lattice's own nodes it cannot add a member: a common descendant is drawn from the `context-down` closures, so it is a node already. Running it anyway cost more than a whole post-hoc read on a 24-context KB, to return the set it was handed.
Where a CxInference answer reports the reader that witnessed it: the keyword
:context, beside the bindings rather than among them.
A binding is what a variable the caller wrote gets bound to, and CxInference is a
constant — the caller named no variable, so there is nothing to bind and inventing one
would be this namespace answering a question nobody asked. Earlier it assoc'd ?ctx,
which read like a binding and was not one: no ?ctx appeared in the call. A keyword
cannot collide with a binding either, since those are keyed by the ?-symbols the goal
spells.
Pass a variable context instead and the witness really is a binding — it unifies into that variable, under whatever name the caller chose.
Where a `CxInference` answer reports the reader that witnessed it: the keyword `:context`, **beside** the bindings rather than among them. A binding is what a *variable* the caller wrote gets bound to, and `CxInference` is a constant — the caller named no variable, so there is nothing to bind and inventing one would be this namespace answering a question nobody asked. Earlier it assoc'd `?ctx`, which read like a binding and was not one: no `?ctx` appeared in the call. A keyword cannot collide with a binding either, since those are keyed by the `?`-symbols the goal spells. Pass a **variable** context instead and the witness really is a binding — it unifies into that variable, under whatever name the caller chose.
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 |