From: Drew McDermott ([email protected])
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