Metric time as a simple temporal problem: bounds lo ≤ t(Q) − t(P) ≤ hi on the gaps
between instants, closed by all-pairs shortest paths, unsatisfiable on a negative cycle.
The algorithm half is pure data; the KB half reads temporalDistance measures, answers
them through TemporalDistanceProver (opt-in, :metric-time), and bridges the bounds
onto Allen's intervals through startOf / endOf for vaelii.impl.interval and
vaelii.impl.duration. See docs/stp.md.
Metric time as a **simple temporal problem**: bounds `lo ≤ t(Q) − t(P) ≤ hi` on the gaps between instants, closed by all-pairs shortest paths, unsatisfiable on a negative cycle. The algorithm half is pure data; the KB half reads `temporalDistance` measures, answers them through `TemporalDistanceProver` (opt-in, `:metric-time`), and bridges the bounds onto Allen's intervals through `startOf` / `endOf` for `vaelii.impl.interval` and `vaelii.impl.duration`. See docs/stp.md.
(allen-narrowing kb context)allen-narrowing-with-support's relation sets alone.
`allen-narrowing-with-support`'s relation sets alone.
The dynamic vars the metric narrowing of the interval algebra reads: the tolerance the
magnitudes are snapped to. vaelii.impl.interval declares these as the narrowing's
:bindings.
The dynamic vars the metric narrowing of the interval algebra reads: the tolerance the magnitudes are snapped to. `vaelii.impl.interval` declares these as the narrowing's `:bindings`.
Every predicate the metric narrowing of the interval algebra reads: the constraints, the
endpoint predicates and the unit table. vaelii.impl.interval declares these as the
narrowing's :sources.
Every predicate the metric narrowing of the interval algebra reads: the constraints, the endpoint predicates and the unit table. `vaelii.impl.interval` declares these as the narrowing's `:sources`.
(allen-narrowing-with-support kb context)What the metric layer determines about the Allen relations, as
{:net {[i j] → #{base relations}} :support {[i j] → #{handle}}} in the calculus
narrowing shape. A pair's support is both intervals' endpoint facts and the chains behind
the four endpoint-gaps. Only narrowed pairs are recorded. nil with no constraints, no
interval with both endpoints, or one such interval and a satisfiable network. An
unsatisfiable network answers per-component-narrowing. A problem refused for spanning
more than one dimension answers unsatisfiable-narrowing over the intervals its
constraints bound, its :metric source naming the :dimensions (docs/stp.md,
"Constraints are measures").
What the metric layer determines about the Allen relations, as
`{:net {[i j] → #{base relations}} :support {[i j] → #{handle}}}` in the calculus
narrowing shape. A pair's support is both intervals' endpoint facts and the chains behind
the four `endpoint-gaps`. Only narrowed pairs are recorded. nil with no constraints, no
interval with both endpoints, or one such interval and a satisfiable network. An
unsatisfiable network answers `per-component-narrowing`. A problem refused for spanning
more than one dimension answers `unsatisfiable-narrowing` over the intervals its
constraints bound, its `:metric` source naming the `:dimensions` (docs/stp.md,
"Constraints are measures").The thirteen Allen base relations, read off endpoint-signature because
vaelii.impl.interval requires this namespace and not the reverse.
The thirteen Allen base relations, read off `endpoint-signature` because `vaelii.impl.interval` requires this namespace and not the reverse.
(close net nodes)close-state's :net, or :inconsistent. The caller passes every node net
mentions; extra nodes are isolated and change nothing.
`close-state`'s `:net`, or `:inconsistent`. The caller passes every node `net` mentions; extra nodes are isolated and change nothing.
(close-state net nodes)All-pairs shortest paths over net across nodes, as a closed state
{:net {[p q] → [lo hi]} :node-vec [instant …] :d ^doubles}, or :inconsistent on a
constraint unsatisfiable as given or a negative cycle. :d is written once; every
function taking a state copies it before an update.
All-pairs shortest paths over `net` across `nodes`, as a closed state
`{:net {[p q] → [lo hi]} :node-vec [instant …] :d ^doubles}`, or `:inconsistent` on a
constraint unsatisfiable as given or a negative cycle. `:d` is written once; every
function taking a state copies it before an update.(close-state-from net prior nodes)close-state, warm-started off prior, a closed state for a network net tightens
(tightening-of?): each moved constraint is relaxed in, and only moved bounds are read
back. At n or more moved edges it runs the full pass instead.
nodes must name every instant of prior as well as of net. A prior that net does
not tighten gives a wrong network, not an error.
`close-state`, warm-started off `prior`, a closed state for a network `net` tightens (`tightening-of?`): each moved constraint is relaxed in, and only moved bounds are read back. At `n` or more moved edges it runs the full pass instead. `nodes` must name every instant of `prior` as well as of `net`. A `prior` that `net` does not tighten gives a wrong network, not an error.
(closed-network kb context)The closed metric network visible from context: nil when problem is, else closure's
answer.
The closed metric network visible from `context`: nil when `problem` is, else `closure`'s answer.
(closure kb context {:keys [net] :as prob} extra-nodes)The closed network of prob across its nodes and extra-nodes, or :inconsistent.
Memoized on [net provers/*quantity-tolerance*], and resident per context and tolerance:
extra-nodes are isolated and stay out of the key, so contexts and KBs holding one
network share one pass. Warm-started (close-state-from) when the network last
resident for context is one this network tightens. An inconsistency is reported once per KB, context and network
(observe/newly-seen?), never on the memoized path.
The closed network of `prob` across its nodes and `extra-nodes`, or `:inconsistent`. Memoized on `[net provers/*quantity-tolerance*]`, and resident per context and tolerance: `extra-nodes` are isolated and stay out of the key, so contexts and KBs holding one network share one pass. Warm-started (`close-state-from`) when the network last resident for `context` is one this network tightens. An inconsistency is reported once per KB, context and network (`observe/newly-seen?`), never on the memoized path.
(constraint net p q)The bound on t(q) − t(p) in net: [0 0] on the diagonal whatever is recorded there,
else the recorded interval, else unbounded.
The bound on `t(q) − t(p)` in `net`: `[0 0]` on the diagonal whatever is recorded there, else the recorded interval, else unbounded.
(endpoint-gaps [a-start a-end] [b-start b-end])The four instant pairs an Allen relation between intervals [a-start a-end] and
[b-start b-end] is decided by, keyed as endpoint-signature keys them. The narrowing
and its support both read these.
The four instant pairs an Allen relation between intervals `[a-start a-end]` and `[b-start b-end]` is decided by, keyed as `endpoint-signature` keys them. The narrowing and its support both read these.
The two predicates naming an interval's bounding instants.
The two predicates naming an interval's bounding instants.
Each Allen base relation as the ordering it forces on each of the four endpoint
comparisons, keyed [which-of-A which-of-B]. The thirteen signatures are distinct.
Each Allen base relation as the ordering it forces on each of the four endpoint comparisons, keyed `[which-of-A which-of-B]`. The thirteen signatures are distinct.
(endpoints-with-support kb i context)Interval i's [[start end] handles] from the believed, visible startOf / endOf
facts and those facts' handles. nil when either is missing or names two different
instants; one instant restated in several visible contexts is one reading, all its
handles named.
Interval `i`'s `[[start end] handles]` from the believed, visible `startOf` / `endOf` facts and those facts' handles. nil when either is missing or names two different instants; one instant restated in several visible contexts is one reading, all its handles named.
(intervals-with-endpoints kb context){interval [[start end] #{handle}]} for every interval endpoints-with-support reads.
`{interval [[start end] #{handle}]}` for every interval `endpoints-with-support` reads.
(merge-narrowings narrowings)narrowings intersected pair by pair, their support unioned and their unsatisfiable
sources listed in order. An absent pair is the universe in each, so a pair one of them
narrows takes that one's set. nil when every one is nil.
`narrowings` intersected pair by pair, their support unioned and their unsatisfiable sources listed in order. An absent pair is the universe in each, so a pair one of them narrows takes that one's set. nil when every one is nil.
(narrow net p q lo hi)Intersect the constraint on [p q] with [lo hi], writing the converse [q p] with it.
Commutative and associative, so a network is a function of its constraints' set.
Intersect the constraint on `[p q]` with `[lo hi]`, writing the converse `[q p]` with it. Commutative and associative, so a network is a function of its constraints' set.
(negative-cycle-nodes d node-vec)The instants whose self-distance in the closed matrix d is below zero by more than
provers/*quantity-tolerance*.
The instants whose self-distance in the closed matrix `d` is below zero by more than `provers/*quantity-tolerance*`.
(nodes net)Every instant named by a constraint in net.
Every instant named by a constraint in `net`.
(overlap-bounds-from-endpoints closed ea eb)How long two intervals overlap, as [lo hi], read off a closed network and their
[start end] instants (docs/stp.md, "Sharpening an overlap").
How long two intervals overlap, as `[lo hi]`, read off a closed network and their `[start end]` instants (docs/stp.md, "Sharpening an overlap").
(overlap-window-with-support kb context i1 i2)The metric bound on how long intervals i1 and i2 overlap, as
[[[dimension unit] lo hi] handles] — hi possibly infinite — with the endpoint facts
and the chains behind the four overlap-gaps as its support. nil when there is nothing
to read, the network is inconsistent, or the bound is the vacuous [0 ∞].
The metric bound on how long intervals `i1` and `i2` overlap, as `[[[dimension unit] lo hi] handles]` — `hi` possibly infinite — with the endpoint facts and the chains behind the four `overlap-gaps` as its support. nil when there is nothing to read, the network is inconsistent, or the bound is the vacuous `[0 ∞]`.
(point-possibilities [lo hi])The vaelii.impl.point base relations a bound [lo hi] on t(q) − t(p) leaves open:
:before while the gap can be positive, :equal while it can be zero, :after while it
can be negative, each read to provers/*quantity-tolerance*. Never empty.
The `vaelii.impl.point` base relations a bound `[lo hi]` on `t(q) − t(p)` leaves open: `:before` while the gap can be positive, `:equal` while it can be zero, `:after` while it can be negative, each read to `provers/*quantity-tolerance*`. Never empty.
(problem kb context)Every temporalDistance believed and visible from context, as
{:dimension :unit :net :support}. nil when nothing is stated, and nil — reported once
per KB and context — when the constraints span more than one dimension.
Every `temporalDistance` believed and visible from `context`, as
`{:dimension :unit :net :support}`. nil when nothing is stated, and nil — reported once
per KB and context — when the constraints span more than one dimension.(relations-from-endpoints closed ea eb)The Allen relations the closed network closed still permits between intervals with
[start end] instants ea and eb: those whose every signature ordering is still
possible. The reading is sound but not sharp (docs/stp.md).
The Allen relations the closed network `closed` still permits between intervals with `[start end]` instants `ea` and `eb`: those whose every signature ordering is still possible. The reading is sound but not sharp (docs/stp.md).
(separation kb context p q)The tightest [lo hi] on t(q) − t(p) visible from context, as
[[dimension unit] lo hi] in the base unit; [-∞ ∞] for a pair nothing reaches. nil
when nothing is stated or the network is inconsistent.
The tightest `[lo hi]` on `t(q) − t(p)` visible from `context`, as `[[dimension unit] lo hi]` in the base unit; `[-∞ ∞]` for a pair nothing reaches. nil when nothing is stated or the network is inconsistent.
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 — (vaelii.core/add-reasoner kb :metric-time).
The metric temporal prover — `(vaelii.core/add-reasoner kb :metric-time)`.
(tightening-of? net prior)Is every bound prior records at least as wide as the one net records for the same
pair? The precondition for close-state-from.
Is every bound `prior` records at least as wide as the one `net` records for the same pair? The precondition for `close-state-from`.
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-narrowing intervals support source)The narrowing an unsatisfiable or refused source answers over intervals, the intervals
its unsatisfiable component bounds: the pair from the first under nm/print-key to each
other emptied both ways, or the first's diagonal emptied when it is the only one,
support behind each. An empty constraint is unsatisfiable as given, so the component
of the interval network holding those intervals is unsatisfiable, and no goal naming one
is answered (docs/qcn.md, "Unsatisfiability is per component"). nil for no intervals.
:unsatisfiable-sources carries source, the description of the clash in the source
network or of its refusal, with the emptied pairs as its :stand-in: they stand in for
the source's clash or refusal and are not pairs any interval fact contradicts
(qcn-kb/unsatisfiable-sources).
Answering nil instead would widen the interval network when a fact arrives, and an entailment drawn through the narrowing would stop holding while the firing that rested on it stayed believed (docs/qcn.md, "A network can have a second reader").
The narrowing an unsatisfiable or refused source answers over `intervals`, the intervals its unsatisfiable component bounds: the pair from the first under `nm/print-key` to each other emptied both ways, or the first's diagonal emptied when it is the only one, `support` behind each. An empty constraint is unsatisfiable as given, so the component of the interval network holding those intervals is unsatisfiable, and no goal naming one is answered (docs/qcn.md, "Unsatisfiability is per component"). nil for no intervals. `:unsatisfiable-sources` carries `source`, the description of the clash in the source network or of its refusal, with the emptied pairs as its `:stand-in`: they stand in for the source's clash or refusal and are not pairs any interval fact contradicts (`qcn-kb/unsatisfiable-sources`). Answering nil instead would widen the interval network when a fact arrives, and an entailment drawn through the narrowing would stop holding while the firing that rested on it stayed believed (docs/qcn.md, "A network can have a second reader").
(unsatisfiable-pairs net)The pairs of net that are unsatisfiable as written; empty when the network is
unsatisfiable only through a cycle.
The pairs of `net` that are unsatisfiable as written; empty when the network is unsatisfiable only through a cycle.
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 |