The KB glue every relation algebra over vaelii.impl.qcn shares — reading believed
facts into a network, and reading entailments back out as prover solutions.
qcn itself knows nothing about a KB: an algebra is a parameter and a network is a
value. This namespace is the other half of that seam, and it is the same half for
every calculus, so it is written once here rather than three times over. A calculus
bundles what actually differs:
{:name a keyword, naming the cache and the parity oracle
:algebra the qcn relation algebra
:denotation {predicate -> #{base relations}} — base ones are the singletons,
derived ones the wider disjunctions}
Everything else — the reader, the two caches, the four goal shapes, the cost and
completeness declarations — follows from those three. vaelii.impl.space,
vaelii.impl.orientation and vaelii.impl.interval each define an algebra and a
vocabulary and call calculus; a fourth would be the same.
Both polarities are read and both are answered. A believed (not (P a b)) narrows the
pair by the complement of P's denotation, and a goal (not (P a b)) is answered by
refutation — possible ∩ denotation(P) = ∅, where the positive goal needs the
stronger possible ⊆ denotation(P). Both are licensed by the base relations being
jointly exhaustive and pairwise disjoint, which is what makes "not P" a constraint
here rather than an absence of information.
Three caches, and they answer different questions:
:qcn atom, keyed [calculus context]
and stamped with observe/change-clock — so it is read out of the KB once and then
reused until the engine actually mutates something. Building it is one
belief-filtered read per predicate of the calculus per polarity (twenty-eight of them
for RCC-8), and it is asked for constantly: a rule joining a qualitative antecedent
asks per binding, and every settle re-checks entailment-withdrawn? once per firing
of every rule that mentions the calculus. Those are stretches in which nothing
mutates at all, which is exactly what the clock recognises.Beside those, and not a cache at all, the resident atom carries the join baseline:
the network a calculus's forward rules were last re-joined over, which is what lets the
next re-join run over the pairs that moved instead of over every pair the network
entails (join-delta). It deliberately outlives a clock tick — its job is to describe a
moment the clock has moved past — and it is safe to lose, since losing it costs a full
re-join and nothing else.
The KB glue every relation algebra over `vaelii.impl.qcn` shares — reading believed
facts into a network, and reading entailments back out as prover solutions.
`qcn` itself knows nothing about a KB: an algebra is a parameter and a network is a
value. This namespace is the other half of that seam, and it is the *same* half for
every calculus, so it is written once here rather than three times over. A **calculus**
bundles what actually differs:
{:name a keyword, naming the cache and the parity oracle
:algebra the `qcn` relation algebra
:denotation {predicate -> #{base relations}} — base ones are the singletons,
derived ones the wider disjunctions}
Everything else — the reader, the two caches, the four goal shapes, the cost and
completeness declarations — follows from those three. `vaelii.impl.space`,
`vaelii.impl.orientation` and `vaelii.impl.interval` each define an algebra and a
vocabulary and call `calculus`; a fourth would be the same.
Both polarities are read and both are answered. A believed `(not (P a b))` narrows the
pair by the **complement** of P's denotation, and a goal `(not (P a b))` is answered by
**refutation** — `possible ∩ denotation(P) = ∅`, where the positive goal needs the
stronger `possible ⊆ denotation(P)`. Both are licensed by the base relations being
jointly exhaustive and pairwise disjoint, which is what makes "not P" a constraint
here rather than an absence of information.
Three caches, and they answer different questions:
* the **network is resident**, on the KB's own `:qcn` atom, keyed `[calculus context]`
and stamped with `observe/change-clock` — so it is read out of the KB once and then
reused until the engine actually mutates something. Building it is one
belief-filtered read per predicate of the calculus per polarity (twenty-eight of them
for RCC-8), and it is asked for constantly: a rule joining a qualitative antecedent
asks per binding, and every settle re-checks `entailment-withdrawn?` once per firing
of every rule that mentions the calculus. Those are stretches in which nothing
mutates at all, which is exactly what the clock recognises.
* the **path-consistency pass** is memoized on the network *value*, in an atom the
calculus owns. That is sound across queries because the network is derived from the
believed facts: any change to them yields a different map and so a different key.
* the **support-carrying pass** — which stored sentexes an entailed relation rests on —
is memoized separately, on the same network value, so an ordinary query never pays to
propagate support nobody asked for.
Beside those, and not a cache at all, the resident atom carries the **join baseline**:
the network a calculus's forward rules were last re-joined over, which is what lets the
next re-join run over the pairs that moved instead of over every pair the network
entails (`join-delta`). It deliberately outlives a clock tick — its job is to describe a
moment the clock has moved past — and it is safe to lose, since losing it costs a full
re-join and nothing else.(calculus nm algebra denotation)Bundle an algebra and its vocabulary into the value every function here takes.
denotation maps each stored predicate to the set of base relations it denotes, so its
keys are the predicates the prover claims.
Bundle an algebra and its vocabulary into the value every function here takes. `denotation` maps each stored predicate to the set of base relations it denotes, so its keys are the predicates the prover claims.
(calculus-for kb pred)The registered calculus claiming pred, or nil. Predicates belong to exactly one
calculus, so the first hit is the only hit.
The registered calculus claiming `pred`, or nil. Predicates belong to exactly one calculus, so the first hit is the only hit.
(constraint calc net i j)The constraint set on [i j] in net: the identity on the diagonal, the recorded
set, else the universe (unknown).
The constraint set on `[i j]` in `net`: the identity on the diagonal, the recorded set, else the universe (unknown).
(definite calc kb context a b)The single base relation between a and b when path consistency pins it down;
:inconsistent when the network contradicts itself, :unknown when two or more
remain possible.
The single base relation between `a` and `b` when path consistency pins it down; `:inconsistent` when the network contradicts itself, `:unknown` when two or more remain possible.
(inconsistency-culprits calc kb context){:pair [i j] :support #{handle}} for an unsatisfiable network — the pair whose
constraint emptied and the sentexes behind it — or nil when the network is satisfiable.
Which pair is blamed for an inconsistency only composition finds depends on the order
the fixpoint reaches it, so this is a diagnosis rather than a canonical explanation.
The verdict itself does not depend on order; only the blame does. For that reason it is
the ledger's unsatisfiable-pairs — a function of the network alone — that
report-inconsistency! records, and this that a caller asks for on demand.
`{:pair [i j] :support #{handle}}` for an unsatisfiable network — the pair whose
constraint emptied and the sentexes behind it — or nil when the network is satisfiable.
Which pair is blamed for an inconsistency only *composition* finds depends on the order
the fixpoint reaches it, so this is a diagnosis rather than a canonical explanation.
The verdict itself does not depend on order; only the blame does. For that reason it is
the ledger's `unsatisfiable-pairs` — a function of the network alone — that
`report-inconsistency!` records, and this that a caller asks for on demand.(inconsistent? calc kb context)Is the network of calc visible from context unsatisfiable? The question
possible answers only obliquely, by going empty for every pair at once.
Is the network of `calc` visible from `context` unsatisfiable? The question `possible` answers only obliquely, by going empty for every pair at once.
(join-baseline kb calc context)What a re-join is measured against: the handles the network of calc in context was
read out of, and the network they close to. Both are resident reads, so taking one
inside a pinned step costs a map lookup and the handle union.
What a re-join is measured against: the handles the network of `calc` in `context` was read out of, and the network they close to. Both are resident reads, so taking one inside a pinned step costs a map lookup and the handle union.
(join-delta kb calc context){:moved … :baseline …} for calc in context — the pairs that may license a firing
the last re-join did not, and the baseline to hand back to note-joined once this
re-join is done.
:moved is :all — join over everything — whenever the delta cannot be trusted: no
baseline recorded yet, either side unsatisfiable, or a handle gone from the network's
input. Otherwise it is the set of pairs, both directions, whose closed constraint
differs.
`{:moved … :baseline …}` for `calc` in `context` — the pairs that may license a firing
the last re-join did not, and the baseline to hand back to `note-joined` once this
re-join is done.
`:moved` is `:all` — join over everything — whenever the delta cannot be trusted: no
baseline recorded yet, either side unsatisfiable, or a handle gone from the network's
input. Otherwise it is the set of pairs, both directions, whose closed constraint
differs.(network kb calc context)Read every believed relation of calc visible from context into a constraint
network {[a b] → #{base relations}}, both directions stored. Each asserted (P a b)
intersects the (a b) constraint with P's denotation and the (b a) constraint with its
converse; each believed (not (P a b)) intersects them with the complement of that
denotation and of its converse. So several facts about one pair narrow it together,
whatever their polarity — an unrecorded pair stays the full (unknown) set, and a pair
narrowed to nothing is a contradiction tighten reports.
Intersection is commutative and associative, so the network is a function of the
believed facts alone, never of the order they were asserted or read in — negatives
included, since a complement is a fixed function of the denotation. Resident on the
KB between reads (read-network).
context is one reader, and a variable is not one: it reads every context's facts
into a single network, which is a diagnostic view of everything stored rather than
anything anybody can see — two incomparable microtheories compose in it and for no
reader. A goal is therefore never answered off that network; the prover fans over
reader-contexts instead, so "in some context" is the union of what the readers
answer.
Read every believed relation of `calc` visible from `context` into a constraint
network `{[a b] → #{base relations}}`, both directions stored. Each asserted `(P a b)`
intersects the (a b) constraint with P's denotation and the (b a) constraint with its
converse; each believed `(not (P a b))` intersects them with the **complement** of that
denotation and of its converse. So several facts about one pair narrow it together,
whatever their polarity — an unrecorded pair stays the full (unknown) set, and a pair
narrowed to nothing is a contradiction `tighten` reports.
Intersection is commutative and associative, so the network is a function of the
believed facts alone, never of the order they were asserted or read in — negatives
included, since a complement is a fixed function of the denotation. Resident on the
KB between reads (`read-network`).
`context` is one **reader**, and a variable is not one: it reads every context's facts
into a single network, which is a diagnostic view of everything stored rather than
anything anybody can see — two incomparable microtheories compose in it and for no
reader. A goal is therefore never answered off that network; the prover fans over
`reader-contexts` instead, so "in some context" is the union of what the readers
answer.(network-support kb calc context)The asserted support of that network: {[a b] → #{handle}}, the sentexes whose
denotations were intersected into each pair. What qcn/path-consistent-with-support
starts from, and what an entailed relation's support is ultimately unioned out of.
The **asserted** support of that network: `{[a b] → #{handle}}`, the sentexes whose
denotations were intersected into each pair. What `qcn/path-consistent-with-support`
starts from, and what an entailed relation's support is ultimately unioned out of.(nodes net)Every term named by a constraint in net.
Every term named by a constraint in `net`.
(note-joined kb calc context baseline)Record baseline as the network every rule mentioning calc has now been joined over
in context. Only a caller that re-joins all of them may say so — a single rule's
own full join (a rule arriving) does not, or the next delta would claim the others were
covered too.
It shares the KB's resident-cache atom, which is cleared wholesale when it grows past its bound; losing a baseline costs a full re-join and nothing else.
Record `baseline` as the network every rule mentioning `calc` has now been joined over in `context`. Only a caller that re-joins *all* of them may say so — a single rule's own full join (a rule arriving) does not, or the next delta would claim the others were covered too. It shares the KB's resident-cache atom, which is cleared wholesale when it grows past its bound; losing a baseline costs a full re-join and nothing else.
(possible calc kb context a b)The base relations still possible between a and b given everything believed in
context — #{} when the network is inconsistent.
The base relations still possible between `a` and `b` given everything believed in
`context` — `#{}` when the network is inconsistent.(prover calc)The entailment prover for calc, to register with vaelii.core/add-prover.
The entailment prover for `calc`, to register with `vaelii.core/add-prover`.
(prover-for? nm pr)Is pr the prover of the calculus named nm? How a caller asks which calculus a
registered prover speaks for, now that they share one record type.
Is `pr` the prover of the calculus named `nm`? How a caller asks which calculus a registered prover speaks for, now that they share one record type.
(reader-contexts kb calc)Every context worth reading a network of calc at: the contexts holding one of its
facts, and the contexts where two or more of those meet (tax/meet-closure, which a
calculus whose facts all sit in one context closes without reading a closure).
The contexts are read from the store rather than from belief, which over-approximates in the safe direction: a context whose only fact of this calculus is defeated is enumerated, reads an empty network there, and entails nothing.
Resident on the KB's :qcn atom, stamped with the change clock exactly as the
networks it names are. Collecting the fact contexts is a record fetch per stored fact
of the calculus — the same walk as reading one network, and answering the same
question about the same content — so a caller asking per goal would pay the whole
extent per goal. Chaining keeps a per-run memo in front of this and is unaffected;
the prover fanning a variable-context goal has no such run to memoize in, and is
exactly the caller that would.
Every context worth reading a network of `calc` at: the contexts holding one of its facts, and the contexts where two or more of those meet (`tax/meet-closure`, which a calculus whose facts all sit in one context closes without reading a closure). The contexts are read from the store rather than from belief, which over-approximates in the safe direction: a context whose only fact of this calculus is defeated is enumerated, reads an empty network there, and entails nothing. **Resident** on the KB's `:qcn` atom, stamped with the change clock exactly as the networks it names are. Collecting the fact contexts is a record fetch per stored fact of the calculus — the same walk as reading one network, and answering the same question about the same content — so a caller asking per goal would pay the whole extent per goal. Chaining keeps a per-run memo in front of this and is unaffected; the prover fanning a variable-context goal has no such run to memoize in, and is exactly the caller that would.
(registered-calculi kb)The calculi whose prover is registered on kb. Registration is the opt-in: with no
prover, a calculus's facts are ordinary facts, matched and chained as they always were,
and nothing here costs anything.
The calculi whose prover is registered on `kb`. Registration is the opt-in: with no prover, a calculus's facts are ordinary facts, matched and chained as they always were, and nothing here costs anything.
(solve-with-support calc kb goal context)(solve-with-support calc kb goal context pairs)Entailed solutions for goal in context, each paired with the handles it rests on —
a seq of [bindings #{handle}].
solve-goal answers which pairs the network entails; support answers what stored
facts each one rests on. Forward chaining needs both, and needs them together: the
bindings extend the join, and the handles become the conclusion's antecedents, so
retracting any fact behind the entailment withdraws whatever was concluded from it.
A pair whose support is empty is dropped rather than answered with a groundless
justification. That is not a hypothetical: the diagonal of a reflexive denotation
((partOfRegion ?x ?x)) is entailed by the algebra's identity alone, with no stored
fact behind it, and a conclusion drawn from it would rest on the rule and nothing else
while looking as though it rested on the network.
pairs narrows the enumeration to those pairs (solve-goal), which is what a re-join
over a delta passes. It costs nothing here: a pair with no support was never going to
be answered, and a pair whose support is what changed is in the delta by construction.
Entailed solutions for `goal` in `context`, each paired with the handles it rests on —
a seq of `[bindings #{handle}]`.
`solve-goal` answers *which* pairs the network entails; `support` answers what stored
facts each one rests on. Forward chaining needs both, and needs them together: the
bindings extend the join, and the handles become the conclusion's antecedents, so
retracting any fact behind the entailment withdraws whatever was concluded from it.
A pair whose support is empty is dropped rather than answered with a groundless
justification. That is not a hypothetical: the *diagonal* of a reflexive denotation
(`(partOfRegion ?x ?x)`) is entailed by the algebra's identity alone, with no stored
fact behind it, and a conclusion drawn from it would rest on the rule and nothing else
while looking as though it rested on the network.
`pairs` narrows the enumeration to those pairs (`solve-goal`), which is what a re-join
over a delta passes. It costs nothing here: a pair with no support was never going to
be answered, and a pair whose support is what changed is in the delta by construction.(support calc kb context a b)The handles of the stored sentexes the relation between a and b rests on: the
facts a reader intersected into that pair's constraint, plus — transitively — the facts
behind every composition that narrowed it. #{} when the pair is unconstrained (there
is nothing to support "unknown") and when the network is inconsistent (an impossible
theory entails nothing to support).
This is the answer to "why does the network say that?", and it is the piece a
justification would need: an entailed relation has no handle of its own, so a datum
resting on it must rest on these instead. It names one derivation and
over-approximates that one, exactly as a justification names one support list —
see qcn/path-consistent-with-support for both halves of that claim.
The handles of the stored sentexes the relation between `a` and `b` rests on: the
facts a reader intersected into that pair's constraint, plus — transitively — the facts
behind every composition that narrowed it. `#{}` when the pair is unconstrained (there
is nothing to support "unknown") and when the network is inconsistent (an impossible
theory entails nothing to support).
This is the answer to "why does the network say that?", and it is the piece a
justification would need: an entailed relation has no handle of its own, so a datum
resting on it must rest on these instead. It names **one** derivation and
over-approximates *that* one, exactly as a justification names one support list —
see `qcn/path-consistent-with-support` for both halves of that claim.(tighten kb {:keys [algebra pc-cache] :as calc} context net extra)Path consistency over net, memoized on the network value and held resident on the KB
in front of that. An unsatisfiable network is reported through report-inconsistency!
on the way past — the pass has just proved it, and the alternative is a query that
silently answers nothing. A cache hit of either kind does not re-record, so a query
loop reports once and a change of belief reports again.
When the last resident answer was computed for a network this one narrows — which is
what an arriving fact does, and it is the ordinary case during a load — the pass is
warm-started off it and revisits only the triples reading a pair that moved
(qcn/path-consistent-from). Same value, less of the cubic loop. Widening — a
retraction, a defeat — has no such shortcut and pays the whole pass; that is the honest
trade rather than a gap, since a fixpoint cannot be run backwards.
extra is the nodes the goal names and the network may not — qcn/path-consistent
needs every node its triples are drawn from, and the ones the network mentions are read
off it here. Naming only the extras is what keeps a cache hit O(1): collecting a
network's own nodes is a walk over every pair, which at a hundred nodes costs more than
the pass lookup it precedes.
Path consistency over `net`, memoized on the network value and held resident on the KB in front of that. An unsatisfiable network is reported through `report-inconsistency!` on the way past — the pass has just proved it, and the alternative is a query that silently answers nothing. A cache hit of either kind does not re-record, so a query loop reports once and a change of belief reports again. When the last resident answer was computed for a network this one **narrows** — which is what an arriving fact does, and it is the ordinary case during a load — the pass is **warm-started** off it and revisits only the triples reading a pair that moved (`qcn/path-consistent-from`). Same value, less of the cubic loop. Widening — a retraction, a defeat — has no such shortcut and pays the whole pass; that is the honest trade rather than a gap, since a fixpoint cannot be run backwards. `extra` is the nodes the *goal* names and the network may not — `qcn/path-consistent` needs every node its triples are drawn from, and the ones the network mentions are read off it here. Naming only the extras is what keeps a cache hit O(1): collecting a network's own nodes is a walk over every pair, which at a hundred nodes costs more than the pass lookup it precedes.
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 |