From: Drew McDermott (drew.mcdermott@yale.edu)
Date: 10/29/02
Now that Jerry and Pat have observed that *PosInf* and *NegInf*
_could_ be bounds on infinite time intervals, even in branching time,
my other question on (beginning-of i) and (end-of i) has an obvious
answer. So I propose we leave them functions, and _not_ make them
into relations as Jerry proposes.
[me]
> The axioms in daml-infinite-linear-time imply that
> (before *PosInf* *PosInf*).
[Jerry]
I guess I don't see this. How does it follow?
Axiom 2.4-3 states:
(forall (t1 - Instant)
(exists (t2 - Instant)
(and (before t1 t2) (before t2 *PosInf*))))
If we take t1 to be *PosInf*, then there is a t2 such that
(before *PosInf* t2) and (before t2 *PosInf*). From this it follows
that (before *PosInf* *PosInf*).
The obvious fix is to change it to
(forall (t1 - Instant)
(if (not (= t1 *PosInf*))
(exists (t2 - Instant)
(and (before t1 t2) (before t2 *PosInf*)))))
A similar edit is required for axiom 2.4-5.
[Jerry]
On *dayofweek* it would be possible to define the predicate
"dayofweek" as follows:
dayofweek(y,n,x) <--> (E n1,x1)[wk(x,n1,x1) & cal-int(y,n,*Day*,x)
That is, y is the nth day of the week of x if and only if x is the
n1-th week in some interval x1 (i.e., x is a calendar week), and y is
the nth day of x. This would replace axioms 4.3-3 and 4.3-4, and
would necessitate no changes in the definitions of Sunday, Monday,
etc.
I think we have to go a bit further than that. Right now it's
understood, but not stated explicitly, that 'wk' is true only of an
"official" week, not an arbitrary 7-day period. I'm not sure how to
state that a week is official, except to figure out what day of the
week January 1, 0001 was. (Someone must have done this!)
The expression "the first Monday in October" is a little more
complicated and has to do with temporal sequences. It really means
"the first second-day-of-a-calendar-week in October". The word
"first" does not mean n = 1 in any predication "dayofweek(y,n,x)". It
refers to an element in the sequence constructed by letting n = 2.
Something like the z such that
eltof(z,1,seq(d | dayofweek(d,2,w) & in(d,m) & October(m,y)))
You just need an existential quantifier to the right of '|' to bind 'w'
and 'm'. 'y' is presumably a free variable here.
[Jerry]
As the expert in branching futures, how would you feel about ....?
Well, speaking as the expert in branching futures, the current
ontology is a bit incoherent. It is mostly concerned with time
_measurement_. From that point of view it would be meaningless to
talk of branching time, because even if you think there are multiple
versions of next week, they presumably all start Wednesday at the same
"date."
The only place where the ontology connects to actual events is in
section 2.5, where the 'holds' predicate is introduced. But the
treatment there is sketchy. For instance, we have the following:
during(e,T) & inside(t,T) --> at-time(e,t)
Intuitively, this would be true only if 'e' is some kind of
proposition, such as "The cat is on the mat." If 'e' is "Sir Fred
bowing three times to Queen Sally," in what sense does that hold at
every instant of an interval over which it occurs? Well, one can
craft one's ontology any way one wants, but in branching time there is
a real problem. Suppose that in one branch, after the first bow Sir
Frank rushes in and knocks Sir Fred to the floor. In another, Frank
is a little late and Fred completes his three bows. Now pick a time
instant in the middle of the first bow. By the axiom above Fred is
bowing three times at that instant, even though in some futures he
never gets to bow 2.
I think it would be cleaner to separate time measurement from events
and other eventualities. The axioms can all stay the same, but we
drop the idea that a time instant is a situation in the McCarthy-Hayes
sense. Instead, we would have a function
(sit-at ti pw)
which denotes the situation that obtains at time 'ti' in the possible
world 'pw'. (If you would rather avoid time instants altogether, you
can also map an interval to a situation sequence or history or
something; I will leave that to others.) Then you set up
relationships among various possible worlds in the usual ways. Then
you make 'holds' a predicate on situations (or histories, mutatis
mutandis). Branching time is the case where if pw1 is an alternative
to pw2, then they share a prefix and nothing thereafter.
-- Drew
This archive was generated by hypermail 2.1.4 : 10/29/02 EST