vaelii.impl.duration — com.vaelii/vaelii 0.1.0

Interval duration arithmetic — the quantitative half of vaelii.impl.interval, which is qualitative. Allen's algebra says that two intervals overlap; this says how long for, in real units, and adds up the lengths of several.

Two computed predicates, neither ever stored:

(totalDuration (list I1 I2 …) D) D is the sum of the components' lengths (overlapDuration I1 I2 D) D is how long I1 and I2 overlap

An interval's own duration is an ordinary stored fact, (length I M), whose measure M is a NAUT — (QuantityFn N Unit) or (QuantityIntervalFn Lo Hi Unit). The index answers those; this prover only reads them, normalizes each through provers/normalize-quantity against the KB's dimensionOf / conversionFactor table, does the arithmetic on [lo hi] magnitude bounds, and renders the result back as a measure.

Bounds throughout, not points. A stored length may itself be an interval measure, and an overlap is often only bounded rather than known, so every computation carries [lo hi] and the render decides the shape: lo and hi within tolerance give a point (QuantityFn …), anything wider gives (QuantityIntervalFn lo hi …). That is what keeps the answer honest — an over-approximation renders as an interval and says so, rather than as a point that would claim more than the KB knows.

The result is rendered in the dimension's base unit, which is read back out of the same conversionFactor table the normalization used — (conversionFactor U Base F) names the base, and a unit that declares no factor is its own base. So no separate declaration says which unit to render in, and none can disagree with the one the arithmetic actually happened in. Every unit of a dimension converts to a single base (the direct-to-base contract), so which component the base is read from cannot change the answer. A caller who wants another unit asks the check form instead — a ground D is compared after normalization, so (totalDuration (list A B) (QuantityFn 2.5 Hour)) is answered whatever unit the components were stated in.

Bind or check, like EvaluateProver: a variable D is bound to the rendered measure; a ground D succeeds iff it names the same dimension and the same bounds within provers/*quantity-tolerance*, the same epsilon policy the measure comparisons use. A magnitude is snapped to that same grid before rendering, so cross-unit normalization's last-bit noise never reaches the answer.

The metric network sharpens an overlap when there is one. The qualitative relation set alone cannot say how much of a partial overlap is shared, so it falls back to the sound [0, min(len1, len2)]. When vaelii.impl.stp has numeric bounds on both intervals' endpoints it computes a real one instead, and the two are intersected: both are sound, so the tighter of them is. A KB stating no temporalDistance gets exactly the qualitative answer, unchanged.

The prover is opt-in — register it with vaelii.core/add-prover. It needs no other prover registered: overlapDuration reads the qualitative relation set straight off interval/possible-allen-relations and the metric bound straight off stp/overlap-window, both functions of the believed facts rather than queries. See docs/duration.md.

duration-prover clj

(duration-prover)

The interval-duration arithmetic prover, to register with vaelii.core/add-prover.

overlap-bounds clj

(overlap-bounds rels [lo1 hi1] [lo2 hi2])

How long two intervals overlap, given the Allen relations still possible between them and each one's own [lo hi] length. Four cases, and the qualitative vocabulary of vaelii.impl.interval names three of them, so the two cannot drift apart:

• temporallyDisjoint — every possible relation puts them apart, so the overlap is exactly zero.
• subintervalOf — every possible relation puts the first inside the second, so the overlap is the whole of the first.
• hasSubinterval — the mirror.
• otherwise the sound over-approximation [0, min(len1, len2)]: they may not overlap at all, and can overlap by no more than the shorter of them. This is what an unconstrained pair gets, and it renders as an interval rather than a point, so the answer says how little is known instead of claiming a figure.

Nil for an empty relation set — that is an inconsistent network, which is not a pair of intervals whose overlap has a length.