The clock behind the calendar constructors — where (YearFn 2000) stops being a name
the interval algebra relates and starts being a stretch between two moments.
vaelii.impl.datetime reads a calendar term to its fields and to the half-open
[start end] it lies between; this namespace is the KB-facing half, one prover
answering three families of goal out of that reading and storing nothing:
(startOf (YearFn 2000) ?i) ?i = (InstantFn 2000 1 1 0 0 0) (endOf (YearFn 2000) ?i) ?i = (InstantFn 2001 1 1 0 0 0) (instantBefore (InstantFn 1999 6 1 0 0 0) (InstantFn 2000 1 1 0 0 0)) (during (MonthFn 2000 3) (YearFn 2000)) (meets (MonthFn 2000 2) (MonthFn 2000 3))
Answered, never stored. Nothing here mints a term, asserts a sentex or posts a
justification, so a computed endpoint is not a belief, needs no retraction, and leaves
no orphan for the NAT sweep to ask about (docs/nat.md). What it rests on is the
calendar and the convention, both of which are in this code rather than in the store —
which is why it implements Prover and not SupportingProver: there is no handle to
name, and a prover that names none is one whose answer no retraction can invalidate
(docs/inference.md, "What a computed answer rests on").
Half-open, [start, end). A term's end is the first moment of the next term at the
same precision, so the end of 1999 and the start of 2000 are the same term and
consecutive calendar terms meet. (before (YearFn 1999) (YearFn 2000)) therefore
does not hold and (precedes …) does — before is Allen's strict one, with a gap, and
precedes is the ordering that does not care whether the two touch, which is what
"1999 comes before 2000" means (docs/time.md).
Fields, not endpoints, answer an interval relation. The relation between two
calendar terms is fixed by their bounds, so relation classifies it directly rather
than routing through startOf / endOf and a constraint network — one comparison of
two six-field vectors against a network build. The endpoints stay answerable because
they are what joins this to the metric layer, not because anything here needs them.
Both ends bound, always. An open variable on either side of an instant ordering or
an interval relation would ask this to enumerate the calendar, which is not an answer
but a process that does not come back — so applicable? refuses it, exactly as the
point algebra's own prover answers nothing for a pair of open variables. The one
variable it binds is a startOf / endOf result, which is a function of the
interval and so exactly one term.
The clock behind the calendar constructors — where `(YearFn 2000)` stops being a name the interval algebra relates and starts being a **stretch between two moments**. `vaelii.impl.datetime` reads a calendar term to its fields and to the half-open `[start end]` it lies between; this namespace is the KB-facing half, one prover answering three families of goal out of that reading and storing nothing: (startOf (YearFn 2000) ?i) ?i = (InstantFn 2000 1 1 0 0 0) (endOf (YearFn 2000) ?i) ?i = (InstantFn 2001 1 1 0 0 0) (instantBefore (InstantFn 1999 6 1 0 0 0) (InstantFn 2000 1 1 0 0 0)) (during (MonthFn 2000 3) (YearFn 2000)) (meets (MonthFn 2000 2) (MonthFn 2000 3)) **Answered, never stored.** Nothing here mints a term, asserts a sentex or posts a justification, so a computed endpoint is not a belief, needs no retraction, and leaves no orphan for the NAT sweep to ask about (docs/nat.md). What it rests on is the calendar and the convention, both of which are in this code rather than in the store — which is why it implements `Prover` and not `SupportingProver`: there is no handle to name, and a prover that names none is one whose answer no retraction can invalidate (docs/inference.md, "What a computed answer rests on"). **Half-open, `[start, end)`.** A term's end is the first moment of the next term at the same precision, so the end of 1999 and the start of 2000 are the same term and consecutive calendar terms **meet**. `(before (YearFn 1999) (YearFn 2000))` therefore does *not* hold and `(precedes …)` does — before is Allen's strict one, with a gap, and `precedes` is the ordering that does not care whether the two touch, which is what "1999 comes before 2000" means (docs/time.md). **Fields, not endpoints, answer an interval relation.** The relation between two calendar terms is fixed by their bounds, so `relation` classifies it directly rather than routing through `startOf` / `endOf` and a constraint network — one comparison of two six-field vectors against a network build. The endpoints stay answerable because they are what joins this to the metric layer, not because anything here needs them. **Both ends bound, always.** An open variable on either side of an instant ordering or an interval relation would ask this to enumerate the calendar, which is not an answer but a process that does not come back — so `applicable?` refuses it, exactly as the point algebra's own prover answers nothing for a pair of open variables. The one variable it binds is a `startOf` / `endOf` **result**, which is a function of the interval and so exactly one term.
(calendar-prover)The calendar-clock prover, to register with vaelii.core/add-prover.
The calendar-clock prover, to register with `vaelii.core/add-prover`.
(relation a b)The Allen base relation between calendar terms a and b, read off their half-open
bounds — or nil when either is not a calendar term the clock can place.
The thirteen are jointly exhaustive and pairwise disjoint over any two intervals, so
this is a classification and not a search: four comparisons of six-field vectors decide
it. Two of the thirteen never come out of it — the calendar's terms are aligned, so
two of them nest, coincide, touch or are disjoint, and neither :overlaps nor
:overlapped-by can hold between a year, a month and a day. The arms are written
anyway, because they are what makes the classification total rather than a case
analysis that happens to cover its inputs.
The Allen base relation between calendar terms `a` and `b`, read off their half-open bounds — or nil when either is not a calendar term the clock can place. The thirteen are jointly exhaustive and pairwise disjoint over any two intervals, so this is a classification and not a search: four comparisons of six-field vectors decide it. Two of the thirteen never come out of it — the calendar's terms are **aligned**, so two of them nest, coincide, touch or are disjoint, and neither `:overlaps` nor `:overlapped-by` can hold between a year, a month and a day. The arms are written anyway, because they are what makes the classification total rather than a case analysis that happens to cover its inputs.
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 |