vaelii.impl.qcn — com.vaelii/vaelii 0.1.0

Generic qualitative-constraint-network path consistency — the shared substrate every relation algebra reasons through (vaelii.impl.space is RCC-8 topology, vaelii.impl.orientation cardinal direction, vaelii.impl.interval Allen's interval time).

Pure data in, pure data out: nothing here knows about a KB, a context, or belief. Reading stored facts into a network and reading an answer back out is the algebra's job; this namespace only tightens.

A relation algebra is a map:

{:universe the full set of base relations — an unknown constraint :identity the singleton constraint on the diagonal (i,i) :compose (fn [s1 s2] → s) — composition of two relation sets :converse (fn [s] → s) — the converse of a relation set}

A network is {[i j] → #{base relations}}, both directions stored; an unrecorded pair is the universe. So a network is a value, which is what lets a caller memoize an expensive pass on its content.

Sets are the interface and bitmasks are the arithmetic: a network is encoded into a flat array of masks for the duration of a pass and decoded back on the way out, so every caller keeps reasoning in relation sets while the cubic loop reasons in bit-and. See "bitmask relation sets" below.

Path consistency is sound but not in general complete: it tightens every pair to what composition permits, and an emptied constraint proves unsatisfiability, but a path-consistent network can still be globally unsatisfiable outside an algebra's tractable subclass. So a constraint that survives is possible, not satisfiable, and a non-entailment is "not provable", never "provably false".

constraint clj

(constraint net {:keys [universe identity]} i j)

The constraint on [i j] in net under algebra: the identity on the diagonal, the recorded set, else the universe (unknown).

narrowing-of? clj

(narrowing-of? net prior {:keys [universe]})

Is net a pointwise narrowing of prior — is every pair's constraint at most as wide? A pair prior records and net does not is the universe in net, so it is a narrowing only where prior records the universe there too.

This is the precondition of path-consistent-from, and it is the caller's to check because only the caller holds the network the previous answer was computed from.

path-consistent clj

(path-consistent net nodes algebra)

Enforce composition closure over net across nodes: for every triple (i j k), tighten R(i,k) ∩= R(i,j)∘R(j,k), to a fixpoint. Returns the tightened network, or :inconsistent the moment any constraint empties — an empty constraint says two nodes can stand in no relation at all, which no model can satisfy. A constraint that is unsatisfiable as given counts too, whatever the node count and whether or not its nodes were passed: see unsatisfiable-as-given?.

Each constraint set is expected to be a subset of the algebra's universe, which is what a reader produces by construction — it intersects into the universe rather than writing relations of its own.

nodes is what the triples are drawn from, so it is the caller's obligation to pass every node the network mentions — tightening reaches only the nodes it is given, and a node left out is a path composition left unmade. Passing extra nodes is safe: an isolated one constrains nothing, since its every constraint is the universe and the universe composes to itself — which is exactly the condition a jointly-exhaustive algebra meets, and the one every calculus here is built on.

The result does not depend on the order of nodes, nor on the order the triples are visited in. Tightening only ever narrows, and composition is monotone in ⊆, so the loop computes the unique greatest fixpoint below the network it was handed — order decides only how many revisits that takes. The universe is finite and every step strictly narrows something, so it terminates. Both directions are written on every tightening, so constraint never has to consult the converse.

It is that order-independence which lets the loop be an arc queue (PC-2) rather than a re-sweep: one full pass over the triples, then revisits of only those a narrowing could have affected (fixpoint-by-queue). path-consistent-naive is the re-sweeping reference it is proven equal to.

path-consistent-from clj

(path-consistent-from net prior nodes algebra)

path-consistent, warm-started from prior — an answer this function returned for some earlier network of which net is a pointwise narrowing (narrowing-of?).

Returns exactly what path-consistent would for net alone: the closure starts from prior ∩ net and revisits only the triples reading a pair where net is stricter than prior, which is the whole of what a narrowing can have invalidated. See the note above for the fixpoint identity that makes those two the same value.

nodes need name only what neither network mentions — a goal's own terms — since the rest are read off the merged network here. That is not merely a convenience: a warm start is taken exactly when facts have arrived, and an arriving fact routinely names a node neither the previous network nor the caller's list holds. A node left out is a node no triple visits, so its every composition goes unmade and the answer comes back looking merely uninformative rather than wrong.

Handing it a prior that is not an answer for a network net narrows — or one from a different algebra — is a caller error and yields a network tighter than the facts license. narrowing-of? is the guard; there is no cheaper one, since the whole point is not to look at the pairs that did not move.

path-consistent-naive clj

(path-consistent-naive net nodes algebra)

Path consistency by repeated full sweeps: visit all n(n-1)(n-2) triples, and do it again while anything narrowed.

Same arguments and same answer as path-consistent, more work — it is kept as the reference the arc queue is proven against (qcn-queue-test runs both over randomized networks across four algebras and asserts they agree, network for network and verdict for verdict). Two implementations that share their tightening step and differ only in which triples they revisit can agree only by both being right.

path-consistent-with-support clj

(path-consistent-with-support net support nodes algebra)

path-consistent, carrying support alongside the constraints: which stored sentexes an entailed relation rests on.

support is the asserted support, {[i j] → #{handle}} — the sentexes a reader intersected into that pair's constraint. A tightened constraint's support is the union of the supports of the two constraints that composed to narrow it and of its own prior support, so support propagates exactly where a narrowing does.

Returns {:network … :support …}, or, when a constraint empties, {:inconsistent [i j] :culprits #{handle}} — the pair that emptied and the sentexes behind it, which is what a caller wants to know about an impossible network. Which pair is blamed for a derived inconsistency depends on which one the fixpoint empties first, so treat the culprits as a diagnosis rather than as a canonical explanation; the verdict does not depend on that, only the blame does.

Two things the support is not, and both matter to a caller.

It is not minimal. Support accumulates on every narrowing, so a pair narrowed twice keeps the first narrowing's support even where the second subsumed it — an over-approximation of the derivation it names.

It is not every derivation. Support propagates only where a constraint moves, so a second route that re-derives the value a first route already reached contributes nothing: what comes back is a witness, the accumulated one that produced the current value, not the set of all of them. That is deliberate — it is exactly what a justification is (one support list; a datum with two derivations gets two justifications), and unioning across re-derivations would mean iterating the support system to its own fixpoint over every triple, whether or not anybody asked. So retracting the reported set destroys that derivation; where the network has an independent second route the relation survives, and asking again names the survivor.

What is guaranteed: every handle named is a sentex really read into this network, and the reported set is enough to have produced the relation on its own.

unsatisfiable-pairs clj

(unsatisfiable-pairs net {:keys [identity]})

The pairs of net that unsatisfiable-as-given? refuses — what a reader wrote down that no model can satisfy, before any tightening. Empty when the network is unsatisfiable only derivably, by composition, which is the case a report has no single pair to blame for.