[ontolog-forum] A basic time points/intervals ontology

[Pat Hayes <phayes@xxxxxxx>]

This is the a simple basic time ontology with a few possible extensions, adapted from my old 'catalog', modified and simplified and transcribed into CL from KIF. It might give us something more concrete to discuss.

Intuitions

The basic notions are timeinterval, timepoint and duration.

Durations form a group under addition (operator ++ with identity zero), can be multiplied by integers, and are ordered by >. They are measures of amounts of time, like 20 seconds or three years.

A timeinterval is a particular chunk of time, such as from 3 to 5 pm GMT on 25 December 2007. Note, a timeinterval need not be an interval in the conventional mathematical sense, i.e. a set of real numbers.

Timepoints are the places where timeintervals meet, and which they have at their ends. (It turns out that these two ways of defining points are interconvertible, so we might as well use both.) Timepoints have zero duration, and are totally ordered by before.

Order

(forall (x y z)(and

   (if (and (before x y)(before y z))(before x z))

   (if (before x y)(not (before y x)))

))

Timeintervals have exactly two associated timepoints, one at each end, called the begin and end of the interval. A meets B when the end of A is the same as the begin of B. Two timepoints x and y with x before y define a unique interval from them. There are some obvious identities:

BEF

(forall (x y i)(and

   (= x (begin (from x y)))

   (= y (end (from x y)))

   (= i (from (begin i)(end i)))

))

Its easy to define the Allen relations by conjunctions of conditions on the ordering of the endpoints. For completeness, these are their definitions:

Allen

(forall ((i timeinterval)(j timeinterval))(and

   (iff (before i j)(before (end i)(begin j)))

   (iff (meets i j)(= (end i)(begin j)))

   (iff (overlaps i j)(and (before (begin i)(begin j))

                   (before (begin j)(end i))

                   (before (end i)(end j))

                  ))

   (iff (starts i j)(and (= (begin i)(begin j))(before (end i)(end j)) ))

   (iff (inside i j)(and (before (begin j)(begin i))(before (end i)(end j)) ))

   (iff (ends i j)(and (before (begin i)(begin j))(= (end i)(end j)) ))

))

plus their inverses (permute the arguments) and equality, makes 13.

Its useful to extend inside to also apply between a point and an interval:

Inside

(forall (p (i timeinterval))(iff (inside p i)

                                        (and (before (begin i) p)(before p (end i)) )

))

There are three basic assumptions about duration:

BD1

(forall (p q)(iff (before p q)(> (duration (from p q)) zero) ))

BD2

(forall ((p timepoint)(= (duration p) zero) )

BD3

(forall (p q r)(if (= (duration (from p q))(duration (from p r))) (= q r) ))

Note, BD3 rules out branching futures. The ordering assumptions rule out  circular models of time. However, this theory so far is seriously agnostic:

= time can be dense or discrete or continuous (or indeed any combination of these, or something else entirely)

= time can be finite or infinite, in either direction

= points can be distinct from intervals, or not

= a timeinterval can be identified with a set of points, or not; and if it is, it can be an open or a closed or a clopen set.

-----------

First extension: clocks

A clock is a set of intervals called ticks, each meeting the next and all having the same duration, called the period of the clock. (This is a simple clock which has no provision for leap seconds and other exotica, or for having its rate re-set. Those can be modelled as sequences of simple clocks.) The time of a point according to a clock is the number of ticks in the set which end at or before the point. As the logic provides no way to speak of numbers of points in a sequence or a set, we will assume that there is a tick function from the clock and natural numbers to ticks which gives the clock time directly, so that (tick c n) is the n-th tick of c. (This description takes the natural numbers and simple operations on them - in particular, addition - for granted, which we will do from now on without further comment. In practice, of course, we mean the elements of any some model of the arithmetic axioms which are in use. Number is true of all and only the natural numbers.)

Notation: (tick c) is a predicate true of all ticks of the clock c, and (time c) is the function from timepoints to clock times according to the clock c.

CLOCK

(forall ((c Clock))(and

    (forall (x)(iff ((tick c) x)(exists ((n Number))(= x (tick c n))) ))

    (forall (x)(if ((tick c) x) (= (duration x)(period c)) ))

    (forall ((n Number))(meets (tick c n)(tick c (+ n 1))

    (forall ((p timepoint) n)(iff

         (= ((time c) p) n)(or (= p (end(tick c n)))

                                       (inside p (tick c (plus n 1))) )) ))

))

Given this, things like changes of the base time of a clock, or conversions of one clock to another, are left as exercises for the reader :-)

Clock times which are more structured than simple integers, such as hours/minutes/seconds, can usually be viewed as alternative notations for integers, e.g. on a 24hour 1-second period clock which repeats each day, H:M:S is a notation for (3600*H)+(60*M)+S. Notice that according to the above, such a clock is replaced at midnight by a new clock. A repeating clock is a clock (eg a day count from Jan 1) with every tick (eg a day) itself inhabited by a clock, so that the begin of tick one of the inner clock is the begin of this tick of the outer clock.

This whole scheme works well for days and smaller intervals, and for years and longer intervals, but it does not work for months. Months are a royal PITA. In the time catalog I invented one way to handle them, but I think the way that Jerry Hobbs handles them in the DAML/OWL-time ontology is better: his 'hath' function (as in '30 days hath September'.) Using this, one can treat each month as a [day-tick/second-click] repeating clock.

As the above illustrates, these basic time axioms are sufficient to define and derive the basic properties of quite a lot of 'temporal' phenomena in everyday life. However, they can be extended in various ways to conform to various intuitions about the basic structure of the time-line.

---------

One whole class of extensions turn on the notion of a 'moment', by which I mean an interval which is not a point, but is a smallest possible interval, i.e. it has no points inside it, only endpoints.

Moment

(forall ((i timeinterval))(iff (moment i)(forall ((p timepoint))(not (inside p i))) ))

The first question is, do such things exist? You can have it either way.

Case 1a: Discrete time: every timepoint is the meeting point of two intervals:

DISCRETE

(forall ((p timepoint))(exists ((i moment)(j moment))(= p (end i)(begin j)) ))

Case 1b: Dense time: Intervals are impossible (so between any two points there is a third):

DENSE

(forall ((p timepoint)(q timepoint))(if (before p q)

        (exists ((r timepoint))(and (before p r)(before r q)))

))

from which it follows that

Theorem

(forall ((i timeinterval))(not (moment i)))

(Note, to specify the real line one would have to use higher-order logic and define limits.)

These two cases are not exhaustive. One can for example allow moments to exist but only 'sparsely', so that two moments can never meet:

Case 1c:

AH1

(forall ((i moment)(j moment))(not (meets i j)) )

This allows one to treat these isolated moments as being rather like points: they are a kind of 'fat point' which can be thought of as intervals of 'infinitesimal' duration. Other models are also possible, but lets leave this topic for now.

---------

One problem with the axiom BEF is that since all intervals must have endpoints, it seems that semi-infinite intervals are impossible, and if time is infinite then the entire timeline is not an interval. If this is an issue, we can extend the theory by adding two special 'points at infinity'. (This is a very old mathematical trick, of course, and is quite safe.) We have to allow an infinite duration to go along with these, and extend the arithmetic of durations to include this infinite value. We call these BOT and EOT (begin of time and end of time). Note, we do not classify these as timepoints: this keeps the axioms simpler; and the values of the from function applied to either of these arguments is not classified as a timeinterval. Similarly, we introduce the special duration value FOREVER.

INF1

(forall ((p timepoint))(and (before BOT p)(before p EOT)))

INF2

(forall ((p timepoint))(and (= FOREVER (duration (from BOT p)))

                                      (= FOREVER (duration (from p EOT)))

                                      (= FOREVER (duration (BOT EOT)))

))

FOREV

(forall ((i timeinterval)(n number))(and

       (> FOREVER (duration i))

       (= FOREVER (++ FOREVER (duration i)))

       (= FOREVER (* n FOREVER))

))

----------

Up to now the theory makes a clear distinction between points and intervals; but if preferred, we can treat points as a special kind of interval, the result of applying from to the same point twice, so that p = (from p p) for any point p:

IP1

(forall ((p timepoint))(and (timeinterval p)(= p (from p p)) ))

This is consistent with all the earlier options, though it does have some apparently odd consequences. Points meet themselves, for example: indeed, this can be used as the definition of a point:

Theorem:

(forall ((i timeinterval)(iff (timepoint i)(meets i i)))

Also, any point is a moment; but not necessarily vice versa. The discrete timeline, for example, is now a totally ordered series of meeting timeintervals which are all moments, but only every other one is a timepoint.

This means also that the usual relationships between the Allen relations is disturbed somewhat: normally for example it is assumed that if i meets j meets k, then i cannot meet k: but now, if j is a point, then i does meet k. Reasoners which use the standard Allen composition algebra therefore have to be reconsidered with this option (or else restricted to non-point intervals, which is probably the most sensible option.)

--------

Allowing points to be intervals amounts to treating (from p q) as meaningful both when p is before q and when p=q. We can go the extra step of treating it as meaningful when q is before p. What could (from p q) mean when p is after q?  It seems to be a 'backward-pointing interval', whose end is earlier than its begin. Although this might seem a rather unintuitive kind of object, it does make sense. Its the 'interval' one gets when some event is earlier than expected and one is using an interval to represent the amount by which something is late; or when it is late, and one is using an interval to measure how early it is. It is the interval after the start gun that someone begins to run when they in fact start prematurely; and so on.

All that is needed to make this picture coherent is to allow such backward intervals to have a negative duration:

V1

(forall ((p timepoint)(q timepoint))(=

   (++ (duration (from p q))(duration (from q p)))

   zero

))

Now the function from is a total function on any pair of points whatsoever: given any two points, without qualification as to their ordering, there is a unique interval going from one of them to another. It has zero duration iff they are the same point; it has positive duration iff the first is before the second; and negative duration iff the second is before the first.

We can now do full arithmetic on durations, and have complete expressive power to conclude, for example, that given any sequence p1,...pn of points, the duration of  the interval (from p1 pn) is the sum of the durations of the intervals (from p1 p2), (from p2 p3)...(from pn-1 pn). In general, allowing 'backward' intervals has the same advantages in temporal reasoning that the invention of negative numbers had on the ability to do arithmetic. For example, a clock which is running fast mis-states all its times by a negative duration.

---------

OK, maybe this will give us something concrete to discuss.

Pat

-- 

---------------------------------------------------------------------
IHMC               (850)434 8903 or (650)494 3973   home
40 South Alcaniz St.       (850)202 4416   office
Pensacola                 (850)202 4440   fax
FL 32502                     (850)291 0667    cell
phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (01)