Further remarks

From: Drew McDermott (drew.mcdermott@yale.edu)
Date: 10/29/02

  • Next message: Drew McDermott: "Revised daml-time.pddl"
    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.
       > The axioms in daml-infinite-linear-time imply that 
       >  (before *PosInf* *PosInf*).  
       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.
       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,
    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.
       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
    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