A simple temporal problem — the metric half of time, where the qualitative calculi say only which of two things came first. A constraint is a bound on the gap between two instants,
lo ≤ t(Q) − t(P) ≤ hi
and a set of them is closed by all-pairs shortest paths over the distance graph they describe. The closure answers the tightest gap the constraints entail between any two instants, including pairs nobody wrote a constraint for, and a negative cycle in that graph is the proof that no assignment of times satisfies them all.
This is not a relation algebra and it is deliberately not forced through
vaelii.impl.qcn: there is no finite set of jointly-exhaustive base relations here, and
no composition table — the constraint on a pair is an interval of the reals, composition
is addition and tightening is min. So it is its own small algorithm, written the way
qcn is written: pure data in, pure data out, knowing nothing about a KB, with the
KB reading and the prover in their own marked section below.
Constraints are measures, not bare numbers. A stated one is the ordinary fact
(temporalDistance P Q M) where M is a (QuantityFn N Unit) for an exact separation or
a (QuantityIntervalFn Lo Hi Unit) for a bounded one, and a negative magnitude says Q
falls before P. Every magnitude normalizes through provers/normalize-quantity against
the KB's dimensionOf / conversionFactor table, so the arithmetic happens in the
dimension's base unit and an answer is rendered back in that same unit — exactly the
contract vaelii.impl.duration follows, so a separation and a duration are written the
same way and compare directly. Constraints spanning more than one dimension are refused
rather than mixed.
Bind or check, like EvaluateProver and the duration arithmetic: an open measure is
bound to the tightest separation entailed, and a ground one is entailed exactly when the
derived bound is contained in it — a stated bound is a weaker claim than the derived one,
so the derived one implies it.
The bridge to the interval algebra is (startOf I P) / (endOf I P), which name an
interval's two bounding instants. With them a metric fact and an Allen relation are about
the same thing, and allen-narrowing reads the closure back as constraints on the
interval relations: if the closure puts A's end strictly before B's start then A is
before B, and so on for all thirteen. It narrows and never widens — it returns relation
sets for a caller to intersect into an interval network, and mutates nothing.
vaelii.impl.duration is the other consumer: overlap-window bounds how long two
intervals overlap from their endpoints alone, which is what turns an indefinite overlap
into a real figure.
The prover is opt-in: register it with vaelii.core/add-prover, and until then a KB
stores and retrieves temporalDistance facts as ordinary facts without paying for the
closure. The vocabulary ships in kb/upper/TimeContext.txt either way. See
docs/stp.md.
A **simple temporal problem** — the metric half of time, where the qualitative calculi say only which of two things came first. A constraint is a bound on the *gap* between two instants, lo ≤ t(Q) − t(P) ≤ hi and a set of them is closed by all-pairs shortest paths over the distance graph they describe. The closure answers the tightest gap the constraints entail between *any* two instants, including pairs nobody wrote a constraint for, and a **negative cycle** in that graph is the proof that no assignment of times satisfies them all. This is not a relation algebra and it is deliberately not forced through `vaelii.impl.qcn`: there is no finite set of jointly-exhaustive base relations here, and no composition table — the constraint on a pair is an interval of the reals, composition is addition and tightening is `min`. So it is its own small algorithm, written the way `qcn` is written: **pure data in, pure data out**, knowing nothing about a KB, with the KB reading and the prover in their own marked section below. **Constraints are measures**, not bare numbers. A stated one is the ordinary fact `(temporalDistance P Q M)` where `M` is a `(QuantityFn N Unit)` for an exact separation or a `(QuantityIntervalFn Lo Hi Unit)` for a bounded one, and a negative magnitude says Q falls before P. Every magnitude normalizes through `provers/normalize-quantity` against the KB's `dimensionOf` / `conversionFactor` table, so the arithmetic happens in the dimension's base unit and an answer is rendered back in that same unit — exactly the contract `vaelii.impl.duration` follows, so a separation and a duration are written the same way and compare directly. Constraints spanning more than one dimension are refused rather than mixed. **Bind or check**, like `EvaluateProver` and the duration arithmetic: an open measure is bound to the tightest separation entailed, and a ground one is *entailed* exactly when the derived bound is contained in it — a stated bound is a weaker claim than the derived one, so the derived one implies it. **The bridge to the interval algebra** is `(startOf I P)` / `(endOf I P)`, which name an interval's two bounding instants. With them a metric fact and an Allen relation are about the same thing, and `allen-narrowing` reads the closure back as constraints on the *interval* relations: if the closure puts A's end strictly before B's start then A is `before` B, and so on for all thirteen. It narrows and never widens — it returns relation sets for a caller to intersect into an interval network, and mutates nothing. `vaelii.impl.duration` is the other consumer: `overlap-window` bounds how long two intervals overlap from their endpoints alone, which is what turns an indefinite overlap into a real figure. The prover is **opt-in**: register it with `vaelii.core/add-prover`, and until then a KB stores and retrieves `temporalDistance` facts as ordinary facts without paying for the closure. The vocabulary ships in `kb/upper/TimeContext.txt` either way. See docs/stp.md.
(allen-narrowing kb context)What the metric constraints pin down about the interval relations, as an Allen network
{[i j] → #{base relations}} for a caller to intersect into one read from stored facts.
This is the payoff of the bridge, and it runs one way only: metric narrows qualitative.
A closed gap of end(A) < start(B) leaves before the only Allen relation A and B can
stand in, and the thirteen signatures in endpoint-signature do the same for every other
shape of constraint. Nothing is asserted, nothing is mutated, and no interval network is
touched — the result is a value.
Only pairs the constraints actually narrow are recorded; a pair still open to all thirteen is the absence of a claim. nil when there is nothing to read: no metric constraints, no interval with both endpoints named, or an inconsistent network — which narrows nothing, since an unsatisfiable theory is not mined for conclusions.
What the metric constraints pin down about the *interval* relations, as an Allen network
`{[i j] → #{base relations}}` for a caller to intersect into one read from stored facts.
This is the payoff of the bridge, and it runs one way only: **metric narrows qualitative**.
A closed gap of `end(A) < start(B)` leaves `before` the only Allen relation A and B can
stand in, and the thirteen signatures in `endpoint-signature` do the same for every other
shape of constraint. Nothing is asserted, nothing is mutated, and no interval network is
touched — the result is a value.
Only pairs the constraints actually narrow are recorded; a pair still open to all thirteen
is the absence of a claim. nil when there is nothing to read: no metric constraints, no
interval with both endpoints named, or an inconsistent network — which narrows nothing,
since an unsatisfiable theory is not mined for conclusions.(close net nodes)All-pairs shortest paths over net across nodes, returning the tightest network the
constraints entail — or :inconsistent when some instant reaches itself at a negative
distance, which is a cycle of gaps that must all be closed and cannot be. A constraint
unsatisfiable as given counts too, whatever the node count: see
unsatisfiable-as-given?.
nodes is what the paths are drawn from, so it is the caller's obligation to pass
every node the network mentions — a node left out is a path never composed. Passing extra
nodes is always safe: an isolated one has no finite edge in either direction, so it can
tighten nothing and can be on no cycle.
Both verdicts are read to provers/*quantity-tolerance*, and that is what makes the
answer a claim about the knowledge rather than about the arithmetic that carried it. A
magnitude reaches here multiplied by a stored conversion factor, so one gap written two
ways — 1.1 Hour and 66 Minute — arrives as 3960.0000000000005 and 3960. Held to an
exact comparison the pair would cross, a chain of them would close a cycle at −5e-13, and
a KB whose own sameQuantity calls the two equal would have every metric goal in the
context refused over them. A contradiction wider than the epsilon is still one.
All-pairs shortest paths over `net` across `nodes`, returning the tightest network the constraints entail — or `:inconsistent` when some instant reaches itself at a negative distance, which is a cycle of gaps that must all be closed and cannot be. A constraint unsatisfiable *as given* counts too, whatever the node count: see `unsatisfiable-as-given?`. `nodes` is what the paths are drawn from, so it is the **caller's** obligation to pass every node the network mentions — a node left out is a path never composed. Passing extra nodes is always safe: an isolated one has no finite edge in either direction, so it can tighten nothing and can be on no cycle. Both verdicts are read to `provers/*quantity-tolerance*`, and that is what makes the answer a claim about the *knowledge* rather than about the arithmetic that carried it. A magnitude reaches here multiplied by a stored conversion factor, so one gap written two ways — `1.1 Hour` and `66 Minute` — arrives as 3960.0000000000005 and 3960. Held to an exact comparison the pair would cross, a chain of them would close a cycle at −5e-13, and a KB whose own `sameQuantity` calls the two equal would have every metric goal in the context refused over them. A contradiction wider than the epsilon is still one.
(closed-network kb context)The closed metric network visible from context, or nil when nothing is stated (or the
constraints span more than one dimension), or :inconsistent when they contradict.
The closed metric network visible from `context`, or nil when nothing is stated (or the constraints span more than one dimension), or `:inconsistent` when they contradict.
(closure kb context {:keys [net] :as prob} extra-nodes)The closed network of prob, memoized on the network value. :inconsistent when the
constraints contradict each other, reported through report-inconsistency! on the way
past — the closure has just proved it, and the alternative is a query that silently answers
nothing.
The key is the network alone, not the nodes a caller adds because its goal names them.
Such a node is isolated: it has a finite edge in neither direction, so it can tighten no
pair and lie on no cycle, and constraint answers unbounded for a pair the read-back never
recorded. So one caller's answer is another's, and the pass runs once per network rather
than once per shape of question.
The report is deliberately not on that path. Two KBs, or two contexts of one KB,
reaching the same network share the pass — and a ledger entry is a claim about a KB and a
context, so it hangs off observe/newly-seen? instead: this KB, this context, this
network. A cache hit still reports if the KB has not said it yet.
The closed network of `prob`, memoized on the network value. `:inconsistent` when the constraints contradict each other, reported through `report-inconsistency!` on the way past — the closure has just proved it, and the alternative is a query that silently answers nothing. The key is the **network alone**, not the nodes a caller adds because its goal names them. Such a node is isolated: it has a finite edge in neither direction, so it can tighten no pair and lie on no cycle, and `constraint` answers unbounded for a pair the read-back never recorded. So one caller's answer is another's, and the pass runs once per network rather than once per shape of question. The **report** is deliberately not on that path. Two KBs, or two contexts of one KB, reaching the same network share the pass — and a ledger entry is a claim about a KB and a context, so it hangs off `observe/newly-seen?` instead: this KB, this context, this network. A cache hit still reports if the KB has not said it yet.
(constraint net p q)The bound on t(q) − t(p) in net: exactly zero on the diagonal, the recorded interval,
else unbounded. The diagonal answers zero whatever is recorded there, because the only
gap between an instant and itself is none.
The bound on `t(q) − t(p)` in `net`: exactly zero on the diagonal, the recorded interval, else unbounded. The diagonal answers zero *whatever* is recorded there, because the only gap between an instant and itself is none.
The two predicates naming an interval's bounding instants — the bridge to the interval algebra.
The two predicates naming an interval's bounding instants — the bridge to the interval algebra.
Each Allen base relation as the four orderings it forces between two intervals' endpoints
— A's start against B's start, A's start against B's end, A's end against B's start, and
A's end against B's end. The keys are [which-of-A which-of-B].
Writing an interval as [start end] with start < end, these follow from the endpoint
inequalities that define the thirteen relations, with the comparisons those inequalities
leave implicit filled in: contains says A starts first and ends last, and therefore
A's start precedes B's end and A's end follows B's start. All four are pinned for every
relation, and the thirteen signatures are distinct — which is what makes them a decision
procedure rather than a filter that could pass two.
Each Allen base relation as the four orderings it forces between two intervals' endpoints — A's start against B's start, A's start against B's end, A's end against B's start, and A's end against B's end. The keys are `[which-of-A which-of-B]`. Writing an interval as `[start end]` with `start < end`, these follow from the endpoint inequalities that define the thirteen relations, with the comparisons those inequalities leave implicit filled in: `contains` says A starts first and ends last, and *therefore* A's start precedes B's end and A's end follows B's start. All four are pinned for every relation, and the thirteen signatures are distinct — which is what makes them a decision procedure rather than a filter that could pass two.
(endpoints-of kb i context)An interval's [start end] instants as (startOf I P) and (endOf I P) state them,
visible from context and believed — or nil when either is missing, or when either is
stated of two different instants, which is a disagreement no reasoning should paper
over.
An interval's `[start end]` instants as `(startOf I P)` and `(endOf I P)` state them, visible from `context` and believed — or nil when either is missing, or when either is stated of two *different* instants, which is a disagreement no reasoning should paper over.
(inconsistent? kb context)Do the temporalDistance constraints visible from context contradict each other?
Do the `temporalDistance` constraints visible from `context` contradict each other?
(intervals-with-endpoints kb context)Every interval both of whose bounding instants are named and agreed on, as
{interval [start end]}.
Every interval both of whose bounding instants are named and agreed on, as
`{interval [start end]}`.(narrow net p q lo hi)Intersect the constraint on [p q] with [lo hi], writing the converse bound on
[q p] with it. Intersection is [max of the los, min of the his] — commutative and
associative, so a network is a function of the constraints alone and never of the order
they were read in.
Intersect the constraint on `[p q]` with `[lo hi]`, writing the converse bound on `[q p]` with it. Intersection is `[max of the los, min of the his]` — commutative and associative, so a network is a function of the constraints alone and never of the order they were read in.
(negative-cycle-nodes d node-vec)The instants lying on some negative cycle of the closed distance graph d — exactly
those whose distance to themselves came out below zero. What a report can name when the
contradiction is derived rather than written.
Below zero by more than the tolerance. A cycle is a sum of stored magnitudes, each of them a stated figure multiplied by a stored conversion factor, so a chain that closes exactly can arrive back a sliver short — ten tenths of a second sum to 0.9999999999999999, and against a stated second that is a cycle of −1.1e-16. The band is the same one every other magnitude comparison here reads.
The instants lying on some negative cycle of the closed distance graph `d` — exactly those whose distance to themselves came out below zero. What a report can name when the contradiction is derived rather than written. **Below zero by more than the tolerance.** A cycle is a sum of stored magnitudes, each of them a stated figure multiplied by a stored conversion factor, so a chain that closes exactly can arrive back a sliver short — ten tenths of a second sum to 0.9999999999999999, and against a stated second that is a cycle of −1.1e-16. The band is the same one every other magnitude comparison here reads.
(nodes net)Every instant named by a constraint in net.
Every instant named by a constraint in `net`.
(overlap-bounds-from-endpoints closed [a-start a-end] [b-start b-end])How long two intervals overlap, as [lo hi], read off a closed metric network and their
endpoints alone.
The shared stretch runs from the later of the two starts to the earlier of the two ends, and is nothing at all when that is backwards:
overlap = max(0, min(a-end, b-end) − max(a-start, b-start))
and min(x,y) − max(p,q) is min(x−p, x−q, y−p, y−q), four gaps the network already
bounds. A minimum lies above the least of the lower bounds and below the least of the
upper ones, so both sides carry through soundly, and clamping at zero is monotone and
carries through with them.
How long two intervals overlap, as `[lo hi]`, read off a closed metric network and their endpoints alone. The shared stretch runs from the later of the two starts to the earlier of the two ends, and is nothing at all when that is backwards: overlap = max(0, min(a-end, b-end) − max(a-start, b-start)) and `min(x,y) − max(p,q)` is `min(x−p, x−q, y−p, y−q)`, four gaps the network already bounds. A minimum lies above the least of the lower bounds and below the least of the upper ones, so both sides carry through soundly, and clamping at zero is monotone and carries through with them.
(overlap-window kb context i1 i2)The bounds the metric constraints put on how long intervals i1 and i2 overlap, as
[[dimension unit] lo hi] in the dimension's base unit — hi possibly infinite, since a
network may pin a floor without a ceiling.
nil when there is nothing to read (no constraints, an endpoint missing, an inconsistent
network) and nil when the answer is the vacuous [0 ∞], which is not a bound at all.
vaelii.impl.duration intersects what comes back with the bound it computes from the
stored lengths and the qualitative relation set: both are sound, so their intersection is.
The bounds the metric constraints put on how long intervals `i1` and `i2` overlap, as `[[dimension unit] lo hi]` in the dimension's base unit — `hi` possibly infinite, since a network may pin a floor without a ceiling. nil when there is nothing to read (no constraints, an endpoint missing, an inconsistent network) and nil when the answer is the vacuous `[0 ∞]`, which is not a bound at all. `vaelii.impl.duration` intersects what comes back with the bound it computes from the stored lengths and the qualitative relation set: both are sound, so their intersection is.
(point-possibilities [lo hi])Which orderings of two instants a metric bound leaves open, as the base relations of
vaelii.impl.point: given [lo hi] on t(q) − t(p), p is before q while the gap can be
positive, coincident while it can be nil, and after while it can be negative. A bound is
a closed interval, so at least one always survives.
A gap sits within the tolerance of zero to count as nil, since a magnitude that ought
to be exactly nil arrives multiplied by a stored conversion factor and can come back a
last bit off — without the band an interval meeting another would read as overlapping it.
The same epsilon unsatisfiable-as-given? and negative-cycle-nodes read, which is what
keeps one network from being satisfiable and its orderings undecidable at once.
Which orderings of two instants a metric bound leaves open, as the base relations of `vaelii.impl.point`: given `[lo hi]` on `t(q) − t(p)`, p is before q while the gap can be positive, coincident while it can be nil, and after while it can be negative. A bound is a closed interval, so at least one always survives. A gap sits within the **tolerance** of zero to count as nil, since a magnitude that ought to be exactly nil arrives multiplied by a stored conversion factor and can come back a last bit off — without the band an interval meeting another would read as overlapping it. The same epsilon `unsatisfiable-as-given?` and `negative-cycle-nodes` read, which is what keeps one network from being satisfiable and its orderings undecidable at once.
(problem kb context)Every temporalDistance believed and visible from context, as {:dimension :unit :net}
— the network together with the dimension and base unit its magnitudes are in.
nil when nothing is stated, and nil when the stated constraints span more than one
dimension: magnitudes only add up once they are in one unit, so a mixed set is refused
outright rather than closed into numbers that mean nothing. That is the same gate
duration's sum applies, and it fails the same way — no answer, rather than a wrong one.
The refusal is reported (report-mixed-dimensions!), once per KB and context, because
its reach is the whole metric layer there rather than the one goal a sum refuses.
Resident on the KB's :qcn atom under a key of this namespace's own, stamped with
observe/change-clock exactly as a qualitative network is (qcn-kb/read-network), so a
rule joining a metric antecedent over many bindings reads the KB once rather than once
per binding — and so does a settle re-checking one firing after another.
Every `temporalDistance` believed and visible from `context`, as `{:dimension :unit :net}`
— the network together with the dimension and base unit its magnitudes are in.
nil when nothing is stated, and nil when the stated constraints span **more than one
dimension**: magnitudes only add up once they are in one unit, so a mixed set is refused
outright rather than closed into numbers that mean nothing. That is the same gate
`duration`'s sum applies, and it fails the same way — no answer, rather than a wrong one.
The refusal is **reported** (`report-mixed-dimensions!`), once per KB and context, because
its reach is the whole metric layer there rather than the one goal a sum refuses.
**Resident** on the KB's `:qcn` atom under a key of this namespace's own, stamped with
`observe/change-clock` exactly as a qualitative network is (`qcn-kb/read-network`), so a
rule joining a metric antecedent over many bindings reads the KB once rather than once
per binding — and so does a settle re-checking one firing after another.(relations-from-endpoints closed [a-start a-end] [b-start b-end])The Allen relations a closed metric network still permits between two intervals, given
each one's [start end] instants. A relation survives while every one of the four
orderings its signature demands is still possible.
Sound but not sharp: the four bounds are read independently, so a set of them that no single assignment of times realizes is not noticed here. That can only leave a relation in that the metric network in fact excludes, never take one out that it permits — which is the direction a narrowing must err in.
The Allen relations a closed metric network still permits between two intervals, given each one's `[start end]` instants. A relation survives while every one of the four orderings its signature demands is still possible. Sound but not sharp: the four bounds are read independently, so a set of them that no single assignment of times realizes is not noticed here. That can only leave a relation in that the metric network in fact excludes, never take one out that it permits — which is the direction a narrowing must err in.
(separation kb context p q)The tightest [lo hi] bound on t(q) − t(p) the constraints visible from context
entail, in the dimension's base unit, as [[dimension unit] lo hi].
nil when nothing is stated at all, and nil when the network is inconsistent — an
unsatisfiable theory is not mined for a number, the same rule the qualitative calculi
follow. A pair the constraints reach on neither side comes back [-∞ ∞], which is a real
answer ("nothing is known") and not an absent one.
The tightest `[lo hi]` bound on `t(q) − t(p)` the constraints visible from `context`
entail, in the dimension's base unit, as `[[dimension unit] lo hi]`.
nil when nothing is stated at all, and nil when the network is inconsistent — an
unsatisfiable theory is not mined for a number, the same rule the qualitative calculi
follow. A pair the constraints reach on neither side comes back `[-∞ ∞]`, which is a real
answer ("nothing is known") and not an absent one.The metric predicate a constraint is stated with, and the prover claims.
The metric predicate a constraint is stated with, and the prover claims.
(stp-prover)The metric temporal prover, to register with vaelii.core/add-prover.
The metric temporal prover, to register with `vaelii.core/add-prover`.
The constraint on a pair nothing is known about: the whole real line.
The constraint on a pair nothing is known about: the whole real line.
(unsatisfiable-pairs net)The pairs of net that unsatisfiable-as-given? refuses — what a reader wrote down that
no assignment of times can satisfy, before any closure. Empty when the network is
unsatisfiable only derivably, through a cycle, which is the case a report has no single
pair to blame for.
The pairs of `net` that `unsatisfiable-as-given?` refuses — what a reader wrote down that no assignment of times can satisfy, before any closure. Empty when the network is unsatisfiable only *derivably*, through a cycle, which is the case a report has no single pair to blame for.
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 |