Relative direction — where one thing lies from another as seen from a point of
view: the mouse on the lion's left, the crow in front of the fox. A relation algebra
over the generic constraint network in vaelii.impl.qcn, beside the RCC-8 topology of
vaelii.impl.space, the cardinal directions of vaelii.impl.orientation and Allen's
intervals in vaelii.impl.interval. The compass says where a place is on the map;
this says where a thing is from where you stand, which is the only thing a story ever
says.
The frame of reference is the context. Relative direction is ternary in the
literature — A is left of B from viewpoint C — and a constraint network is strictly
binary, a constraint being a set of relations on a pair. The resolution is that a
context already is a frame of reference: a network is built per context out of the
facts visible there, so (leftOf Mouse Lion) asserted in LionMouseContext is a claim
in that microtheory's frame and in no other. Two microtheories looking at the same
individuals from opposite sides state opposite facts and neither contaminates the
other; a frame that has to be argued about rather than assumed is a context, and the
argument is genlContext. So this calculus is binary, composes exactly as the
cardinal directions do, and needs nothing of the shared glue that the other three do
not already need.
The nine base relations are the projection-based calculus that shape allows. A
relative direction decomposes into two independent one-dimensional point relations,
one per axis of the frame — left-right, and front-back — each :lt / :eq / :gt,
reading the axes as coordinates that grow rightwards and frontwards:
:left [:lt :eq] :front-left [:lt :gt] :behind-left [:lt :lt] :right [:gt :eq] :front-right [:gt :gt] :behind-right [:gt :lt] :front [:eq :gt] :behind [:eq :lt] :eq [:eq :eq]
That decomposition is the whole trick, and it is why there is no 9×9 table here:
composition is computed, not transcribed. Composing two relations is composing
their left-right projections and their front-back projections separately through the
three-relation point algebra, then reading the result pairs back as relations. Since
the nine relations are exactly the nine [left-right front-back] combinations, that
read-back is total and the composition of any two base relations is a non-empty set —
so the table nobody wrote down cannot disagree with itself, and left-then-in-front is
front-left because :lt;:eq is :lt on one axis and :eq;:gt is :gt on the other.
(The one-dimensional point algebra below is the same mathematics the cardinal
directions project onto; the two calculi share it as a fact about ordered axes, not as
code, and neither reads the other's vocabulary.)
Relative directions are stored as ordinary sentexes — the nine named binary
predicates (leftOf, frontRightOf, sameRelativePositionAs, …), plus four derived
predicates (leftwardOf, frontwardOf, …) that each name a disjunction of them: a
leftward component, whatever the front-back one. The things related are ordinary
individuals; nothing about them is special, and nothing declares a viewpoint, because
the context is the viewpoint.
The calculus reads every asserted relation visible from a context into a
qualitative constraint network — {[a b] → #{possible base relations}}, an unrecorded
pair meaning "unknown", i.e. all nine — and qcn/path-consistent tightens it to a
fixpoint. The prover then answers a goal (P a b) by entailment: it holds iff
every relation still possible between a and b satisfies P, possible ⊆ denotation(P).
So (leftOf A B) and (leftOf B D) entail (leftOf A D), and with it the weaker
(leftwardOf A D).
An emptied constraint anywhere means the asserted relations are unsatisfiable, and then no goal of this calculus is answered in that context — an inconsistent theory should not be mined for conclusions. Since the frame is the context, an inconsistency is confined to the frame it was stated in.
Soundness. Path consistency is sound but not in general complete, so an entailment
reported here is real while a non-entailment means "not provable", never "provably
false" — the same open-world reading argIsa and exceptWhen take.
The vocabulary ships in kb/upper/SpaceContext.txt beside the topology, the compass and
the distance scale — all of them are about space, so CoreContext keeps only the
grammar they are declared in. The prover is opt-in on top of it: register it with
vaelii.core/add-prover, and until then a KB stores and retrieves relative directions
as ordinary facts without paying for the network.
Relative direction — where one thing lies from another **as seen from a point of
view**: the mouse on the lion's left, the crow in front of the fox. A relation algebra
over the generic constraint network in `vaelii.impl.qcn`, beside the RCC-8 topology of
`vaelii.impl.space`, the cardinal directions of `vaelii.impl.orientation` and Allen's
intervals in `vaelii.impl.interval`. The compass says where a place is on the map;
this says where a thing is from where you stand, which is the only thing a story ever
says.
**The frame of reference is the context.** Relative direction is ternary in the
literature — A is left of B *from viewpoint C* — and a constraint network is strictly
binary, a constraint being a set of relations on a *pair*. The resolution is that a
context already **is** a frame of reference: a network is built per context out of the
facts visible there, so `(leftOf Mouse Lion)` asserted in `LionMouseContext` is a claim
in that microtheory's frame and in no other. Two microtheories looking at the same
individuals from opposite sides state opposite facts and neither contaminates the
other; a frame that has to be argued about rather than assumed is a context, and the
argument is `genlContext`. So this calculus is binary, composes exactly as the
cardinal directions do, and needs nothing of the shared glue that the other three do
not already need.
The nine base relations are the projection-based calculus that shape allows. A
relative direction decomposes into two **independent** one-dimensional point relations,
one per axis of the frame — left-right, and front-back — each `:lt` / `:eq` / `:gt`,
reading the axes as coordinates that grow rightwards and frontwards:
:left [:lt :eq] :front-left [:lt :gt] :behind-left [:lt :lt]
:right [:gt :eq] :front-right [:gt :gt] :behind-right [:gt :lt]
:front [:eq :gt] :behind [:eq :lt] :eq [:eq :eq]
That decomposition is the whole trick, and it is why there is no 9×9 table here:
**composition is computed, not transcribed.** Composing two relations is composing
their left-right projections and their front-back projections separately through the
three-relation point algebra, then reading the result pairs back as relations. Since
the nine relations are exactly the nine `[left-right front-back]` combinations, that
read-back is total and the composition of any two base relations is a non-empty set —
so the table nobody wrote down cannot disagree with itself, and left-then-in-front *is*
front-left because `:lt;:eq` is `:lt` on one axis and `:eq;:gt` is `:gt` on the other.
(The one-dimensional point algebra below is the same mathematics the cardinal
directions project onto; the two calculi share it as a fact about ordered axes, not as
code, and neither reads the other's vocabulary.)
Relative directions are **stored as ordinary sentexes** — the nine named binary
predicates (`leftOf`, `frontRightOf`, `sameRelativePositionAs`, …), plus four derived
predicates (`leftwardOf`, `frontwardOf`, …) that each name a *disjunction* of them: a
leftward component, whatever the front-back one. The things related are ordinary
individuals; nothing about them is special, and nothing declares a viewpoint, because
the context is the viewpoint.
The calculus reads every asserted relation visible from a context into a
qualitative constraint network — `{[a b] → #{possible base relations}}`, an unrecorded
pair meaning "unknown", i.e. all nine — and `qcn/path-consistent` tightens it to a
fixpoint. The prover then answers a goal `(P a b)` by **entailment**: it holds iff
every relation still possible between a and b satisfies P, `possible ⊆ denotation(P)`.
So `(leftOf A B)` and `(leftOf B D)` entail `(leftOf A D)`, and with it the weaker
`(leftwardOf A D)`.
An emptied constraint anywhere means the asserted relations are unsatisfiable, and then
*no* goal of this calculus is answered in that context — an inconsistent theory should
not be mined for conclusions. Since the frame is the context, an inconsistency is
confined to the frame it was stated in.
**Soundness.** Path consistency is sound but not in general complete, so an entailment
reported here is real while a *non*-entailment means "not provable", never "provably
false" — the same open-world reading `argIsa` and `exceptWhen` take.
The vocabulary ships in `kb/upper/SpaceContext.txt` beside the topology, the compass and
the distance scale — all of them are *about* space, so CoreContext keeps only the
grammar they are declared in. The prover is **opt-in** on top of it: register it with
`vaelii.core/add-prover`, and until then a KB stores and retrieves relative directions
as ordinary facts without paying for the network.The nine base relative directions — the four sides, the four corners between them, and coincidence. Jointly exhaustive and pairwise disjoint, so exactly one holds of any two things in one frame, and this is the universe of the algebra: the constraint on a pair nothing is known about.
The nine base relative directions — the four sides, the four corners between them, and coincidence. Jointly exhaustive and pairwise disjoint, so exactly one holds of any two things in one frame, and this is the universe of the algebra: the constraint on a pair nothing is known about.
The projection read backwards. It is total over the nine [left-right front-back]
combinations — three point relations on each of two axes, nine relations — which is what
makes composition total: whatever pair of point relations the axes compose to names a
relation, so no combination falls out of the algebra.
The projection read backwards. It is **total** over the nine `[left-right front-back]` combinations — three point relations on each of two axes, nine relations — which is what makes composition total: whatever pair of point relations the axes compose to names a relation, so no combination falls out of the algebra.
Base relation keyword → the binary predicate a fact about it is stored under. :eq is
spelled sameRelativePositionAs rather than borrowing the compass's sameLocationAs:
a predicate belongs to exactly one calculus, each network reads only its own vocabulary,
and this one is a claim about a frame's own axes.
Base relation keyword → the binary predicate a fact about it is stored under. `:eq` is spelled `sameRelativePositionAs` rather than borrowing the compass's `sameLocationAs`: a predicate belongs to exactly one calculus, each network reads only its own vocabulary, and this one is a claim about a frame's own axes.
(compose s1 s2)The composition of two relation SETS: every relative direction possible from x to z
when the direction x→y is in s1 and y→z is in s2.
Computed, never looked up. Each relation is a pair of independent axis projections, so
composing them is composing each axis through point-compose and taking the product of
the two results — left-then-in-front is :lt;:eq = :lt on the left-right axis and
:eq;:gt = :gt on the front-back one, which is front-left. Two opposite corners lose
both axes at once and compose to the whole universe.
Both relations are read in one frame, which is what makes the composition legitimate at all: the network they live in is the network of a single context.
The composition of two relation SETS: every relative direction possible from x to z when the direction x→y is in `s1` and y→z is in `s2`. Computed, never looked up. Each relation is a pair of independent axis projections, so composing them is composing each axis through `point-compose` and taking the product of the two results — left-then-in-front is `:lt;:eq` = `:lt` on the left-right axis and `:eq;:gt` = `:gt` on the front-back one, which is front-left. Two opposite corners lose both axes at once and compose to the whole universe. Both relations are read in **one** frame, which is what makes the composition legitimate at all: the network they live in is the network of a single context.
(constraint net i j)The constraint set on [i j] in net: #{:eq} on the diagonal, the recorded set,
else all nine (unknown).
The constraint set on `[i j]` in `net`: `#{:eq}` on the diagonal, the recorded set,
else all nine (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-relative-direction kb context a b)The single base relation from a to b when path consistency pins it down;
:inconsistent when the network contradicts itself, :unknown when two or more
relations remain possible.
The single base relation from `a` to `b` 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 relative-direction network visible from context unsatisfiable? A frame can be
incoherent on its own without saying anything about any other.
Is the relative-direction network visible from `context` unsatisfiable? A frame can be incoherent on its own without saying anything about any other.
The one-dimensional point algebra: [a b] → the relations possible between x and z
when a relates x to y and b relates y to z. Only the two disagreeing pairs lose
information — x < y and y > z says nothing at all about x and z.
The one-dimensional point algebra: `[a b]` → the relations possible between x and z when a relates x to y and b relates y to z. Only the two disagreeing pairs lose information — x < y and y > z says nothing at all about x and z.
The one-dimensional point algebra's converse: reading a relation backwards flips it.
The one-dimensional point algebra's converse: reading a relation backwards flips it.
(possible-relative-directions kb context a b)The base relations still possible from a to b in the frame context names, given
everything believed there — #{} when the network is inconsistent.
The base relations still possible from `a` to `b` in the frame `context` names, given
everything believed there — `#{}` when the network is inconsistent.Each base relation as its [left-right front-back] projection — where the target lies
on the frame's left-right axis, and where on its front-back one. The coordinates grow
rightwards and frontwards, so :lt on the first axis is to the left and :gt on the
second is in front.
Each base relation as its `[left-right front-back]` projection — where the target lies on the frame's left-right axis, and where on its front-back one. The coordinates grow rightwards and frontwards, so `:lt` on the first axis is *to the left* and `:gt` on the second is *in front*.
Relative direction 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 the other calculi run.
Relative direction 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 the other calculi run.
Relative direction as a vaelii.impl.qcn relation algebra.
Relative direction as a `vaelii.impl.qcn` relation algebra.
Every relative-direction predicate — the nine base ones and the four derived ones —
mapped to the set of base relations it denotes. A goal (P a b) is entailed exactly
when the relations still possible from a to 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 four derived predicates each constrain one axis and leave the other open:
leftwardOf is anything with a leftward component, whatever it does front-to-back.
None of them contains :eq, so none holds of a thing and itself.
Every relative-direction predicate — the nine base ones and the four derived ones — mapped to the set of base relations it denotes. A goal `(P a b)` is entailed exactly when the relations still possible from a to 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 four derived predicates each constrain one axis and leave the other open: `leftwardOf` is anything with a leftward component, whatever it does front-to-back. None of them contains `:eq`, so none holds of a thing and itself.
(relative-prover)The relative-direction entailment prover, to register with vaelii.core/add-prover.
The relative-direction entailment prover, to register with `vaelii.core/add-prover`.
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 |