The point algebra over time instants — a relation algebra over the generic
constraint network in vaelii.impl.qcn, and the smallest one there is. Three base
relations, jointly exhaustive and pairwise disjoint, so exactly one holds of any two
instants:
:before t(a) < t(b) :equal t(a) = t(b) :after t(a) > t(b)
vaelii.impl.interval is about stretches of time, which have extent and can therefore
meet, overlap and nest; this is about the moments themselves, where the only question is
which came first. The two meet at vaelii.impl.stp, which relates an interval to its
two endpoint instants and puts numbers on the gaps between them.
The same algebra appears twice in this tree. vaelii.impl.orientation composes two
independent one-dimensional projections to get the nine cardinal directions, and each
projection is exactly these three relations under the spellings :lt / :eq / :gt.
The table is duplicated rather than shared: there the three relations are a position on
an axis and are a private implementation detail of a nine-relation algebra, here they
are an order in time with their own vocabulary, and neither namespace should have to
read the other's keywords to say what it means. Nine identical entries are cheaper than
that coupling, and either copy is checkable against the definitions on its own.
Instants are stored as ordinary sentexes — the three named binary predicates
(instantBefore, instantAfter, instantEqual) plus three derived ones
(instantNotBefore, instantNotAfter, instantNotEqual) that each name a disjunction
of them. Instants are ordinary individuals; nothing about them is special, and nothing
here is about clocks or calendars — only about order.
The calculus reads every asserted instant relation visible from a context into a
qualitative constraint network — {[i j] → #{possible base relations}}, an unrecorded
pair meaning "unknown", i.e. all three — and qcn/path-consistent tightens it to a
fixpoint. The prover then answers a goal (P i j) by entailment: it holds iff every
relation still possible between i and j satisfies P, possible ⊆ denotation(P). So
(instantBefore A B) and (instantBefore B C) entail (instantBefore A C), and the
weaker (instantNotAfter A C) with it.
For three relations path consistency is not merely sound but complete: the point
algebra's full disjunctive form is tractable, and a network of it that survives the pass
has a model. So an emptied constraint here means genuine unsatisfiability, which is what
makes a cycle of strict instantBefore facts a reportable contradiction rather than a
suspicion.
The vocabulary ships in kb/upper/TimeContext.txt beside the interval relations. The
prover is opt-in on top of it: register it with vaelii.core/add-prover, and until
then a KB stores and retrieves instant relations as ordinary facts without paying for the
network.
The point algebra over time **instants** — a relation algebra over the generic
constraint network in `vaelii.impl.qcn`, and the smallest one there is. Three base
relations, jointly exhaustive and pairwise disjoint, so exactly one holds of any two
instants:
:before t(a) < t(b)
:equal t(a) = t(b)
:after t(a) > t(b)
`vaelii.impl.interval` is about stretches of time, which have extent and can therefore
meet, overlap and nest; this is about the moments themselves, where the only question is
which came first. The two meet at `vaelii.impl.stp`, which relates an interval to its
two endpoint instants and puts numbers on the gaps between them.
**The same algebra appears twice in this tree.** `vaelii.impl.orientation` composes two
independent one-dimensional projections to get the nine cardinal directions, and each
projection is exactly these three relations under the spellings `:lt` / `:eq` / `:gt`.
The table is duplicated rather than shared: there the three relations are a position on
an axis and are a private implementation detail of a nine-relation algebra, here they
are an order in time with their own vocabulary, and neither namespace should have to
read the other's keywords to say what it means. Nine identical entries are cheaper than
that coupling, and either copy is checkable against the definitions on its own.
Instants are **stored as ordinary sentexes** — the three named binary predicates
(`instantBefore`, `instantAfter`, `instantEqual`) plus three derived ones
(`instantNotBefore`, `instantNotAfter`, `instantNotEqual`) that each name a *disjunction*
of them. Instants are ordinary individuals; nothing about them is special, and nothing
here is about clocks or calendars — only about order.
The calculus reads every asserted instant relation visible from a context into a
qualitative constraint network — `{[i j] → #{possible base relations}}`, an unrecorded
pair meaning "unknown", i.e. all three — and `qcn/path-consistent` tightens it to a
fixpoint. The prover then answers a goal `(P i j)` by **entailment**: it holds iff every
relation still possible between i and j satisfies P, `possible ⊆ denotation(P)`. So
`(instantBefore A B)` and `(instantBefore B C)` entail `(instantBefore A C)`, and the
weaker `(instantNotAfter A C)` with it.
For three relations path consistency is not merely sound but **complete**: the point
algebra's full disjunctive form is tractable, and a network of it that survives the pass
has a model. So an emptied constraint here means genuine unsatisfiability, which is what
makes a cycle of strict `instantBefore` facts a reportable contradiction rather than a
suspicion.
The vocabulary ships in `kb/upper/TimeContext.txt` beside the interval relations. The
prover is **opt-in** on top of it: register it with `vaelii.core/add-prover`, and until
then a KB stores and retrieves instant relations as ordinary facts without paying for the
network.The three jointly-exhaustive, pairwise-disjoint instant relations — the universe of the algebra, and so the constraint on a pair nothing is known about.
The three jointly-exhaustive, pairwise-disjoint instant relations — the universe of the algebra, and so the constraint on a pair nothing is known about.
Base relation keyword → the binary predicate a fact about it is stored under. Every
name carries the instant prefix: before and after are already Allen's interval
relations, and a moment ordered against a moment is a different claim from a stretch
ordered against a stretch. :equal is instantEqual for the reason intervalEqual is
not equals — two instants coinciding is a claim about time, not about the identity of
two terms.
Base relation keyword → the binary predicate a fact about it is stored under. Every name carries the `instant` prefix: `before` and `after` are already Allen's *interval* relations, and a moment ordered against a moment is a different claim from a stretch ordered against a stretch. `:equal` is `instantEqual` for the reason `intervalEqual` is not `equals` — two instants coinciding is a claim about time, not about the identity of two terms.
(compose s1 s2)The composition of two relation SETS: every base relation possible between a and c when
r(a,b) ∈ s1 and r(b,c) ∈ s2 — the union of the table entries, since a disjunction on
either side admits every combination.
The composition of two relation SETS: every base relation possible between a and c when r(a,b) ∈ `s1` and r(b,c) ∈ `s2` — the union of the table entries, since a disjunction on either side admits every combination.
(constraint net i j)The constraint set on [i j] in net: #{:equal} on the diagonal, the recorded set,
else all three (unknown).
The constraint set on `[i j]` in `net`: `#{:equal}` on the diagonal, the recorded set,
else all three (unknown).(converse-set rels)The converse of a relation set — how an asserted (P a b) constraint is read backwards
as the constraint on (b a).
The converse of a relation set — how an asserted `(P a b)` constraint is read backwards as the constraint on `(b a)`.
(definite-point-relation kb context i1 i2)The single base relation between i1 and i2 when path consistency pins it down;
:inconsistent when the network contradicts itself, :unknown when two or more relations
remain possible.
The single base relation between `i1` and `i2` when path consistency pins it down; `:inconsistent` when the network contradicts itself, `:unknown` when two or more relations remain possible.
(inconsistent? kb context)Is the instant network visible from context unsatisfiable?
Is the instant network visible from `context` unsatisfiable?
Every instant predicate — the three base ones and the three derived ones — mapped to the
set of base relations it denotes. A goal (P a b) is entailed exactly when the relations
still possible between a and b are a subset of P's denotation, so a derived predicate is
entailed by more networks than a base one, and the base predicates are the singletons.
The three derived predicates are each the complement of one base relation, and over a
jointly-exhaustive triple a complement is a negation — so the names are literal.
instantNotAfter is ≤ and instantNotBefore is ≥, which is what a temporal ordering
usually wants; instantNotEqual is ≠. With them the vocabulary names every disjunction
the algebra can express bar the universe, which is the absence of a claim and needs no
name.
Every instant predicate — the three base ones and the three derived ones — mapped to the set of base relations it denotes. A goal `(P a b)` is entailed exactly when the relations still possible between a and b are a *subset* of P's denotation, so a derived predicate is entailed by more networks than a base one, and the base predicates are the singletons. The three derived predicates are each the complement of one base relation, and over a jointly-exhaustive triple a complement *is* a negation — so the names are literal. `instantNotAfter` is ≤ and `instantNotBefore` is ≥, which is what a temporal ordering usually wants; `instantNotEqual` is ≠. With them the vocabulary names every disjunction the algebra can express bar the universe, which is the absence of a claim and needs no name.
The point algebra as a vaelii.impl.qcn-kb calculus — the algebra, the vocabulary, and
the two caches. Everything below delegates to the shared glue, which is the same code
RCC-8, the cardinal directions and Allen's intervals run.
The point algebra as a `vaelii.impl.qcn-kb` calculus — the algebra, the vocabulary, and the two caches. Everything below delegates to the shared glue, which is the same code RCC-8, the cardinal directions and Allen's intervals run.
The point algebra as a vaelii.impl.qcn relation algebra.
The point algebra as a `vaelii.impl.qcn` relation algebra.
(get-in point-composition [r1 r2]) is the set of base relations possible between a and
c given r1(a,b) and r2(b,c). :equal is the identity element on both sides.
Only two entries lose information, and they are the same shape twice: a before b with b after c puts both a and c on the far side of b, in either order, so nothing at all follows. Everything else is a singleton — which is why a chain of strict orderings composes to a strict ordering however long it is.
`(get-in point-composition [r1 r2])` is the set of base relations possible between a and c given `r1`(a,b) and `r2`(b,c). `:equal` is the identity element on both sides. Only two entries lose information, and they are the same shape twice: a before b with b after c puts both a and c on the far side of b, in either order, so nothing at all follows. Everything else is a singleton — which is why a chain of strict orderings composes to a strict ordering however long it is.
Each base relation's converse — reading the claim backwards. One pair and one
self-converse, since :equal is the identity.
Each base relation's converse — reading the claim backwards. One pair and one self-converse, since `:equal` is the identity.
(point-prover)The point-algebra entailment prover, to register with vaelii.core/add-prover.
The point-algebra entailment prover, to register with `vaelii.core/add-prover`.
(possible-point-relations kb context i1 i2)The base relations still possible between instants i1 and i2 given everything
believed in context — #{} when the network is inconsistent.
This is the algebra read directly rather than through a goal, so a caller that needs to know how much is pinned down — rather than whether one named relation is entailed — asks here.
The base relations still possible between instants `i1` and `i2` given everything
believed in `context` — `#{}` when the network is inconsistent.
This is the algebra read directly rather than through a goal, so a caller that needs to
know *how much* is pinned down — rather than whether one named relation is entailed —
asks here.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 |