Issue 16689: D0 Should be Quantified (date-time-ftf)
Source: International Business Machines (Mr. Mark H. Linehan, mlinehan(at)us.ibm.com)
Nature: Uncategorized Issue
Severity: 
Summary: Clause 7.2.2 has several CLIF axioms that reference 'D0' but fail to quantify that variable.  They should each existentially quantify 'D0'.
Resolution: 
Revised Text: 
Actions taken:
November 17, 2011: received issue
Discussion: 

End of Annotations:=====
sposition: ???
	OMG Issue No:  16689 
Title:	D0 Should be Quantified
Source:
Mark H. Linehan . IBM . mlinehan@us.ibm.com

Summary:
Clause 7.2.2 has several CLIF axioms that reference 'D0' but fail to quantify that variable.  They should each existentially quantify 'D0'.

Resolution:  
Revised Text: 
Disposition:	???

Date: Mon, 16 Jul 2012 19:21:07 -0400
From: Ed Barkmeyer <edbark@nist.gov>
Reply-To: <edbark@nist.gov>
Organization: NIST
User-Agent: Thunderbird 2.0.0.23 (Windows/20090812)
To: OMG DateTimeVoc FTF <date-time-ftf@omg.org>
Subject: DTV Issues 16689, 16951, 17367 proposed resolutions
X-NISTMEL-MailScanner-Information: Please contact postmaster@mel.nist.gov for more information
X-NISTMEL-MailScanner-ID: q6GNLC0g026153
X-NISTMEL-MailScanner: Found to be clean
X-NISTMEL-MailScanner-SpamCheck: 
X-NISTMEL-MailScanner-From: edbark@nist.gov
X-NISTMEL-MailScanner-Watermark: 1343085673.55422@IEaF9gf9d6nkQdYdT6Y+Ag
X-Spam-Status: No


Per today's conference call, I attach the revised drafts for resolution of Issues
16689 - D0 should be quantified (added the UML object D0)
16951 - time point subdivision (see markup),
17367- no smallest time interval (1st draft, needs OCL)


For 16689, should we have defined a term like 'zero duration'?  Should that be the term and D0 the Synonym?


-Ed


-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800







 DTV Issue 17367- no smallest time interval-d1.docx 


 DTV Issue 16689-D0 should be quantified1.docx 


 DTV Issue 16951-time point subdivision-d4.doc 




Disposition: Resolved
OMG Issue No:  16689
Title:	D0 Should be Quantified
Source:  Mark H. Linehan . IBM . mlinehan@us.ibm.com

Summary:
Clause 8.2.2 has several CLIF axioms that reference 'D0' but fail to quantify that variable.  They should each existentially quantify 'D0'.

Resolution:
In 8.2.2, D0 is declared to be an individual concept . a logical constant . under Axiom V.4.  The problem is that there is no CLIF rendition of this axiom, and there needs to be a theorem that D0 is unique.
In resolving this issue, the FTF noted that the CLIF .plus. operator must be defined between durations, because it is not the same as the .plus. operator for numbers.  And the closure axiom does not follow from the definition.

Revised Text:
1.  In clause 8.2.2, REPLACE Figure 8-11 with:

2.  In clause 8.2.2, in the entry for .duration3 = duration1 + duration2., DELETE the Note that reads:
Note:	Axiom V.1 (Addition is closed) is incorporated into this verb concept by definition.
and INSERT:
Note:	The following definition defines the CLIF duration addition function; the verb concept is primitive and has no definition.
CLIF Definition:	(forall ((d1 duration) (d2 duration) d3)
  (iff
    (= d3 (+ d1 d2))
    (and
      (duration d3)
      ("duration3 = duration1 + duration2"
         d3 d1 d2) )))
Axiom V.1 (Addition is closed): For all durations d1 and d2, there is a duration d3 such that d3 = d1 + d2.
CLIF Axiom:	(forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
3.  In clause 8.2.2, in Axiom V.4, in the entry for D0, after the Definition, INSERT:
CLIF Definition:	(exists D0 (and
  (duration D0)
  (forall (d duration)
    (= (+ d D0) d)) ))
Note:	D0 is a duration that is the additive identity, and it is unique.  The uniqueness of D0 follows from the definition and the commutative axiom (V.3):  If there is some other Dx such that 
d + Dx = d for all durations d, then D0 + Dx = D0, but 
D0 + Dx = Dx + D0 and Dx + D0 = Dx, by definition of D0.

Disposition:	Resolved

To: date-time-ftf@omg.org
Subject: Re: DTV Issues 16689, 16951, 17367 proposed resolutions
X-KeepSent: 3B603CE5:20605F92-85257A42:0030F06E;
 type=4; name=$KeepSent
X-Mailer: Lotus Notes Release 8.5.3 September 15, 2011
From: Mark H Linehan <mlinehan@us.ibm.com>
Date: Wed, 25 Jul 2012 22:55:07 -0400
X-MIMETrack: Serialize by Router on D01MC604/01/M/IBM(Release 8.5.3 ZX853HP5|January 12, 2012) at
 07/25/2012 22:55:09,
        Serialize complete at 07/25/2012 22:55:09
X-Content-Scanned: Fidelis XPS MAILER
x-cbid: 12072602-8974-0000-0000-00000B7F6E3E


Regarding 16689: 
* I don't see the value of this CLIF axiom; it doesn't seem to say anything.  The one proposed to go after axiom V1 seems sufficient. 
CLIF Definition:        (forall ((d1 duration) (d2 duration) d3)
 (iff
   (= d3 (+ d1 d2))
   (and
     (duration d3)
     ("duration3 = duration1 + duration2"
        d3 d1 d2) ))) 
* I don't have a strong opinion about 'D0' versus 'zero duration'.  I don't see a lot of value in using the term 'zero duration' instead of 'D0'. 

Regarding 16951: 
* Editorial instruction #2 should make it clear that the new subsection has a regular section number, not the literal "9.4bis".  Something like "Immediately before clause 9.5, create a new subclause:", and renumber subclauses 9.5 and 9.6 as 9.6 and 9.7".  And then show "9.4bis" as "9.4". 
* I notice that all the uses of the 'subdivides' verb concept are of the form "<finite time scale> subdivides <time point> into <number> of <time point>".  Which makes me wonder whether the verb concept should have 4 roles rather than 2. 
* There should be a Note that explains why we talk about a subsequence of the finite time scale.  The reason is that the subdivision of some kinds of time points into finite time scales is irregular.  Months are subdivided into 28-31 days and years are subdivided into 365 or 366 days. 
* But, looking further, all of the uses of this verb concept talk about subdividing the "larger" time point into a fixed (not varying) number of "smaller" time points.  For example, the 'Gregorian year of days scale' is defined as "the finite time scale that subdivides âGregorian yearâ into 366 of âGregorian day of yearâ ".  Should it talk about subdividing leap years into 366 and common years into 365 'Gregorian day of year'?  Should the 'Gregorian month of days scale' be explicit about how it divides each of the Gregorian months?  What do we do about the 'year of weeks scale' since the number of weeks in a year is really messy? 
* The wording of the Necessity seems like something a logician would write not something that makes business sense.  The phrase "If a finite time scale subdivides a time point," should not be needed since the Necessity is in the context of this verb concept.  (In any case, this Necessity will be rewritten if my point about missing roles is accepted.) 
* I agree that this verb concept is related to 'time point converts to time point sequence on time scale' but I don't agree that this verb concept is a 'special case' of the latter.  This verb concept is about the definitional relationship between finite time scales and time points; whereas the other is about computing the conversion. 

Regarding 17367: 
* I think that the OCL for the new axiom in 8.1.1 should read, as follows -- but need to consult the OCL book when I get home to be sure: 
OCL Constraint:        context: "time interval" 
                                   inv: "time interval"."time interval1 is proper part of time interval2"-->notEmpty() 
* Why not wrap the new axiom in 8.1.6 into the definition of 'properly during'?  Why should it be a separate axiom? 
* I haven't provided the OCL for this new axiom because I think it instead should be a modification of the definitional OCL for 'properly during'. 
* I think that what Fabian asked for is a different new axiom that says that every time interval has a proper part that starts/finishes it. 
-------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        OMG DateTimeVoc FTF <date-time-ftf@omg.org>, 
Date:        07/16/2012 07:23 PM 
Subject:        DTV Issues 16689, 16951, 17367 proposed resolutions 

--------------------------------------------------------------------------------



Per today's conference call, I attach the revised drafts for resolution 
of Issues
16689 - D0 should be quantified (added the UML object D0)
16951 - time point subdivision (see markup),
17367- no smallest time interval (1st draft, needs OCL)

For 16689, should we have defined a term like 'zero duration'?  Should 
that be the term and D0 the Synonym?

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800



[attachment "DTV Issue 17367- no smallest time interval-d1.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16689-D0 should be quantified.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16951-time point subdivision-d4.doc" deleted by Mark H Linehan/Watson/IBM] 
Date: Thu, 26 Jul 2012 13:13:53 -0400
From: Ed Barkmeyer <edbark@nist.gov>
Reply-To: <edbark@nist.gov>
Organization: NIST
User-Agent: Thunderbird 2.0.0.23 (Windows/20090812)
To: Mark H Linehan <mlinehan@us.ibm.com>
CC: "date-time-ftf@omg.org" <date-time-ftf@omg.org>,
        Stan Hendryx
        <stan@hendryxassoc.com>
Subject: Re: DTV Issues 16689, 16951, 17367 proposed resolutions
X-NISTMEL-MailScanner-Information: Please contact postmaster@mel.nist.gov for more information
X-NISTMEL-MailScanner-ID: q6QHDxWQ020586
X-NISTMEL-MailScanner: Found to be clean
X-NISTMEL-MailScanner-SpamCheck: 
X-NISTMEL-MailScanner-From: edbark@nist.gov
X-NISTMEL-MailScanner-Watermark: 1343927645.10142@6DsG5WLPb8zkZQWdoGtwZA
X-Spam-Status: No




Mark H Linehan wrote: 
Regarding 16689: 
* I don't see the value of this CLIF axiom; it doesn't seem to say anything.  The one proposed to go after axiom V1 seems sufficient. 
CLIF Definition:        (forall ((d1 duration) (d2 duration) d3)
 (iff
   (= d3 (+ d1 d2))
   (and
     (duration d3)
     ("duration3 = duration1 + duration2"
        d3 d1 d2) ))) 


This axiom defines the function (+ d1 d2).  Otherwise it is primitive, and not clearly related to the predicate "duration3 = duration1 + duration2".  Or at least, I think that is the case.  The proposed axiom for V1 says that the function is defined everywhere:
(forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
  
* I don't have a strong opinion about 'D0' versus 'zero duration'.  I don't see a lot of value in using the term 'zero duration' instead of 'D0'. 

In SBVR parlance, D0 is a symbol, 'zero duration' is a term.  Given that it is a term for something that is strictly a mathematical concept, it probably makes no difference.


Regarding 16951: 
* Editorial instruction #2 should make it clear that the new subsection has a regular section number, not the literal "9.4bis".  Something like "Immediately before clause 9.5, create a new subclause:", and renumber subclauses 9.5 and 9.6 as 9.6 and 9.7".  And then show "9.4bis" as "9.4". 


OK.


* I notice that all the uses of the 'subdivides' verb concept are of the form "<finite time scale> subdivides <time point> into <number> of <time point>".  Which makes me wonder whether the verb concept should have 4 roles rather than 2. 


Hmm.  I think the original verb was based on the idea that the subdivision was like hours and minutes -- the whole finite time scale.  But of course that was never true for month-of-days or year-of-days.  The subdivision really uses a time point sequence beginning with the origin index, which is what the proposed revised definition says.  But that 'time point sequence' idea may be wrong.  That is, I think a time point sequence is different from a sequence of time points, and 'subdivides' is about that difference.

Technically a sequence of time points corresponds to sequences of time intervals.  We say a 'time point sequence' corresponds to the one big interval that is the span (hull) of the sequence of intervals.  Now the 'one big interval' view is consistent with the idea that '2:00 to 4:00' indicates a time point sequence that corresponds to intervals that have a duration of two hours (or correctly 120 minutes).  But that is not what we mean by 'subdivides',  We mean treating the larger time point as a sequence of time points that corresponds to sequences of smaller time intervals, rather than to the hull of them.  This leads me to think that the term 'time point sequence' violates (Bernd Wenzel's) Law of Least Astonishment.  That is 'time point sequence' is not the same as 'sequence of time points'.


* There should be a Note that explains why we talk about a subsequence of the finite time scale.  The reason is that the subdivision of some kinds of time points into finite time scales is irregular.  Months are subdivided into 28-31 days and years are subdivided into 365 or 366 days. 


Agree.


* But, looking further, all of the uses of this verb concept talk about subdividing the "larger" time point into a fixed (not varying) number of "smaller" time points.  For example, the 'Gregorian year of days scale' is defined as "the finite time scale that subdivides .Gregorian year. into 366 of .Gregorian day of year. ".  Should it talk about subdividing leap years into 366 and common years into 365 'Gregorian day of year'?  Should the 'Gregorian month of days scale' be explicit about how it divides each of the Gregorian months?  What do we do about the 'year of weeks scale' since the number of weeks in a year is really messy? 


I guess we need to discuss this.  I agree with Mark's concern here, but I don't know what we want to write.  And <expletive deleted> leap seconds make minute-of-seconds or day-of-seconds truly variable.  


* The wording of the Necessity seems like something a logician would write not something that makes business sense.  The phrase "If a finite time scale subdivides a time point," should not be needed since the Necessity is in the context of this verb concept.  (In any case, this Necessity will be rewritten if my point about missing roles is accepted.) 


Yes.  This is part of the above.


* I agree that this verb concept is related to 'time point converts to time point sequence on time scale' but I don't agree that this verb concept is a 'special case' of the latter.  This verb concept is about the definitional relationship between finite time scales and time points; whereas the other is about computing the conversion. 


The Beta text of this verb concept is broken.  The replacement text from Issue 17227 says:

<!--[if !supportLists]-->Definition:                             <!--[endif]-->the time point is coextensive with the time point sequence

<!--[if !supportLists]-->Necessity:                              <!--[endif]-->Each time point of the time point sequence is on the time scale.

<!--[if !supportLists]-->Possibility:                             <!--[endif]-->The time point is an absolute time point or is a relative time point.

<!--[if !supportLists]-->Description:                          <!--[endif]-->The time point and the time point sequence are two different ways to identify the same time intervals.


It doesn't say anything about computation.  The purpose is to provide meaning to the idea of computing the referents of a time coordinate, yes.  The Beta text indicated that intent -- it was trying to say that the decomposition into time points was about identifying time periods.  But the mechanism is said here to involve the conversion to an equivalent sequence of time points.  The example for 17227:


<!--[if !supportLists]-->Example:                                 <!--[endif]-->The time point that is indicated by the time coordinate January 2012 converts to the time point sequence 2012 day 1 through 2012 day 31 on the Gregorian days scale.


shows that the intent is different from 'subdivides'.  'subdivides' is about converting January 2012 to the month-of-days; this is about converting it to a subsequence of 'day-of-year'.

But this takes us back to the idea above, that there are two different time point sequence ideas.  I think the 'converts to' idea is about locating the larger interval in a longer sequence of finer granularity intervals, as the large interval that is the hull of a subsequence, while 'subdivides' is about treating the larger time point as a sequence of consecutive time points that corresponds to sequences of consecutive smaller time intervals.  That is, 'converts to' is not about decomposing the time point and its corresponding time periods, it is about locating it in some other sequence; but subdivides is about decomposing the time point and its corresponding time periods.  

So I agree with Mark that 'subdivides' is not a special case of 'converts to', but we somehow have to be clear about the difference in intent in the definitions.  They both seem to say:  "time point on scale A is coextensive with time point sequence on scale B."  17227 is correct that that is what converts to means.  For 'subdivides' we have to talk about sequences of time intervals, somehow.


Regarding 17367: 
* I think that the OCL for the new axiom in 8.1.1 should read, as follows -- but need to consult the OCL book when I get home to be sure: 
OCL Constraint:        context: "time interval" 
                                   inv: "time interval"."time interval1 is proper part of time interval2"-->notEmpty() 


OK.  I will put that in the next draft, with a comment that says 'check this'.


* Why not wrap the new axiom in 8.1.6 into the definition of 'properly during'?  Why should it be a separate axiom? 
* I haven't provided the OCL for this new axiom because I think it instead should be a modification of the definitional OCL for 'properly during'. 


Well, 'properly during' is one of the Allen relations, and it is defined in terms of 'part of ' and 'before'.  'properly during' just says there is a proper part that is before it and one that is after it, which logically completes the partitioning of 'proper part': starts has no before, finishes has no after, and during has both.  What Mark suggests is that 'A is properly during B' could be defined as:  A is a proper part of B and there is a time interval C such that C starts B and C meets A, etc.  That does not clearly complete the partition.  To complete it, you would have to prove that:  If A does not start or finish B, then there is a C that starts B and meets A.   That is, if there is a C that is a proper part of B and is before A (i.e. A does not start B), then there is a C' that starts B and meets A.  And that is what the proposed axiom says, because you can't prove it from the other axioms.

In a similar way, the weak supplementation axiom says that for every proper part there is another proper part that does not overlap it.  So if A starts B, A has a supplement and the supplement must be after A.  But there is a 'start complement' axiom that says that if A starts B, there is a C that is met by A and finishes B -- the "maximal" supplement.  I don't think you can get these "maximal supplement" theorems from the axioms for 'part of' and 'before', precisely because we don't have strong supplementation:  If A is properly during B, then B-A is not a time interval.


* I think that what Fabian asked for is a different new axiom that says that every time interval has a proper part that starts/finishes it. 


Ah!  But those follow from the proposed axiom, together with the existing start-complement and finish-complement axioms.  E.g.
Theorem:  Every time interval has a proper part that starts it.
Proof:
If a time interval B has a proper part A, then (by the Allen partitioning), one of the following must be true: A starts B, A finishes B, A is properly during B.
Now, if A starts B, B has a proper part (A) that starts it.
If A finishes B, by the finish complement axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
If A is during B, by the proposed axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
So, if a time interval B has a proper part A, B has a proper part that starts B in all cases.  
By the no-smallest-interval axiom, every time interval B has some proper part A.  
So every time interval B has a proper part that starts B in all cases.  Q.E.D.
 
The nagging question is whether there might be a simpler solution than having these three complement axioms.  In particular, could we instead assert that every time interval has a proper part that starts it and a proper part that finishes it?  I think not, because there is no basis for relating an arbitrary starting part to an arbitrary finishing part.

-Ed


-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800

"The opinions expressed above do not reflect consensus of NIST, 
 and have not been reviewed by any Government authority."




-------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        OMG DateTimeVoc FTF <date-time-ftf@omg.org>, 
Date:        07/16/2012 07:23 PM 
Subject:        DTV Issues 16689, 16951, 17367 proposed resolutions 

--------------------------------------------------------------------------------



Per today's conference call, I attach the revised drafts for resolution 
of Issues
16689 - D0 should be quantified (added the UML object D0)
16951 - time point subdivision (see markup),
17367- no smallest time interval (1st draft, needs OCL)

For 16689, should we have defined a term like 'zero duration'?  Should 
that be the term and D0 the Synonym?

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800



[attachment "DTV Issue 17367- no smallest time interval-d1.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16689-D0 should be quantified.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16951-time point subdivision-d4.doc" deleted by Mark H Linehan/Watson/IBM] 


To: "date-time-ftf@omg.org" <date-time-ftf@omg.org>,
        Stan Hendryx <stan@hendryxassoc.com>
Subject: Re: DTV Issues 16689, 16951, 17367 proposed resolutions
X-KeepSent: 32C99A50:8D6694E3-85257A48:0010747B;
 type=4; name=$KeepSent
X-Mailer: Lotus Notes Release 8.5.3 September 15, 2011
From: Mark H Linehan <mlinehan@us.ibm.com>
Date: Thu, 26 Jul 2012 23:42:28 -0400
X-MIMETrack: Serialize by Router on D01MC604/01/M/IBM(Release 8.5.3 ZX853HP5|January 12, 2012) at
 07/26/2012 23:42:29,
        Serialize complete at 07/26/2012 23:42:29
X-Content-Scanned: Fidelis XPS MAILER
x-cbid: 12072703-9360-0000-0000-000008D0F9BE


Ed, 

Regarding 16689:  Why isn't the  function (+ d1 d2) just a noun form of the predicate "duration3 = duration1 + duration2"? 

Regarding 16951:  I don't think we need to distinguish "time point sequence" from "sequence of time points".  I think these are just two views of the same thing: either the time interval that corresponds to the convex hull of the whole time point sequence, or a sequence of time intervals that correspond to the individual time points of the time point sequence.  I think the two verb concepts ('subdivides' and 'converts to') are two different ways of using the one general concept. 

Regarding how to define the time scales that irregularly subdivide time points, here's an example of what I suggest we should write: 

"Gregorian year of days scale: the finite time scale that subdivides âcommon yearâ into 365 of âGregorian day of yearâ and that subdivides 'leap year' into 366 of âGregorian day of yearâ. 

I don't think leap seconds have anything to do with this discussion.  Leap seconds involve displacing the UTC time scale, not adding seconds to calendar days.  BIPM is clear that 'day' is fixed at 86400 seconds. 

Regarding 17367: OK on adding the new axiom.  Here's the OCL, I think: 

OCL Definition:        context "time interval" 
                        inv: "time interval".allInstances-->forAll(t2 | 
                                       t2."is properly during"(self) 
                                                   implies "time interval".allInstances-->exists(t3 | 
                                                        t3.starts(self) and t3.meets(t2))) 
                        context "time interval" 
                        inv: "time interval".allInstances-->forAll(t2 | 
                                       t2." is properly during"(self) 
                                                   implies "time interval".allInstances-->exists(t3 | 
                                                        t3.ends(self) and t2.meets(t3))) 

I think we should make explicit the new axiom requested by Fabian. 
--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        Mark H Linehan/Watson/IBM@IBMUS, 
Cc:        "date-time-ftf@omg.org" <date-time-ftf@omg.org>, Stan Hendryx <stan@hendryxassoc.com> 
Date:        07/26/2012 01:19 PM 
Subject:        Re: DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------





Mark H Linehan wrote: 
Regarding 16689: 
* I don't see the value of this CLIF axiom; it doesn't seem to say anything.  The one proposed to go after axiom V1 seems sufficient. 
CLIF Definition:        (forall ((d1 duration) (d2 duration) d3)
 (iff
   (= d3 (+ d1 d2))
   (and
     (duration d3)
     ("duration3 = duration1 + duration2"
        d3 d1 d2) ))) 

This axiom defines the function (+ d1 d2).  Otherwise it is primitive, and not clearly related to the predicate "duration3 = duration1 + duration2".  Or at least, I think that is the case.  The proposed axiom for V1 says that the function is defined everywhere:
(forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
  
* I don't have a strong opinion about 'D0' versus 'zero duration'.  I don't see a lot of value in using the term 'zero duration' instead of 'D0'. 

In SBVR parlance, D0 is a symbol, 'zero duration' is a term.  Given that it is a term for something that is strictly a mathematical concept, it probably makes no difference.

Regarding 16951: 
* Editorial instruction #2 should make it clear that the new subsection has a regular section number, not the literal "9.4bis".  Something like "Immediately before clause 9.5, create a new subclause:", and renumber subclauses 9.5 and 9.6 as 9.6 and 9.7".  And then show "9.4bis" as "9.4". 

OK.

* I notice that all the uses of the 'subdivides' verb concept are of the form "<finite time scale> subdivides <time point> into <number> of <time point>".  Which makes me wonder whether the verb concept should have 4 roles rather than 2. 

Hmm.  I think the original verb was based on the idea that the subdivision was like hours and minutes -- the whole finite time scale.  But of course that was never true for month-of-days or year-of-days.  The subdivision really uses a time point sequence beginning with the origin index, which is what the proposed revised definition says.  But that 'time point sequence' idea may be wrong.  That is, I think a time point sequence is different from a sequence of time points, and 'subdivides' is about that difference.

Technically a sequence of time points corresponds to sequences of time intervals.  We say a 'time point sequence' corresponds to the one big interval that is the span (hull) of the sequence of intervals.  Now the 'one big interval' view is consistent with the idea that '2:00 to 4:00' indicates a time point sequence that corresponds to intervals that have a duration of two hours (or correctly 120 minutes).  But that is not what we mean by 'subdivides',  We mean treating the larger time point as a sequence of time points that corresponds to sequences of smaller time intervals, rather than to the hull of them.  This leads me to think that the term 'time point sequence' violates (Bernd Wenzel's) Law of Least Astonishment.  That is 'time point sequence' is not the same as 'sequence of time points'.

* There should be a Note that explains why we talk about a subsequence of the finite time scale.  The reason is that the subdivision of some kinds of time points into finite time scales is irregular.  Months are subdivided into 28-31 days and years are subdivided into 365 or 366 days. 

Agree.

* But, looking further, all of the uses of this verb concept talk about subdividing the "larger" time point into a fixed (not varying) number of "smaller" time points.  For example, the 'Gregorian year of days scale' is defined as "the finite time scale that subdivides âGregorian yearâ into 366 of âGregorian day of yearâ ".  Should it talk about subdividing leap years into 366 and common years into 365 'Gregorian day of year'?  Should the 'Gregorian month of days scale' be explicit about how it divides each of the Gregorian months?  What do we do about the 'year of weeks scale' since the number of weeks in a year is really messy? 

I guess we need to discuss this.  I agree with Mark's concern here, but I don't know what we want to write.  And <expletive deleted> leap seconds make minute-of-seconds or day-of-seconds truly variable.  

* The wording of the Necessity seems like something a logician would write not something that makes business sense.  The phrase "If a finite time scale subdivides a time point," should not be needed since the Necessity is in the context of this verb concept.  (In any case, this Necessity will be rewritten if my point about missing roles is accepted.) 

Yes.  This is part of the above.

* I agree that this verb concept is related to 'time point converts to time point sequence on time scale' but I don't agree that this verb concept is a 'special case' of the latter.  This verb concept is about the definitional relationship between finite time scales and time points; whereas the other is about computing the conversion. 

The Beta text of this verb concept is broken.  The replacement text from Issue 17227 says: 
Definition:                             the time point is coextensive with the time point sequence 

Necessity:                              Each time point of the time point sequence is on the time scale. 

Possibility:                             The time point is an absolute time point or is a relative time point. 

Description:                          The time point and the time point sequence are two different ways to identify the same time intervals. 


It doesn't say anything about computation.  The purpose is to provide meaning to the idea of computing the referents of a time coordinate, yes.  The Beta text indicated that intent -- it was trying to say that the decomposition into time points was about identifying time periods.  But the mechanism is said here to involve the conversion to an equivalent sequence of time points.  The example for 17227:


Example:                                 The time point that is indicated by the time coordinate January 2012 converts to the time point sequence 2012 day 1 through 2012 day 31 on the Gregorian days scale. 


shows that the intent is different from 'subdivides'.  'subdivides' is about converting January 2012 to the month-of-days; this is about converting it to a subsequence of 'day-of-year'.

But this takes us back to the idea above, that there are two different time point sequence ideas.  I think the 'converts to' idea is about locating the larger interval in a longer sequence of finer granularity intervals, as the large interval that is the hull of a subsequence, while 'subdivides' is about treating the larger time point as a sequence of consecutive time points that corresponds to sequences of consecutive smaller time intervals.  That is, 'converts to' is not about decomposing the time point and its corresponding time periods, it is about locating it in some other sequence; but subdivides is about decomposing the time point and its corresponding time periods.  

So I agree with Mark that 'subdivides' is not a special case of 'converts to', but we somehow have to be clear about the difference in intent in the definitions.  They both seem to say:  "time point on scale A is coextensive with time point sequence on scale B."  17227 is correct that that is what converts to means.  For 'subdivides' we have to talk about sequences of time intervals, somehow.

Regarding 17367: 
* I think that the OCL for the new axiom in 8.1.1 should read, as follows -- but need to consult the OCL book when I get home to be sure: 
OCL Constraint:        context: "time interval" 
                                   inv: "time interval"."time interval1 is proper part of time interval2"-->notEmpty() 

OK.  I will put that in the next draft, with a comment that says 'check this'.

* Why not wrap the new axiom in 8.1.6 into the definition of 'properly during'?  Why should it be a separate axiom? 
* I haven't provided the OCL for this new axiom because I think it instead should be a modification of the definitional OCL for 'properly during'. 

Well, 'properly during' is one of the Allen relations, and it is defined in terms of 'part of ' and 'before'.  'properly during' just says there is a proper part that is before it and one that is after it, which logically completes the partitioning of 'proper part': starts has no before, finishes has no after, and during has both.  What Mark suggests is that 'A is properly during B' could be defined as:  A is a proper part of B and there is a time interval C such that C starts B and C meets A, etc.  That does not clearly complete the partition.  To complete it, you would have to prove that:  If A does not start or finish B, then there is a C that starts B and meets A.   That is, if there is a C that is a proper part of B and is before A (i.e. A does not start B), then there is a C' that starts B and meets A.  And that is what the proposed axiom says, because you can't prove it from the other axioms.

In a similar way, the weak supplementation axiom says that for every proper part there is another proper part that does not overlap it.  So if A starts B, A has a supplement and the supplement must be after A.  But there is a 'start complement' axiom that says that if A starts B, there is a C that is met by A and finishes B -- the "maximal" supplement.  I don't think you can get these "maximal supplement" theorems from the axioms for 'part of' and 'before', precisely because we don't have strong supplementation:  If A is properly during B, then B-A is not a time interval.

* I think that what Fabian asked for is a different new axiom that says that every time interval has a proper part that starts/finishes it. 

Ah!  But those follow from the proposed axiom, together with the existing start-complement and finish-complement axioms.  E.g.
Theorem:  Every time interval has a proper part that starts it.
Proof:
If a time interval B has a proper part A, then (by the Allen partitioning), one of the following must be true: A starts B, A finishes B, A is properly during B.
Now, if A starts B, B has a proper part (A) that starts it.
If A finishes B, by the finish complement axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
If A is during B, by the proposed axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
So, if a time interval B has a proper part A, B has a proper part that starts B in all cases.  
By the no-smallest-interval axiom, every time interval B has some proper part A.  
So every time interval B has a proper part that starts B in all cases.  Q.E.D.
 
The nagging question is whether there might be a simpler solution than having these three complement axioms.  In particular, could we instead assert that every time interval has a proper part that starts it and a proper part that finishes it?  I think not, because there is no basis for relating an arbitrary starting part to an arbitrary finishing part.

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800

"The opinions expressed above do not reflect consensus of NIST, 
and have not been reviewed by any Government authority." 



-------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        OMG DateTimeVoc FTF <date-time-ftf@omg.org>, 
Date:        07/16/2012 07:23 PM 
Subject:        DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------



Per today's conference call, I attach the revised drafts for resolution 
of Issues
16689 - D0 should be quantified (added the UML object D0)
16951 - time point subdivision (see markup),
17367- no smallest time interval (1st draft, needs OCL)

For 16689, should we have defined a term like 'zero duration'?  Should 
that be the term and D0 the Synonym?

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800



[attachment "DTV Issue 17367- no smallest time interval-d1.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16689-D0 should be quantified.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16951-time point subdivision-d4.doc" deleted by Mark H Linehan/Watson/IBM] 

<Down>
<Down>
Date: Fri, 27 Jul 2012 11:12:34 -0400
From: Ed Barkmeyer <edbark@nist.gov>
Reply-To: <edbark@nist.gov>
Organization: NIST
User-Agent: Thunderbird 2.0.0.23 (Windows/20090812)
To: Mark H Linehan <mlinehan@us.ibm.com>
CC: "date-time-ftf@omg.org" <date-time-ftf@omg.org>,
        Stan Hendryx
        <stan@hendryxassoc.com>
Subject: Re: DTV Issues 16689, 16951, 17367 proposed resolutions
X-NISTMEL-MailScanner-Information: Please contact postmaster@mel.nist.gov for more information
X-NISTMEL-MailScanner-ID: q6RFCe2T006363
X-NISTMEL-MailScanner: Found to be clean
X-NISTMEL-MailScanner-SpamCheck: 
X-NISTMEL-MailScanner-From: edbark@nist.gov
X-NISTMEL-MailScanner-Watermark: 1344006762.83562@KLFdVdmrpmJLFVcnkNwSaw
X-Spam-Status: No




Mark H Linehan wrote: 
Ed, 

Regarding 16689:  Why isn't the  function (+ d1 d2) just a noun form of the predicate "duration3 = duration1 + duration2"?

Noun-form of a verb is an SBVR idea that is misleading.  (I raised an issue on this in the first SBVR FTF, and it was swept under the rug.) In SBVR the instances of a verb concept are actualities, but the instances of the 'noun-form' of the verb are things that play roles in the actualities.  The "extensions" are not even of the same kind.  That is why I say the SBVR term is misleading.  The "noun-form" represents the 'function' concept, which is not a 'verb concept'.  It is a different, but related, concept.  And the two concepts are related by a definition such as the CLIF definition I gave.
[In classical formal logics, a predicate (verb concept) is a mapping from a tuple of things to true/false.  (Of course, Lowe and Zalta don't agree.)  And a function is a mapping from a tuple of things to a thing.  The SBVR 'noun form' is a function, as Mark pointed out.]

The real "noun form" of a verb concept is the gerund, or a noun that objectifies the verb, as defined in clause 11.  Those concepts have the same extension.



Regarding 16951:  I don't think we need to distinguish "time point sequence" from "sequence of time points".  I think these are just two views of the same thing: either the time interval that corresponds to the convex hull of the whole time point sequence, or a sequence of time intervals that correspond to the individual time points of the time point sequence.  I think the two verb concepts ('subdivides' and 'converts to') are two different ways of using the one general concept.


OK, but my point is that those two 'views' see technically different extensions of a time point sequence.  The whole point of subdivision is to decompose the time intervals, not to see them as one big interval.  subdivides decomposes an X into Ys, converts composes Ys into an X.



Regarding how to define the time scales that irregularly subdivide time points, here's an example of what I suggest we should write: 

"Gregorian year of days scale: the finite time scale that subdivides .common year. into 365 of .Gregorian day of year. and that subdivides 'leap year' into 366 of .Gregorian day of year.. 



Yes.  I agree.


I don't think leap seconds have anything to do with this discussion.  Leap seconds involve displacing the UTC time scale, not adding seconds to calendar days.  BIPM is clear that 'day' is fixed at 86400 seconds. 



But the BIPM 'day' is a duration, a time unit.  A UTC day is a calendar day, and its length is variable, and the variation does not follow a named pattern like common year and leap year.  We don't cast 'leap seconds' as a kind of 'time offset' (from TAI to UTC), but that is what "displacing the UTC time scale" suggests.  It makes some sense.  The UTC rules are then rather like those of timezones -- some authority decides when to change from one time offset to another. We already have time offsets in hours and minutes; we could add seconds.  Is that a better approach than what we wrote?  


Regarding 17367: OK on adding the new axiom.  Here's the OCL, I think: 

OCL Definition:        context "time interval" 
                        inv: "time interval".allInstances-->forAll(t2 | 
                                       t2."is properly during"(self) 
                                                   implies "time interval".allInstances-->exists(t3 | 
                                                        t3.starts(self) and t3.meets(t2))) 
                        context "time interval" 
                        inv: "time interval".allInstances-->forAll(t2 | 
                                       t2." is properly during"(self) 
                                                   implies "time interval".allInstances-->exists(t3 | 
                                                        t3.ends(self) and t2.meets(t3))) 

I think we should make explicit the new axiom requested by Fabian. 



I agree.  I didn't realize I had not done that.

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800





--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        Mark H Linehan/Watson/IBM@IBMUS, 
Cc:        "date-time-ftf@omg.org" <date-time-ftf@omg.org>, Stan Hendryx <stan@hendryxassoc.com> 
Date:        07/26/2012 01:19 PM 
Subject:        Re: DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------





Mark H Linehan wrote: 
Regarding 16689: 
* I don't see the value of this CLIF axiom; it doesn't seem to say anything.  The one proposed to go after axiom V1 seems sufficient. 
CLIF Definition:        (forall ((d1 duration) (d2 duration) d3)
 (iff
   (= d3 (+ d1 d2))
   (and
     (duration d3)
     ("duration3 = duration1 + duration2"
        d3 d1 d2) ))) 

This axiom defines the function (+ d1 d2).  Otherwise it is primitive, and not clearly related to the predicate "duration3 = duration1 + duration2".  Or at least, I think that is the case.  The proposed axiom for V1 says that the function is defined everywhere:
(forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
  
* I don't have a strong opinion about 'D0' versus 'zero duration'.  I don't see a lot of value in using the term 'zero duration' instead of 'D0'. 

In SBVR parlance, D0 is a symbol, 'zero duration' is a term.  Given that it is a term for something that is strictly a mathematical concept, it probably makes no difference.

Regarding 16951: 
* Editorial instruction #2 should make it clear that the new subsection has a regular section number, not the literal "9.4bis".  Something like "Immediately before clause 9.5, create a new subclause:", and renumber subclauses 9.5 and 9.6 as 9.6 and 9.7".  And then show "9.4bis" as "9.4". 

OK.

* I notice that all the uses of the 'subdivides' verb concept are of the form "<finite time scale> subdivides <time point> into <number> of <time point>".  Which makes me wonder whether the verb concept should have 4 roles rather than 2. 

Hmm.  I think the original verb was based on the idea that the subdivision was like hours and minutes -- the whole finite time scale.  But of course that was never true for month-of-days or year-of-days.  The subdivision really uses a time point sequence beginning with the origin index, which is what the proposed revised definition says.  But that 'time point sequence' idea may be wrong.  That is, I think a time point sequence is different from a sequence of time points, and 'subdivides' is about that difference.

Technically a sequence of time points corresponds to sequences of time intervals.  We say a 'time point sequence' corresponds to the one big interval that is the span (hull) of the sequence of intervals.  Now the 'one big interval' view is consistent with the idea that '2:00 to 4:00' indicates a time point sequence that corresponds to intervals that have a duration of two hours (or correctly 120 minutes).  But that is not what we mean by 'subdivides',  We mean treating the larger time point as a sequence of time points that corresponds to sequences of smaller time intervals, rather than to the hull of them.  This leads me to think that the term 'time point sequence' violates (Bernd Wenzel's) Law of Least Astonishment.  That is 'time point sequence' is not the same as 'sequence of time points'.

* There should be a Note that explains why we talk about a subsequence of the finite time scale.  The reason is that the subdivision of some kinds of time points into finite time scales is irregular.  Months are subdivided into 28-31 days and years are subdivided into 365 or 366 days. 

Agree.

* But, looking further, all of the uses of this verb concept talk about subdividing the "larger" time point into a fixed (not varying) number of "smaller" time points.  For example, the 'Gregorian year of days scale' is defined as "the finite time scale that subdivides .Gregorian year. into 366 of .Gregorian day of year. ".  Should it talk about subdividing leap years into 366 and common years into 365 'Gregorian day of year'?  Should the 'Gregorian month of days scale' be explicit about how it divides each of the Gregorian months?  What do we do about the 'year of weeks scale' since the number of weeks in a year is really messy? 

I guess we need to discuss this.  I agree with Mark's concern here, but I don't know what we want to write.  And <expletive deleted> leap seconds make minute-of-seconds or day-of-seconds truly variable.  

* The wording of the Necessity seems like something a logician would write not something that makes business sense.  The phrase "If a finite time scale subdivides a time point," should not be needed since the Necessity is in the context of this verb concept.  (In any case, this Necessity will be rewritten if my point about missing roles is accepted.) 

Yes.  This is part of the above.

* I agree that this verb concept is related to 'time point converts to time point sequence on time scale' but I don't agree that this verb concept is a 'special case' of the latter.  This verb concept is about the definitional relationship between finite time scales and time points; whereas the other is about computing the conversion. 

The Beta text of this verb concept is broken.  The replacement text from Issue 17227 says: 
Definition:                             the time point is coextensive with the time point sequence 

Necessity:                              Each time point of the time point sequence is on the time scale. 

Possibility:                             The time point is an absolute time point or is a relative time point. 

Description:                          The time point and the time point sequence are two different ways to identify the same time intervals. 


It doesn't say anything about computation.  The purpose is to provide meaning to the idea of computing the referents of a time coordinate, yes.  The Beta text indicated that intent -- it was trying to say that the decomposition into time points was about identifying time periods.  But the mechanism is said here to involve the conversion to an equivalent sequence of time points.  The example for 17227:


Example:                                 The time point that is indicated by the time coordinate January 2012 converts to the time point sequence 2012 day 1 through 2012 day 31 on the Gregorian days scale. 


shows that the intent is different from 'subdivides'.  'subdivides' is about converting January 2012 to the month-of-days; this is about converting it to a subsequence of 'day-of-year'.

But this takes us back to the idea above, that there are two different time point sequence ideas.  I think the 'converts to' idea is about locating the larger interval in a longer sequence of finer granularity intervals, as the large interval that is the hull of a subsequence, while 'subdivides' is about treating the larger time point as a sequence of consecutive time points that corresponds to sequences of consecutive smaller time intervals.  That is, 'converts to' is not about decomposing the time point and its corresponding time periods, it is about locating it in some other sequence; but subdivides is about decomposing the time point and its corresponding time periods.  

So I agree with Mark that 'subdivides' is not a special case of 'converts to', but we somehow have to be clear about the difference in intent in the definitions.  They both seem to say:  "time point on scale A is coextensive with time point sequence on scale B."  17227 is correct that that is what converts to means.  For 'subdivides' we have to talk about sequences of time intervals, somehow.

Regarding 17367: 
* I think that the OCL for the new axiom in 8.1.1 should read, as follows -- but need to consult the OCL book when I get home to be sure: 
OCL Constraint:        context: "time interval" 
                                   inv: "time interval"."time interval1 is proper part of time interval2"-->notEmpty() 

OK.  I will put that in the next draft, with a comment that says 'check this'.

* Why not wrap the new axiom in 8.1.6 into the definition of 'properly during'?  Why should it be a separate axiom? 
* I haven't provided the OCL for this new axiom because I think it instead should be a modification of the definitional OCL for 'properly during'. 

Well, 'properly during' is one of the Allen relations, and it is defined in terms of 'part of ' and 'before'.  'properly during' just says there is a proper part that is before it and one that is after it, which logically completes the partitioning of 'proper part': starts has no before, finishes has no after, and during has both.  What Mark suggests is that 'A is properly during B' could be defined as:  A is a proper part of B and there is a time interval C such that C starts B and C meets A, etc.  That does not clearly complete the partition.  To complete it, you would have to prove that:  If A does not start or finish B, then there is a C that starts B and meets A.   That is, if there is a C that is a proper part of B and is before A (i.e. A does not start B), then there is a C' that starts B and meets A.  And that is what the proposed axiom says, because you can't prove it from the other axioms.

In a similar way, the weak supplementation axiom says that for every proper part there is another proper part that does not overlap it.  So if A starts B, A has a supplement and the supplement must be after A.  But there is a 'start complement' axiom that says that if A starts B, there is a C that is met by A and finishes B -- the "maximal" supplement.  I don't think you can get these "maximal supplement" theorems from the axioms for 'part of' and 'before', precisely because we don't have strong supplementation:  If A is properly during B, then B-A is not a time interval.

* I think that what Fabian asked for is a different new axiom that says that every time interval has a proper part that starts/finishes it. 

Ah!  But those follow from the proposed axiom, together with the existing start-complement and finish-complement axioms.  E.g.
Theorem:  Every time interval has a proper part that starts it.
Proof:
If a time interval B has a proper part A, then (by the Allen partitioning), one of the following must be true: A starts B, A finishes B, A is properly during B.
Now, if A starts B, B has a proper part (A) that starts it.
If A finishes B, by the finish complement axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
If A is during B, by the proposed axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
So, if a time interval B has a proper part A, B has a proper part that starts B in all cases.  
By the no-smallest-interval axiom, every time interval B has some proper part A.  
So every time interval B has a proper part that starts B in all cases.  Q.E.D.
 
The nagging question is whether there might be a simpler solution than having these three complement axioms.  In particular, could we instead assert that every time interval has a proper part that starts it and a proper part that finishes it?  I think not, because there is no basis for relating an arbitrary starting part to an arbitrary finishing part.

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800

"The opinions expressed above do not reflect consensus of NIST, 
and have not been reviewed by any Government authority." 



-------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        OMG DateTimeVoc FTF <date-time-ftf@omg.org>, 
Date:        07/16/2012 07:23 PM 
Subject:        DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------



Per today's conference call, I attach the revised drafts for resolution 
of Issues
16689 - D0 should be quantified (added the UML object D0)
16951 - time point subdivision (see markup),
17367- no smallest time interval (1st draft, needs OCL)

For 16689, should we have defined a term like 'zero duration'?  Should 
that be the term and D0 the Synonym?

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800



[attachment "DTV Issue 17367- no smallest time interval-d1.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16689-D0 should be quantified.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16951-time point subdivision-d4.doc" deleted by Mark H Linehan/Watson/IBM] 



To: date-time-ftf@omg.org, Stan@hendryxassoc.com
Subject: Re: DTV Issues 16689, 16951, 17367 proposed resolutions
X-KeepSent: 9BC86758:42435A73-85257A48:006E0E0C;
 type=4; name=$KeepSent
X-Mailer: Lotus Notes Release 8.5.3 September 15, 2011
From: Mark H Linehan <mlinehan@us.ibm.com>
Date: Fri, 27 Jul 2012 16:08:39 -0400
X-MIMETrack: Serialize by Router on D01MC604/01/M/IBM(Release 8.5.3 ZX853HP5|January 12, 2012) at
 07/27/2012 16:08:44,
        Serialize complete at 07/27/2012 16:08:44
X-Content-Scanned: Fidelis XPS MAILER
x-cbid: 12072720-5806-0000-0000-000017BD13F2


I think we basically agree.  My responses like this. 
--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        Mark H Linehan/Watson/IBM@IBMUS, 
Cc:        "date-time-ftf@omg.org" <date-time-ftf@omg.org>, Stan Hendryx <stan@hendryxassoc.com> 
Date:        07/27/2012 11:13 AM 
Subject:        Re: DTV Issues 16689, 16951, 17367 proposed resolutions 

--------------------------------------------------------------------------------





Mark H Linehan wrote: 
Ed, 

Regarding 16689:  Why isn't the  function (+ d1 d2) just a noun form of the predicate "duration3 = duration1 + duration2"? 

Noun-form of a verb is an SBVR idea that is misleading.  (I raised an issue on this in the first SBVR FTF, and it was swept under the rug.) In SBVR the instances of a verb concept are actualities, but the instances of the 'noun-form' of the verb are things that play roles in the actualities.  The "extensions" are not even of the same kind.  That is why I say the SBVR term is misleading.  The "noun-form" represents the 'function' concept, which is not a 'verb concept'.  It is a different, but related, concept.  And the two concepts are related by a definition such as the CLIF definition I gave.
[In classical formal logics, a predicate (verb concept) is a mapping from a tuple of things to true/false.  (Of course, Lowe and Zalta don't agree.)  And a function is a mapping from a tuple of things to a thing.  The SBVR 'noun form' is a function, as Mark pointed out.]

The real "noun form" of a verb concept is the gerund, or a noun that objectifies the verb, as defined in clause 11.  Those concepts have the same extension. 

I don't want to debate the concept or term 'noun form'.  My point is that the standard SBVR approach is to define "+d1 d2" as a synonymous form of "duration3 equals duration1 plus duration2".  Actually, I see we already have this synonymous form. 

Given that, the proposed CLIF doesn't say anything that isn't already implied by having the synonymous form.

Regarding 16951:  I don't think we need to distinguish "time point sequence" from "sequence of time points".  I think these are just two views of the same thing: either the time interval that corresponds to the convex hull of the whole time point sequence, or a sequence of time intervals that correspond to the individual time points of the time point sequence.  I think the two verb concepts ('subdivides' and 'converts to') are two different ways of using the one general concept. 


OK, but my point is that those two 'views' see technically different extensions of a time point sequence.  The whole point of subdivision is to decompose the time intervals, not to see them as one big interval.  subdivides decomposes an X into Ys, converts composes Ys into an X.


Yes, that's why I said one isn't a subtype of the other, but they are related.  I think we agree. 

Regarding how to define the time scales that irregularly subdivide time points, here's an example of what I suggest we should write: 

"Gregorian year of days scale: the finite time scale that subdivides âcommon yearâ into 365 of âGregorian day of yearâ and that subdivides 'leap year' into 366 of âGregorian day of yearâ. 


Yes.  I agree.


I don't think leap seconds have anything to do with this discussion.  Leap seconds involve displacing the UTC time scale, not adding seconds to calendar days.  BIPM is clear that 'day' is fixed at 86400 seconds. 


But the BIPM 'day' is a duration, a time unit.  A UTC day is a calendar day, and its length is variable, and the variation does not follow a named pattern like common year and leap year.  We don't cast 'leap seconds' as a kind of 'time offset' (from TAI to UTC), but that is what "displacing the UTC time scale" suggests.  It makes some sense.  The UTC rules are then rather like those of timezones -- some authority decides when to change from one time offset to another. We already have time offsets in hours and minutes; we could add seconds.  Is that a better approach than what we wrote?  


That's what we already decided and voted in issue 16680. Given that resolution, there's no reason to bring leap seconds into this "subdivides" discussion. 

Actually, I see that that resolution redefined the 'day of seconds scale' as "the finite time scale that subdivides each calendar day into at most 86 401 second of day".   So that resolution already started down the path of making these definitions acknowledge the varying number of x units in y time point.  Let's continue that. 

Regarding 17367: OK on adding the new axiom.  Here's the OCL, I think: 

OCL Definition:        context "time interval" 
                        inv: "time interval".allInstances-->forAll(t2 | 
                                       t2."is properly during"(self) 
                                                   implies "time interval".allInstances-->exists(t3 | 
                                                        t3.starts(self) and t3.meets(t2))) 
                        context "time interval" 
                        inv: "time interval".allInstances-->forAll(t2 | 
                                       t2." is properly during"(self) 
                                                   implies "time interval".allInstances-->exists(t3 | 
                                                        t3.ends(self) and t2.meets(t3))) 

I think we should make explicit the new axiom requested by Fabian. 


I agree.  I didn't realize I had not done that.

-Ed 
-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800





--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        Mark H Linehan/Watson/IBM@IBMUS, 
Cc:        "date-time-ftf@omg.org" <date-time-ftf@omg.org>, Stan Hendryx <stan@hendryxassoc.com> 
Date:        07/26/2012 01:19 PM 
Subject:        Re: DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------





Mark H Linehan wrote: 
Regarding 16689: 
* I don't see the value of this CLIF axiom; it doesn't seem to say anything.  The one proposed to go after axiom V1 seems sufficient. 
CLIF Definition:        (forall ((d1 duration) (d2 duration) d3)
 (iff
   (= d3 (+ d1 d2))
   (and
     (duration d3)
     ("duration3 = duration1 + duration2"
        d3 d1 d2) ))) 

This axiom defines the function (+ d1 d2).  Otherwise it is primitive, and not clearly related to the predicate "duration3 = duration1 + duration2".  Or at least, I think that is the case.  The proposed axiom for V1 says that the function is defined everywhere:
(forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
  
* I don't have a strong opinion about 'D0' versus 'zero duration'.  I don't see a lot of value in using the term 'zero duration' instead of 'D0'. 

In SBVR parlance, D0 is a symbol, 'zero duration' is a term.  Given that it is a term for something that is strictly a mathematical concept, it probably makes no difference.

Regarding 16951: 
* Editorial instruction #2 should make it clear that the new subsection has a regular section number, not the literal "9.4bis".  Something like "Immediately before clause 9.5, create a new subclause:", and renumber subclauses 9.5 and 9.6 as 9.6 and 9.7".  And then show "9.4bis" as "9.4". 

OK.

* I notice that all the uses of the 'subdivides' verb concept are of the form "<finite time scale> subdivides <time point> into <number> of <time point>".  Which makes me wonder whether the verb concept should have 4 roles rather than 2. 

Hmm.  I think the original verb was based on the idea that the subdivision was like hours and minutes -- the whole finite time scale.  But of course that was never true for month-of-days or year-of-days.  The subdivision really uses a time point sequence beginning with the origin index, which is what the proposed revised definition says.  But that 'time point sequence' idea may be wrong.  That is, I think a time point sequence is different from a sequence of time points, and 'subdivides' is about that difference.

Technically a sequence of time points corresponds to sequences of time intervals.  We say a 'time point sequence' corresponds to the one big interval that is the span (hull) of the sequence of intervals.  Now the 'one big interval' view is consistent with the idea that '2:00 to 4:00' indicates a time point sequence that corresponds to intervals that have a duration of two hours (or correctly 120 minutes).  But that is not what we mean by 'subdivides',  We mean treating the larger time point as a sequence of time points that corresponds to sequences of smaller time intervals, rather than to the hull of them.  This leads me to think that the term 'time point sequence' violates (Bernd Wenzel's) Law of Least Astonishment.  That is 'time point sequence' is not the same as 'sequence of time points'.

* There should be a Note that explains why we talk about a subsequence of the finite time scale.  The reason is that the subdivision of some kinds of time points into finite time scales is irregular.  Months are subdivided into 28-31 days and years are subdivided into 365 or 366 days. 

Agree.

* But, looking further, all of the uses of this verb concept talk about subdividing the "larger" time point into a fixed (not varying) number of "smaller" time points.  For example, the 'Gregorian year of days scale' is defined as "the finite time scale that subdivides âGregorian yearâ into 366 of âGregorian day of yearâ ".  Should it talk about subdividing leap years into 366 and common years into 365 'Gregorian day of year'?  Should the 'Gregorian month of days scale' be explicit about how it divides each of the Gregorian months?  What do we do about the 'year of weeks scale' since the number of weeks in a year is really messy? 

I guess we need to discuss this.  I agree with Mark's concern here, but I don't know what we want to write.  And <expletive deleted> leap seconds make minute-of-seconds or day-of-seconds truly variable.  

* The wording of the Necessity seems like something a logician would write not something that makes business sense.  The phrase "If a finite time scale subdivides a time point," should not be needed since the Necessity is in the context of this verb concept.  (In any case, this Necessity will be rewritten if my point about missing roles is accepted.) 

Yes.  This is part of the above.

* I agree that this verb concept is related to 'time point converts to time point sequence on time scale' but I don't agree that this verb concept is a 'special case' of the latter.  This verb concept is about the definitional relationship between finite time scales and time points; whereas the other is about computing the conversion. 

The Beta text of this verb concept is broken.  The replacement text from Issue 17227 says: 
Definition:                             the time point is coextensive with the time point sequence 

Necessity:                              Each time point of the time point sequence is on the time scale. 

Possibility:                             The time point is an absolute time point or is a relative time point. 

Description:                          The time point and the time point sequence are two different ways to identify the same time intervals. 


It doesn't say anything about computation.  The purpose is to provide meaning to the idea of computing the referents of a time coordinate, yes.  The Beta text indicated that intent -- it was trying to say that the decomposition into time points was about identifying time periods.  But the mechanism is said here to involve the conversion to an equivalent sequence of time points.  The example for 17227: 

Example:                                 The time point that is indicated by the time coordinate January 2012 converts to the time point sequence 2012 day 1 through 2012 day 31 on the Gregorian days scale. 


shows that the intent is different from 'subdivides'.  'subdivides' is about converting January 2012 to the month-of-days; this is about converting it to a subsequence of 'day-of-year'.

But this takes us back to the idea above, that there are two different time point sequence ideas.  I think the 'converts to' idea is about locating the larger interval in a longer sequence of finer granularity intervals, as the large interval that is the hull of a subsequence, while 'subdivides' is about treating the larger time point as a sequence of consecutive time points that corresponds to sequences of consecutive smaller time intervals.  That is, 'converts to' is not about decomposing the time point and its corresponding time periods, it is about locating it in some other sequence; but subdivides is about decomposing the time point and its corresponding time periods.  

So I agree with Mark that 'subdivides' is not a special case of 'converts to', but we somehow have to be clear about the difference in intent in the definitions.  They both seem to say:  "time point on scale A is coextensive with time point sequence on scale B."  17227 is correct that that is what converts to means.  For 'subdivides' we have to talk about sequences of time intervals, somehow.

Regarding 17367: 
* I think that the OCL for the new axiom in 8.1.1 should read, as follows -- but need to consult the OCL book when I get home to be sure: 
OCL Constraint:        context: "time interval" 
                                   inv: "time interval"."time interval1 is proper part of time interval2"-->notEmpty() 

OK.  I will put that in the next draft, with a comment that says 'check this'.

* Why not wrap the new axiom in 8.1.6 into the definition of 'properly during'?  Why should it be a separate axiom? 
* I haven't provided the OCL for this new axiom because I think it instead should be a modification of the definitional OCL for 'properly during'. 

Well, 'properly during' is one of the Allen relations, and it is defined in terms of 'part of ' and 'before'.  'properly during' just says there is a proper part that is before it and one that is after it, which logically completes the partitioning of 'proper part': starts has no before, finishes has no after, and during has both.  What Mark suggests is that 'A is properly during B' could be defined as:  A is a proper part of B and there is a time interval C such that C starts B and C meets A, etc.  That does not clearly complete the partition.  To complete it, you would have to prove that:  If A does not start or finish B, then there is a C that starts B and meets A.   That is, if there is a C that is a proper part of B and is before A (i.e. A does not start B), then there is a C' that starts B and meets A.  And that is what the proposed axiom says, because you can't prove it from the other axioms.

In a similar way, the weak supplementation axiom says that for every proper part there is another proper part that does not overlap it.  So if A starts B, A has a supplement and the supplement must be after A.  But there is a 'start complement' axiom that says that if A starts B, there is a C that is met by A and finishes B -- the "maximal" supplement.  I don't think you can get these "maximal supplement" theorems from the axioms for 'part of' and 'before', precisely because we don't have strong supplementation:  If A is properly during B, then B-A is not a time interval.

* I think that what Fabian asked for is a different new axiom that says that every time interval has a proper part that starts/finishes it. 

Ah!  But those follow from the proposed axiom, together with the existing start-complement and finish-complement axioms.  E.g.
Theorem:  Every time interval has a proper part that starts it.
Proof:
If a time interval B has a proper part A, then (by the Allen partitioning), one of the following must be true: A starts B, A finishes B, A is properly during B.
Now, if A starts B, B has a proper part (A) that starts it.
If A finishes B, by the finish complement axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
If A is during B, by the proposed axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
So, if a time interval B has a proper part A, B has a proper part that starts B in all cases.  
By the no-smallest-interval axiom, every time interval B has some proper part A.  
So every time interval B has a proper part that starts B in all cases.  Q.E.D.
 
The nagging question is whether there might be a simpler solution than having these three complement axioms.  In particular, could we instead assert that every time interval has a proper part that starts it and a proper part that finishes it?  I think not, because there is no basis for relating an arbitrary starting part to an arbitrary finishing part.

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800

"The opinions expressed above do not reflect consensus of NIST, 
and have not been reviewed by any Government authority." 



-------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        OMG DateTimeVoc FTF <date-time-ftf@omg.org>, 
Date:        07/16/2012 07:23 PM 
Subject:        DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------



Per today's conference call, I attach the revised drafts for resolution 
of Issues
16689 - D0 should be quantified (added the UML object D0)
16951 - time point subdivision (see markup),
17367- no smallest time interval (1st draft, needs OCL)

For 16689, should we have defined a term like 'zero duration'?  Should 
that be the term and D0 the Synonym?

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800



[attachment "DTV Issue 17367- no smallest time interval-d1.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16689-D0 should be quantified.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16951-time point subdivision-d4.doc" deleted by Mark H Linehan/Watson/IBM] 



<Down>
<Down>
Date: Fri, 27 Jul 2012 18:44:52 -0400
From: Ed Barkmeyer <edbark@nist.gov>
Reply-To: <edbark@nist.gov>
Organization: NIST
User-Agent: Thunderbird 2.0.0.23 (Windows/20090812)
To: Mark H Linehan <mlinehan@us.ibm.com>
CC: "date-time-ftf@omg.org" <date-time-ftf@omg.org>,
        "Stan@hendryxassoc.com"
        <Stan@hendryxassoc.com>
Subject: Re: DTV Issues 16689, 16951, 17367 proposed resolutions
X-NISTMEL-MailScanner-Information: Please contact postmaster@mel.nist.gov for more information
X-NISTMEL-MailScanner-ID: q6RMiviB003968
X-NISTMEL-MailScanner: Found to be clean
X-NISTMEL-MailScanner-SpamCheck: 
X-NISTMEL-MailScanner-From: edbark@nist.gov
X-NISTMEL-MailScanner-Watermark: 1344033901.27701@njp8Ztk9+7PoD0eAHl268Q
X-Spam-Status: No


I attach the revised version of Issue 17367, incorporating the agreements.  (I didn't have change tracking on.  I added Mark's OCL and Fabian's corollaries.)

I attach a slightly revised version of 16689.  I hope we are done with this.

I need to do more work on 16951.

Mark H Linehan wrote:

Regarding 16689:  Why isn't the  function (+ d1 d2) just a noun form of the predicate "duration3 = duration1 + duration2"? 
...
My point is that the standard SBVR approach is to define "+d1 d2" as a synonymous form of "duration3 equals duration1 plus duration2".  Actually, I see we already have this synonymous form. 

Given that, the proposed CLIF doesn't say anything that isn't already implied by having the synonymous form.


Well, perhaps the function is implied by the predicate in SBVR, but in CLIF they are unrelated symbols unless we relate them.  In the same way, defining the association in the UML model doesn't define the operation.  That is all this does.  You have to read the CLIF to say: d3 is (+ d1 d2) exactly when ("duration3 equals duration1 plus duration2" d3 d1 d2).  (In a reasoner, one would "skolemize" the thing named (+ d1 d2) by inventing a d3 to be the result, i.e., (exists (d3))(= d3 (+ d1 d2)), and then this definition axiom turns "d3 =  structured name" into a proposition involving d1, d2, and d3.)


Regarding 16951:  I don't think we need to distinguish "time point sequence" from "sequence of time points".  I think these are just two views of the same thing: either the time interval that corresponds to the convex hull of the whole time point sequence, or a sequence of time intervals that correspond to the individual time points of the time point sequence.  I think the two verb concepts ('subdivides' and 'converts to') are two different ways of using the one general concept. 

EJB
OK, but my point is that those two 'views' see technically different extensions of a time point sequence.  The whole point of subdivision is to decompose the time intervals, not to see them as one big interval.  subdivides decomposes an X into Ys, converts composes Ys into an X.


MHL: Yes, that's why I said one isn't a subtype of the other, but they are related.  I think we agree.


Yes, we agree on that.  I am still a bit worried about what the extension of a time point sequence is.  The convex hull is in some sense equivalent to the sequence of component intervals, but it is not the same thing.
.  


MHL

I don't think leap seconds have anything to do with this discussion.  Leap seconds involve displacing the UTC time scale, not adding seconds to calendar days.  BIPM is clear that 'day' is fixed at 86400 seconds. 

EJB
But the BIPM 'day' is a duration, a time unit.  A UTC day is a calendar day, and its length is variable, and the variation does not follow a named pattern like common year and leap year.  We don't cast 'leap seconds' as a kind of 'time offset' (from TAI to UTC), but that is what "displacing the UTC time scale" suggests.  It makes some sense.  The UTC rules are then rather like those of timezones -- some authority decides when to change from one time offset to another. We already have time offsets in hours and minutes; we could add seconds.  Is that a better approach than what we wrote?  


MHL
That's what we already decided and voted in issue 16680. Given that resolution, there's no reason to bring leap seconds into this "subdivides" discussion. 

Actually, I see that that resolution redefined the 'day of seconds scale' as "the finite time scale that subdivides each calendar day into at most 86 401 second of day".   So that resolution already started down the path of making these definitions acknowledge the varying number of x units in y time point.  Let's continue that.


What we agreed to in 16680 is NOT to describe leap seconds as time offsets, but rather to agree that there are minutes of different lengths and days of different lengths.  Describing 'leap seconds' as time offsets is very different:  Every clock minute would be subdivided into exactly 60 seconds, and every calendar day into exactly 86400 seconds.  But every time UTC adds a leap second we use a different calendar with a different time offset from TAI.  In the same way, the US Eastern Time Zone does not have variable length days, it just sometimes uses the EST offset and sometimes uses the EDT offset.  This affects the duration of a 'day period', but not a calendar day.  What I am suggesting is that UTC is several different calendars with different time offsets from TAI -- each leap second they add defines a new calendar with a different time offset: "UTC as of <datetime>".

If we adopt that view of leap seconds, we can do what you suggest about the subdivisions:  common years and leap years have different subdivisions, March and April have different subdivisions, but none of them is variable.  Leap seconds are the only things that create truly variable subdivisions, and if we switch to a time offset model of leap seconds, the variable subdivisions disappear entirely. 






--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        Mark H Linehan/Watson/IBM@IBMUS, 
Cc:        "date-time-ftf@omg.org" <date-time-ftf@omg.org>, Stan Hendryx <stan@hendryxassoc.com> 
Date:        07/26/2012 01:19 PM 
Subject:        Re: DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------





Mark H Linehan wrote: 
Regarding 16689: 
* I don't see the value of this CLIF axiom; it doesn't seem to say anything.  The one proposed to go after axiom V1 seems sufficient. 
CLIF Definition:        (forall ((d1 duration) (d2 duration) d3)
 (iff
   (= d3 (+ d1 d2))
   (and
     (duration d3)
     ("duration3 = duration1 + duration2"
        d3 d1 d2) ))) 

This axiom defines the function (+ d1 d2).  Otherwise it is primitive, and not clearly related to the predicate "duration3 = duration1 + duration2".  Or at least, I think that is the case.  The proposed axiom for V1 says that the function is defined everywhere:
(forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
  
* I don't have a strong opinion about 'D0' versus 'zero duration'.  I don't see a lot of value in using the term 'zero duration' instead of 'D0'. 

In SBVR parlance, D0 is a symbol, 'zero duration' is a term.  Given that it is a term for something that is strictly a mathematical concept, it probably makes no difference.

Regarding 16951: 
* Editorial instruction #2 should make it clear that the new subsection has a regular section number, not the literal "9.4bis".  Something like "Immediately before clause 9.5, create a new subclause:", and renumber subclauses 9.5 and 9.6 as 9.6 and 9.7".  And then show "9.4bis" as "9.4". 

OK.

* I notice that all the uses of the 'subdivides' verb concept are of the form "<finite time scale> subdivides <time point> into <number> of <time point>".  Which makes me wonder whether the verb concept should have 4 roles rather than 2. 

Hmm.  I think the original verb was based on the idea that the subdivision was like hours and minutes -- the whole finite time scale.  But of course that was never true for month-of-days or year-of-days.  The subdivision really uses a time point sequence beginning with the origin index, which is what the proposed revised definition says.  But that 'time point sequence' idea may be wrong.  That is, I think a time point sequence is different from a sequence of time points, and 'subdivides' is about that difference.

Technically a sequence of time points corresponds to sequences of time intervals.  We say a 'time point sequence' corresponds to the one big interval that is the span (hull) of the sequence of intervals.  Now the 'one big interval' view is consistent with the idea that '2:00 to 4:00' indicates a time point sequence that corresponds to intervals that have a duration of two hours (or correctly 120 minutes).  But that is not what we mean by 'subdivides',  We mean treating the larger time point as a sequence of time points that corresponds to sequences of smaller time intervals, rather than to the hull of them.  This leads me to think that the term 'time point sequence' violates (Bernd Wenzel's) Law of Least Astonishment.  That is 'time point sequence' is not the same as 'sequence of time points'.

* There should be a Note that explains why we talk about a subsequence of the finite time scale.  The reason is that the subdivision of some kinds of time points into finite time scales is irregular.  Months are subdivided into 28-31 days and years are subdivided into 365 or 366 days. 

Agree.

* But, looking further, all of the uses of this verb concept talk about subdividing the "larger" time point into a fixed (not varying) number of "smaller" time points.  For example, the 'Gregorian year of days scale' is defined as "the finite time scale that subdivides .Gregorian year. into 366 of .Gregorian day of year. ".  Should it talk about subdividing leap years into 366 and common years into 365 'Gregorian day of year'?  Should the 'Gregorian month of days scale' be explicit about how it divides each of the Gregorian months?  What do we do about the 'year of weeks scale' since the number of weeks in a year is really messy? 

I guess we need to discuss this.  I agree with Mark's concern here, but I don't know what we want to write.  And <expletive deleted> leap seconds make minute-of-seconds or day-of-seconds truly variable.  

* The wording of the Necessity seems like something a logician would write not something that makes business sense.  The phrase "If a finite time scale subdivides a time point," should not be needed since the Necessity is in the context of this verb concept.  (In any case, this Necessity will be rewritten if my point about missing roles is accepted.) 

Yes.  This is part of the above.

* I agree that this verb concept is related to 'time point converts to time point sequence on time scale' but I don't agree that this verb concept is a 'special case' of the latter.  This verb concept is about the definitional relationship between finite time scales and time points; whereas the other is about computing the conversion. 

The Beta text of this verb concept is broken.  The replacement text from Issue 17227 says: 
Definition:                             the time point is coextensive with the time point sequence 

Necessity:                              Each time point of the time point sequence is on the time scale. 

Possibility:                             The time point is an absolute time point or is a relative time point. 

Description:                          The time point and the time point sequence are two different ways to identify the same time intervals. 


It doesn't say anything about computation.  The purpose is to provide meaning to the idea of computing the referents of a time coordinate, yes.  The Beta text indicated that intent -- it was trying to say that the decomposition into time points was about identifying time periods.  But the mechanism is said here to involve the conversion to an equivalent sequence of time points.  The example for 17227: 

Example:                                 The time point that is indicated by the time coordinate January 2012 converts to the time point sequence 2012 day 1 through 2012 day 31 on the Gregorian days scale. 


shows that the intent is different from 'subdivides'.  'subdivides' is about converting January 2012 to the month-of-days; this is about converting it to a subsequence of 'day-of-year'.

But this takes us back to the idea above, that there are two different time point sequence ideas.  I think the 'converts to' idea is about locating the larger interval in a longer sequence of finer granularity intervals, as the large interval that is the hull of a subsequence, while 'subdivides' is about treating the larger time point as a sequence of consecutive time points that corresponds to sequences of consecutive smaller time intervals.  That is, 'converts to' is not about decomposing the time point and its corresponding time periods, it is about locating it in some other sequence; but subdivides is about decomposing the time point and its corresponding time periods.  

So I agree with Mark that 'subdivides' is not a special case of 'converts to', but we somehow have to be clear about the difference in intent in the definitions.  They both seem to say:  "time point on scale A is coextensive with time point sequence on scale B."  17227 is correct that that is what converts to means.  For 'subdivides' we have to talk about sequences of time intervals, somehow.

Regarding 17367: 
* I think that the OCL for the new axiom in 8.1.1 should read, as follows -- but need to consult the OCL book when I get home to be sure: 
OCL Constraint:        context: "time interval" 
                                   inv: "time interval"."time interval1 is proper part of time interval2"-->notEmpty() 

OK.  I will put that in the next draft, with a comment that says 'check this'.

* Why not wrap the new axiom in 8.1.6 into the definition of 'properly during'?  Why should it be a separate axiom? 
* I haven't provided the OCL for this new axiom because I think it instead should be a modification of the definitional OCL for 'properly during'. 

Well, 'properly during' is one of the Allen relations, and it is defined in terms of 'part of ' and 'before'.  'properly during' just says there is a proper part that is before it and one that is after it, which logically completes the partitioning of 'proper part': starts has no before, finishes has no after, and during has both.  What Mark suggests is that 'A is properly during B' could be defined as:  A is a proper part of B and there is a time interval C such that C starts B and C meets A, etc.  That does not clearly complete the partition.  To complete it, you would have to prove that:  If A does not start or finish B, then there is a C that starts B and meets A.   That is, if there is a C that is a proper part of B and is before A (i.e. A does not start B), then there is a C' that starts B and meets A.  And that is what the proposed axiom says, because you can't prove it from the other axioms.

In a similar way, the weak supplementation axiom says that for every proper part there is another proper part that does not overlap it.  So if A starts B, A has a supplement and the supplement must be after A.  But there is a 'start complement' axiom that says that if A starts B, there is a C that is met by A and finishes B -- the "maximal" supplement.  I don't think you can get these "maximal supplement" theorems from the axioms for 'part of' and 'before', precisely because we don't have strong supplementation:  If A is properly during B, then B-A is not a time interval.

* I think that what Fabian asked for is a different new axiom that says that every time interval has a proper part that starts/finishes it. 

Ah!  But those follow from the proposed axiom, together with the existing start-complement and finish-complement axioms.  E.g.
Theorem:  Every time interval has a proper part that starts it.
Proof:
If a time interval B has a proper part A, then (by the Allen partitioning), one of the following must be true: A starts B, A finishes B, A is properly during B.
Now, if A starts B, B has a proper part (A) that starts it.
If A finishes B, by the finish complement axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
If A is during B, by the proposed axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
So, if a time interval B has a proper part A, B has a proper part that starts B in all cases.  
By the no-smallest-interval axiom, every time interval B has some proper part A.  
So every time interval B has a proper part that starts B in all cases.  Q.E.D.
 
The nagging question is whether there might be a simpler solution than having these three complement axioms.  In particular, could we instead assert that every time interval has a proper part that starts it and a proper part that finishes it?  I think not, because there is no basis for relating an arbitrary starting part to an arbitrary finishing part.

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800

"The opinions expressed above do not reflect consensus of NIST, 
and have not been reviewed by any Government authority." 



-------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        OMG DateTimeVoc FTF <date-time-ftf@omg.org>, 
Date:        07/16/2012 07:23 PM 
Subject:        DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------



Per today's conference call, I attach the revised drafts for resolution 
of Issues
16689 - D0 should be quantified (added the UML object D0)
16951 - time point subdivision (see markup),
17367- no smallest time interval (1st draft, needs OCL)

For 16689, should we have defined a term like 'zero duration'?  Should 
that be the term and D0 the Synonym?

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800



[attachment "DTV Issue 17367- no smallest time interval-d1.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16689-D0 should be quantified.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16951-time point subdivision-d4.doc" deleted by Mark H Linehan/Watson/IBM] 





-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800





 DTV Issue 17367- no smallest time interval-d2.docx 


Disposition: Resolved
OMG Issue No:  16689
Title:	D0 Should be Quantified
Source:  Mark H. Linehan . IBM . mlinehan@us.ibm.com

Summary:
Clause 8.2.2 has several CLIF axioms that reference 'D0' but fail to quantify that variable.  They should each existentially quantify 'D0'.

Resolution:
In 8.2.2, D0 is declared to be an individual concept . a logical constant . under Axiom V.4.  The problem is that there is no CLIF rendition of this axiom, and there needs to be a theorem that D0 is unique.
In resolving this issue, the FTF noted that the CLIF .plus. operator must be defined between durations, because it is not the same as the .plus. operator for numbers.  And the closure axiom does not follow from the definition.

Revised Text:
1.  In clause 8.2.2, REPLACE Figure 8-11 with:

2.  In clause 8.2.2, in the entry for .duration3 = duration1 + duration2., DELETE the Note that reads:
Note:	Axiom V.1 (Addition is closed) is incorporated into this verb concept by definition.
and INSERT:
Note:	The following definition defines the CLIF duration addition function in terms of the verb concept.; The verb concept is primitive and has no formal definition.
CLIF Definition:	(forall ((d1 duration) (d2 duration) d3)
  (iff
    (= d3 (+ d1 d2))
    (and
      (duration d3)
      ("duration3 = duration1 + duration2"
         d3 d1 d2) )))
Axiom V.1 (Addition is closed): For all durations d1 and d2, there is a duration d3 such that d3 = d1 + d2.
Necessity:	For each duration1 and each duration2 there is some duration3 that equals duration1 plus duration2.
CLIF Axiom:	 (forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
3.  In clause 8.2.2, in Axiom V.4, in the entry for D0, before the Definition, INSERT:
Synonym:	zero duration 

4.  In clause 8.2.2, in Axiom V.4, in the entry for D0, after the Definition, INSERT:
CLIF Definition:	(exists (D0) (and
  (duration D0)
  (forall (d duration)
    (= (+ d D0) d)) ))
Note:	D0 is a duration that is the additive identity, and it is unique.  The uniqueness of D0 follows from the definition and the commutative axiom (V.3):  If there is some other Dx such that 
d + Dx = d for all durations d, then D0 + Dx = D0, but 
D0 + Dx = Dx + D0 and Dx + D0 = Dx, by definition of D0.

Disposition:	Resolved

To: date-time-ftf@omg.org, Stan@hendryxassoc.com
Subject: Re: DTV Issues 16689, 16951, 17367 proposed resolutions
X-KeepSent: A312519A:19F93632-85257A4A:0054ED08;
 type=4; name=$KeepSent
X-Mailer: Lotus Notes Release 8.5.3 September 15, 2011
From: Mark H Linehan <mlinehan@us.ibm.com>
Date: Sun, 29 Jul 2012 21:26:25 -0400
X-MIMETrack: Serialize by Router on D01MC604/01/M/IBM(Release 8.5.3 ZX853HP5|January 12, 2012) at
 07/29/2012 21:26:27,
        Serialize complete at 07/29/2012 21:26:27
X-Content-Scanned: Fidelis XPS MAILER
x-cbid: 12073001-6078-0000-0000-00000DAABC86


Regarding 16669 - I understand what you are doing with the "(= d3 (+ d1 d2))".  What I don't understand is why we need this.  We don't have such for other verb concepts where we define noun forms. 

17367 - looks good.  Minor formatting issue: double "OCL Constraint" captions for the final axiom. 


leap seconds -  I don't want to reopen the solution from 16680, which I think is perfectly adequate.  The Gregorian Calendar is defined in terms of UTC.  UTC gets shifted (compared to TAI) when leap seconds are added.  The calendar day gets longer by 1 leap second, but hour-of-day and minute-of-day does not change. 

--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        Mark H Linehan/Watson/IBM@IBMUS, 
Cc:        "date-time-ftf@omg.org" <date-time-ftf@omg.org>, "Stan@hendryxassoc.com" <Stan@hendryxassoc.com> 
Date:        07/27/2012 06:46 PM 
Subject:        Re: DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------



I attach the revised version of Issue 17367, incorporating the agreements.  (I didn't have change tracking on.  I added Mark's OCL and Fabian's corollaries.)

I attach a slightly revised version of 16689.  I hope we are done with this.

I need to do more work on 16951.

Mark H Linehan wrote: 
Regarding 16689:  Why isn't the  function (+ d1 d2) just a noun form of the predicate "duration3 = duration1 + duration2"? 
...
My point is that the standard SBVR approach is to define "+d1 d2" as a synonymous form of "duration3 equals duration1 plus duration2".  Actually, I see we already have this synonymous form. 

Given that, the proposed CLIF doesn't say anything that isn't already implied by having the synonymous form. 

Well, perhaps the function is implied by the predicate in SBVR, but in CLIF they are unrelated symbols unless we relate them.  In the same way, defining the association in the UML model doesn't define the operation.  That is all this does.  You have to read the CLIF to say: d3 is (+ d1 d2) exactly when ("duration3 equals duration1 plus duration2" d3 d1 d2).  (In a reasoner, one would "skolemize" the thing named (+ d1 d2) by inventing a d3 to be the result, i.e., (exists (d3))(= d3 (+ d1 d2)), and then this definition axiom turns "d3 =  structured name" into a proposition involving d1, d2, and d3.)

Regarding 16951:  I don't think we need to distinguish "time point sequence" from "sequence of time points".  I think these are just two views of the same thing: either the time interval that corresponds to the convex hull of the whole time point sequence, or a sequence of time intervals that correspond to the individual time points of the time point sequence.  I think the two verb concepts ('subdivides' and 'converts to') are two different ways of using the one general concept. 

EJB
OK, but my point is that those two 'views' see technically different extensions of a time point sequence.  The whole point of subdivision is to decompose the time intervals, not to see them as one big interval.  subdivides decomposes an X into Ys, converts composes Ys into an X. 

MHL: Yes, that's why I said one isn't a subtype of the other, but they are related.  I think we agree. 


Yes, we agree on that.  I am still a bit worried about what the extension of a time point sequence is.  The convex hull is in some sense equivalent to the sequence of component intervals, but it is not the same thing.
.  

MHL 

I don't think leap seconds have anything to do with this discussion.  Leap seconds involve displacing the UTC time scale, not adding seconds to calendar days.  BIPM is clear that 'day' is fixed at 86400 seconds. 

EJB
But the BIPM 'day' is a duration, a time unit.  A UTC day is a calendar day, and its length is variable, and the variation does not follow a named pattern like common year and leap year.  We don't cast 'leap seconds' as a kind of 'time offset' (from TAI to UTC), but that is what "displacing the UTC time scale" suggests.  It makes some sense.  The UTC rules are then rather like those of timezones -- some authority decides when to change from one time offset to another. We already have time offsets in hours and minutes; we could add seconds.  Is that a better approach than what we wrote?  

MHL
That's what we already decided and voted in issue 16680. Given that resolution, there's no reason to bring leap seconds into this "subdivides" discussion. 

Actually, I see that that resolution redefined the 'day of seconds scale' as "the finite time scale that subdivides each calendar day into at most 86 401 second of day".   So that resolution already started down the path of making these definitions acknowledge the varying number of x units in y time point.  Let's continue that. 


What we agreed to in 16680 is NOT to describe leap seconds as time offsets, but rather to agree that there are minutes of different lengths and days of different lengths.  Describing 'leap seconds' as time offsets is very different:  Every clock minute would be subdivided into exactly 60 seconds, and every calendar day into exactly 86400 seconds.  But every time UTC adds a leap second we use a different calendar with a different time offset from TAI.  In the same way, the US Eastern Time Zone does not have variable length days, it just sometimes uses the EST offset and sometimes uses the EDT offset.  This affects the duration of a 'day period', but not a calendar day.  What I am suggesting is that UTC is several different calendars with different time offsets from TAI -- each leap second they add defines a new calendar with a different time offset: "UTC as of <datetime>".

If we adopt that view of leap seconds, we can do what you suggest about the subdivisions:  common years and leap years have different subdivisions, March and April have different subdivisions, but none of them is variable.  Leap seconds are the only things that create truly variable subdivisions, and if we switch to a time offset model of leap seconds, the variable subdivisions disappear entirely. 



--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        Mark H Linehan/Watson/IBM@IBMUS, 
Cc:        "date-time-ftf@omg.org" <date-time-ftf@omg.org>, Stan Hendryx <stan@hendryxassoc.com> 
Date:        07/26/2012 01:19 PM 
Subject:        Re: DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------





Mark H Linehan wrote: 
Regarding 16689: 
* I don't see the value of this CLIF axiom; it doesn't seem to say anything.  The one proposed to go after axiom V1 seems sufficient. 
CLIF Definition:        (forall ((d1 duration) (d2 duration) d3)
 (iff
   (= d3 (+ d1 d2))
   (and
     (duration d3)
     ("duration3 = duration1 + duration2"
        d3 d1 d2) ))) 

This axiom defines the function (+ d1 d2).  Otherwise it is primitive, and not clearly related to the predicate "duration3 = duration1 + duration2".  Or at least, I think that is the case.  The proposed axiom for V1 says that the function is defined everywhere:
(forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
  
* I don't have a strong opinion about 'D0' versus 'zero duration'.  I don't see a lot of value in using the term 'zero duration' instead of 'D0'. 

In SBVR parlance, D0 is a symbol, 'zero duration' is a term.  Given that it is a term for something that is strictly a mathematical concept, it probably makes no difference.

Regarding 16951: 
* Editorial instruction #2 should make it clear that the new subsection has a regular section number, not the literal "9.4bis".  Something like "Immediately before clause 9.5, create a new subclause:", and renumber subclauses 9.5 and 9.6 as 9.6 and 9.7".  And then show "9.4bis" as "9.4". 

OK.

* I notice that all the uses of the 'subdivides' verb concept are of the form "<finite time scale> subdivides <time point> into <number> of <time point>".  Which makes me wonder whether the verb concept should have 4 roles rather than 2. 

Hmm.  I think the original verb was based on the idea that the subdivision was like hours and minutes -- the whole finite time scale.  But of course that was never true for month-of-days or year-of-days.  The subdivision really uses a time point sequence beginning with the origin index, which is what the proposed revised definition says.  But that 'time point sequence' idea may be wrong.  That is, I think a time point sequence is different from a sequence of time points, and 'subdivides' is about that difference.

Technically a sequence of time points corresponds to sequences of time intervals.  We say a 'time point sequence' corresponds to the one big interval that is the span (hull) of the sequence of intervals.  Now the 'one big interval' view is consistent with the idea that '2:00 to 4:00' indicates a time point sequence that corresponds to intervals that have a duration of two hours (or correctly 120 minutes).  But that is not what we mean by 'subdivides',  We mean treating the larger time point as a sequence of time points that corresponds to sequences of smaller time intervals, rather than to the hull of them.  This leads me to think that the term 'time point sequence' violates (Bernd Wenzel's) Law of Least Astonishment.  That is 'time point sequence' is not the same as 'sequence of time points'.

* There should be a Note that explains why we talk about a subsequence of the finite time scale.  The reason is that the subdivision of some kinds of time points into finite time scales is irregular.  Months are subdivided into 28-31 days and years are subdivided into 365 or 366 days. 

Agree.

* But, looking further, all of the uses of this verb concept talk about subdividing the "larger" time point into a fixed (not varying) number of "smaller" time points.  For example, the 'Gregorian year of days scale' is defined as "the finite time scale that subdivides âGregorian yearâ into 366 of âGregorian day of yearâ ".  Should it talk about subdividing leap years into 366 and common years into 365 'Gregorian day of year'?  Should the 'Gregorian month of days scale' be explicit about how it divides each of the Gregorian months?  What do we do about the 'year of weeks scale' since the number of weeks in a year is really messy? 

I guess we need to discuss this.  I agree with Mark's concern here, but I don't know what we want to write.  And <expletive deleted> leap seconds make minute-of-seconds or day-of-seconds truly variable.  

* The wording of the Necessity seems like something a logician would write not something that makes business sense.  The phrase "If a finite time scale subdivides a time point," should not be needed since the Necessity is in the context of this verb concept.  (In any case, this Necessity will be rewritten if my point about missing roles is accepted.) 

Yes.  This is part of the above.

* I agree that this verb concept is related to 'time point converts to time point sequence on time scale' but I don't agree that this verb concept is a 'special case' of the latter.  This verb concept is about the definitional relationship between finite time scales and time points; whereas the other is about computing the conversion. 

The Beta text of this verb concept is broken.  The replacement text from Issue 17227 says: 
Definition:                             the time point is coextensive with the time point sequence 

Necessity:                              Each time point of the time point sequence is on the time scale. 

Possibility:                             The time point is an absolute time point or is a relative time point. 

Description:                          The time point and the time point sequence are two different ways to identify the same time intervals. 


It doesn't say anything about computation.  The purpose is to provide meaning to the idea of computing the referents of a time coordinate, yes.  The Beta text indicated that intent -- it was trying to say that the decomposition into time points was about identifying time periods.  But the mechanism is said here to involve the conversion to an equivalent sequence of time points.  The example for 17227: 

Example:                                 The time point that is indicated by the time coordinate January 2012 converts to the time point sequence 2012 day 1 through 2012 day 31 on the Gregorian days scale. 


shows that the intent is different from 'subdivides'.  'subdivides' is about converting January 2012 to the month-of-days; this is about converting it to a subsequence of 'day-of-year'.

But this takes us back to the idea above, that there are two different time point sequence ideas.  I think the 'converts to' idea is about locating the larger interval in a longer sequence of finer granularity intervals, as the large interval that is the hull of a subsequence, while 'subdivides' is about treating the larger time point as a sequence of consecutive time points that corresponds to sequences of consecutive smaller time intervals.  That is, 'converts to' is not about decomposing the time point and its corresponding time periods, it is about locating it in some other sequence; but subdivides is about decomposing the time point and its corresponding time periods.  

So I agree with Mark that 'subdivides' is not a special case of 'converts to', but we somehow have to be clear about the difference in intent in the definitions.  They both seem to say:  "time point on scale A is coextensive with time point sequence on scale B."  17227 is correct that that is what converts to means.  For 'subdivides' we have to talk about sequences of time intervals, somehow.

Regarding 17367: 
* I think that the OCL for the new axiom in 8.1.1 should read, as follows -- but need to consult the OCL book when I get home to be sure: 
OCL Constraint:        context: "time interval" 
                                   inv: "time interval"."time interval1 is proper part of time interval2"-->notEmpty() 

OK.  I will put that in the next draft, with a comment that says 'check this'.

* Why not wrap the new axiom in 8.1.6 into the definition of 'properly during'?  Why should it be a separate axiom? 
* I haven't provided the OCL for this new axiom because I think it instead should be a modification of the definitional OCL for 'properly during'. 

Well, 'properly during' is one of the Allen relations, and it is defined in terms of 'part of ' and 'before'.  'properly during' just says there is a proper part that is before it and one that is after it, which logically completes the partitioning of 'proper part': starts has no before, finishes has no after, and during has both.  What Mark suggests is that 'A is properly during B' could be defined as:  A is a proper part of B and there is a time interval C such that C starts B and C meets A, etc.  That does not clearly complete the partition.  To complete it, you would have to prove that:  If A does not start or finish B, then there is a C that starts B and meets A.   That is, if there is a C that is a proper part of B and is before A (i.e. A does not start B), then there is a C' that starts B and meets A.  And that is what the proposed axiom says, because you can't prove it from the other axioms.

In a similar way, the weak supplementation axiom says that for every proper part there is another proper part that does not overlap it.  So if A starts B, A has a supplement and the supplement must be after A.  But there is a 'start complement' axiom that says that if A starts B, there is a C that is met by A and finishes B -- the "maximal" supplement.  I don't think you can get these "maximal supplement" theorems from the axioms for 'part of' and 'before', precisely because we don't have strong supplementation:  If A is properly during B, then B-A is not a time interval.

* I think that what Fabian asked for is a different new axiom that says that every time interval has a proper part that starts/finishes it. 

Ah!  But those follow from the proposed axiom, together with the existing start-complement and finish-complement axioms.  E.g.
Theorem:  Every time interval has a proper part that starts it.
Proof:
If a time interval B has a proper part A, then (by the Allen partitioning), one of the following must be true: A starts B, A finishes B, A is properly during B.
Now, if A starts B, B has a proper part (A) that starts it.
If A finishes B, by the finish complement axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
If A is during B, by the proposed axiom, there is a C that starts B and meets A.  So B has a proper part (C) that starts it.
So, if a time interval B has a proper part A, B has a proper part that starts B in all cases.  
By the no-smallest-interval axiom, every time interval B has some proper part A.  
So every time interval B has a proper part that starts B in all cases.  Q.E.D.
 
The nagging question is whether there might be a simpler solution than having these three complement axioms.  In particular, could we instead assert that every time interval has a proper part that starts it and a proper part that finishes it?  I think not, because there is no basis for relating an arbitrary starting part to an arbitrary finishing part.

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800

"The opinions expressed above do not reflect consensus of NIST, 
and have not been reviewed by any Government authority." 



-------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        OMG DateTimeVoc FTF <date-time-ftf@omg.org>, 
Date:        07/16/2012 07:23 PM 
Subject:        DTV Issues 16689, 16951, 17367 proposed resolutions 



--------------------------------------------------------------------------------



Per today's conference call, I attach the revised drafts for resolution 
of Issues
16689 - D0 should be quantified (added the UML object D0)
16951 - time point subdivision (see markup),
17367- no smallest time interval (1st draft, needs OCL)

For 16689, should we have defined a term like 'zero duration'?  Should 
that be the term and D0 the Synonym?

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800



[attachment "DTV Issue 17367- no smallest time interval-d1.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16689-D0 should be quantified.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16951-time point subdivision-d4.doc" deleted by Mark H Linehan/Watson/IBM] 



-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800


[attachment "DTV Issue 17367- no smallest time interval-d2.docx" deleted by Mark H Linehan/Watson/IBM] [attachment "DTV Issue 16689-D0 should be quantified-d2.docx" deleted by Mark H Linehan/Watson/IBM] 
Date: Mon, 30 Jul 2012 18:45:51 -0400
From: Ed Barkmeyer <edbark@nist.gov>
Reply-To: <edbark@nist.gov>
Organization: NIST
User-Agent: Thunderbird 2.0.0.23 (Windows/20090812)
To: OMG DateTimeVoc FTF <date-time-ftf@omg.org>
Subject: DTV issue 16689 - D0 should be quantified (and other fixes to 8.2.2
 axioms)
X-NISTMEL-MailScanner-Information: Please contact postmaster@mel.nist.gov for more information
X-NISTMEL-MailScanner-ID: q6UMjuOj021106
X-NISTMEL-MailScanner: Found to be clean
X-NISTMEL-MailScanner-SpamCheck: 
X-NISTMEL-MailScanner-From: edbark@nist.gov
X-NISTMEL-MailScanner-Watermark: 1344293157.32236@3nNTFt69CWKDluYTWZPi4w
X-Spam-Status: No


I attach what I hope is the final revision of DTV Issue 16689 per today's conference call.


-Ed


-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800







 DTV Issue 16689-D0 should be quantified-d3.docx <Down>
<Down>
<Down>
Disposition: Resolved
OMG Issue No:  16689
Title:	D0 Should be Quantified
Source:  Mark H. Linehan . IBM . mlinehan@us.ibm.com

Summary:
Clause 8.2.2 has several CLIF axioms that reference 'D0' but fail to quantify that variable.  They should each existentially quantify 'D0'.

Resolution:
In 8.2.2, D0 is declared to be an individual concept . a logical constant . under Axiom V.4.  The problem is that there is no CLIF rendition of this axiom, and there needs to be a theorem that D0 is unique.
In resolving this issue, the FTF noted that the CLIF .plus. operators (+, ., *) must be defined between durations, because it isthey are not the same as the .plus. operators for numbers.  And the closure axiom does not follow from the definition.

Revised Text:
1.  In clause 8.2.2, REPLACE Figure 8-11 with:

2.  In clause 8.2.2, in the entry for .duration3 = duration1 + duration2., DELETE the Note that reads:
Note:	Axiom V.1 (Addition is closed) is incorporated into this verb concept by definition.
and INSERT:
Note:	The following definition defines the CLIF duration addition function in terms of the verb concept. The verb concept is primitive and has no formal definition.
CLIF Definition:	(forall ((d1 duration) (d2 duration) d3)
  (iff
    (= d3 (+ d1 d2))
    (and
      (duration d3)
      ("duration3 = duration1 + duration2"
         d3 d1 d2) )))
Axiom V.1 (Addition is closed): For all durations d1 and d2, there is a duration d3 such that d3 = d1 + d2.
Necessity:	For each duration1 and each duration2 there is some duration3 that equals duration1 plus duration2.
CLIF Axiom:	 (forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
3.  In clause 8.2.2, in Axiom V.4, in the entry for D0, before the Definition, INSERT:
Synonym:	zero duration 

4.  In clause 8.2.2, in Axiom V.4, in the entry for D0, after the Definition, INSERT:
CLIF Definition:	(exists (D0) (and
  (duration D0)
  (forall (d duration)
    (= (+ d D0) d)) ))
Note:	D0 is a duration that is the additive identity, and it is unique.  The uniqueness of D0 follows from the definition and the commutative axiom (V.3):  If there is some other Dx such that 
d + Dx = d for all durations d, then D0 + Dx = D0, but 
D0 + Dx = Dx + D0 and Dx + D0 = Dx, by definition of D0.
5.  In clause 8.2.2, in the entry for duration3 = duration1 . duration2, after the Example paragraph, INSERT:
CLIF Definition:	(forall ((d1 duration) (d2 duration) d3)
  (iff
    (= d3 (. d1 d2))
    (and
      (duration d3)
      ("duration3 = duration1 . duration2"
         d3 d1 d2) )))

6.  In clause 8.2.2, in the entry for duration2 = number times duration1, after the Example paragraph, INSERT:
CLIF Definition:	(forall ((d1 duration) (n number))
  (iff
    (= d2 (* n d1))
    (and
      (duration d2)
      ("duration2 = number * duration1"
         n d1) )))


Disposition:	Resolved

To: date-time-ftf@omg.org
Subject: Re: DTV issue 16689 - D0 should be quantified (and other fixes to 8.2.2
 axioms)
X-KeepSent: CC68E6C3:850CF4D0-85257A4E:0051CD06;
 type=4; name=$KeepSent
X-Mailer: Lotus Notes Release 8.5.3 September 15, 2011
From: Mark H Linehan <mlinehan@us.ibm.com>
Date: Thu, 2 Aug 2012 10:54:23 -0400
X-MIMETrack: Serialize by Router on D01MC604/01/M/IBM(Release 8.5.3 ZX853HP5|January 12, 2012) at
 08/02/2012 10:54:24
X-Content-Scanned: Fidelis XPS MAILER
x-cbid: 12080215-5112-0000-0000-00000AAA06A9


I made one very minor change, which is to add 'd2' as a quantified variable in the final axiom.   
--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        OMG DateTimeVoc FTF <date-time-ftf@omg.org>, 
Date:        07/30/2012 06:46 PM 
Subject:        DTV issue 16689 - D0 should be quantified (and other fixes to 8.2.2 axioms) 

--------------------------------------------------------------------------------



I attach what I hope is the final revision of DTV Issue 16689 per 
today's conference call.

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800



[attachment "DTV Issue 16689-D0 should be quantified-d3.docx" deleted by Mark H Linehan/Watson/IBM] 


 Date-Time Issue 16689 -D0 should be quantified.docx <Down>
<Down>
Disposition: Resolved
OMG Issue No:  16689
Title:	D0 Should be Quantified
Source:  Mark H. Linehan . IBM . mlinehan@us.ibm.com

Summary:
Clause 8.2.2 has several CLIF axioms that reference 'D0' but fail to quantify that variable.  They should each existentially quantify 'D0'.

Resolution:
In 8.2.2, D0 is declared to be an individual concept . a logical constant . under Axiom V.4.  The problem is that there is no CLIF rendition of this axiom, and there needs to be a theorem that D0 is unique.
In resolving this issue, the FTF noted that the CLIF .plus. operators (+, ., *) must be defined between durations, because it isthey are not the same as the .plus. operators for numbers.  And the closure axiom does not follow from the definition.

Revised Text:
1.  In clause 8.2.2, REPLACE Figure 8-11 with:

2.  In clause 8.2.2, in the entry for .duration3 = duration1 + duration2., DELETE the Note that reads:
Note:	Axiom V.1 (Addition is closed) is incorporated into this verb concept by definition.
and INSERT:
Note:	The following definition defines the CLIF duration addition function in terms of the verb concept. The verb concept is primitive and has no formal definition.
CLIF Definition:	(forall ((d1 duration) (d2 duration) d3)
  (iff
    (= d3 (+ d1 d2))
    (and
      (duration d3)
      ("duration3 = duration1 + duration2"
         d3 d1 d2) )))
Axiom V.1 (Addition is closed): For all durations d1 and d2, there is a duration d3 such that d3 = d1 + d2.
Necessity:	For each duration1 and each duration2 there is some duration3 that equals duration1 plus duration2.
CLIF Axiom:	 (forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
3.  In clause 8.2.2, in Axiom V.4, in the entry for D0, before the Definition, INSERT:
Synonym:	zero duration 

4.  In clause 8.2.2, in Axiom V.4, in the entry for D0, after the Definition, INSERT:
CLIF Definition:	(exists (D0) (and
  (duration D0)
  (forall (d duration)
    (= (+ d D0) d)) ))
Note:	D0 is a duration that is the additive identity, and it is unique.  The uniqueness of D0 follows from the definition and the commutative axiom (V.3):  If there is some other Dx such that 
d + Dx = d for all durations d, then D0 + Dx = D0, but 
D0 + Dx = Dx + D0 and Dx + D0 = Dx, by definition of D0.
5.  In clause 8.2.2, in the entry for duration3 = duration1 . duration2, after the Example paragraph, INSERT:
CLIF Definition:	(forall ((d1 duration) (d2 duration) d3)
  (iff
    (= d3 (. d1 d2))
    (and
      (duration d3)
      ("duration3 = duration1 . duration2"
         d3 d1 d2) )))

6.  In clause 8.2.2, in the entry for duration2 = number times duration1, after the Example paragraph, INSERT:
CLIF Definition:	(forall ((d1 duration) (n number) d2)
  (iff
    (= d2 (* n d1))
    (and
      (duration d2)
      ("duration2 = number * duration1"
         n d1) )))


Disposition:	Resolved

<Down>
<Down>
Date: Thu, 2 Aug 2012 18:55:02 -0400
From: Ed Barkmeyer <edbark@nist.gov>
Reply-To: <edbark@nist.gov>
Organization: NIST
User-Agent: Thunderbird 2.0.0.23 (Windows/20090812)
To: Mark H Linehan <mlinehan@us.ibm.com>
CC: "date-time-ftf@omg.org" <date-time-ftf@omg.org>
Subject: Re: DTV issue 16689 - D0 should be quantified (and other fixes to
 8.2.2 axioms)
X-NISTMEL-MailScanner-Information: Please contact postmaster@mel.nist.gov for more information
X-NISTMEL-MailScanner-ID: q72Mt7Kr024836
X-NISTMEL-MailScanner: Found to be clean
X-NISTMEL-MailScanner-SpamCheck: 
X-NISTMEL-MailScanner-From: edbark@nist.gov
X-NISTMEL-MailScanner-Watermark: 1344552908.90431@ezKbtyCLLolbF4PUqxHTJw
X-Spam-Status: No


I accepted Mark's change, and then I realized that, having defined the CLIF functions, we can greatly simplify Axiom v.7.  So I added that change to the text.   

Is it soup yet?

-Ed

Mark H Linehan wrote: 
I made one very minor change, which is to add 'd2' as a quantified variable in the final axiom.   
--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        OMG DateTimeVoc FTF <date-time-ftf@omg.org>, 
Date:        07/30/2012 06:46 PM 
Subject:        DTV issue 16689 - D0 should be quantified (and other fixes to 8.2.2 axioms) 

--------------------------------------------------------------------------------



I attach what I hope is the final revision of DTV Issue 16689 per 
today's conference call.

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800



[attachment "DTV Issue 16689-D0 should be quantified-d3.docx" deleted by Mark H Linehan/Watson/IBM] 




 DTV Issue 16689-D0 should be quantified-d4.docx 
Disposition: Resolved
OMG Issue No:  16689
Title:	D0 Should be Quantified
Source:  Mark H. Linehan . IBM . mlinehan@us.ibm.com

Summary:
Clause 8.2.2 has several CLIF axioms that reference 'D0' but fail to quantify that variable.  They should each existentially quantify 'D0'.

Resolution:
In 8.2.2, D0 is declared to be an individual concept . a logical constant . under Axiom V.4.  The problem is that there is no CLIF rendition of this axiom, and there needs to be a theorem that D0 is unique.
In resolving this issue, the FTF noted that the CLIF operators (+, ., *) must be defined between durations, because they are not the same as the operators for numbers.  And the closure axiom does not follow from the definition.

Revised Text:
1.  In clause 8.2.2, REPLACE Figure 8-11 with:

2.  In clause 8.2.2, in the entry for .duration3 = duration1 + duration2., DELETE the Note that reads:
Note:	Axiom V.1 (Addition is closed) is incorporated into this verb concept by definition.
and INSERT:
Note:	The following definition defines the CLIF duration addition function in terms of the verb concept. The verb concept is primitive and has no formal definition.
CLIF Definition:	(forall ((d1 duration) (d2 duration) d3)
  (iff
    (= d3 (+ d1 d2))
    (and
      (duration d3)
      ("duration3 = duration1 + duration2"
         d3 d1 d2) )))
Axiom V.1 (Addition is closed): For all durations d1 and d2, there is a duration d3 such that d3 = d1 + d2.
Necessity:	For each duration1 and each duration2 there is some duration3 that equals duration1 plus duration2.
CLIF Axiom:	 (forall ((d1 duration) (d2 duration))
  (exists (d3 duration) 
    (= d3 (+ d1 d2)) )))
3.  In clause 8.2.2, in Axiom V.4, in the entry for D0, before the Definition, INSERT:
Synonym:	zero duration 

4.  In clause 8.2.2, in Axiom V.4, in the entry for D0, after the Definition, INSERT:
CLIF Definition:	(exists (D0) (and
  (duration D0)
  (forall (d duration)
    (= (+ d D0) d)) ))
Note:	D0 is a duration that is the additive identity, and it is unique.  The uniqueness of D0 follows from the definition and the commutative axiom (V.3):  If there is some other Dx such that 
d + Dx = d for all durations d, then D0 + Dx = D0, but 
D0 + Dx = Dx + D0 and Dx + D0 = Dx, by definition of D0.
5.  In clause 8.2.2, in the entry for duration3 = duration1 . duration2, after the Example paragraph, INSERT:
CLIF Definition:	(forall ((d1 duration) (d2 duration) d3)
  (iff
    (= d3 (. d1 d2))
    (and
      (duration d3)
      ("duration3 = duration1 . duration2"
         d3 d1 d2) )))

6.  In clause 8.2.2, in the entry for duration2 = number times duration1, after the Example paragraph, INSERT:
CLIF Definition:	(forall ((d1 duration) (n number) d2)
  (iff
    (= d2 (* n d1))
    (and
      (duration d2)
      ("duration2 = number * duration1"
         n d1) )))

7.  In clause 8.2.2, under Axiom V.7, REPLACE the CLIF Axiom paragraph:
CLIF Axiom:	(forall ((d1 duration) (d2 duration) 
 (n1 number))
(exists ((d3 duration) (d4 duration) 
 (d5 duration) (d6 duration) (d7 duration))
(if (and
     (+ d1 d2 d3)
     (* n1 d3 d4)
     (* n1 d1 d5)
     (* n1 d2 d6)
     (+ d5 d6 d7))
   (= d4 d7))))
with:
CLIF Axiom:	(forall ((d1 duration) (d2 duration) 
        (d3 duration) (n1 number))
(if (= d3 (* n1 (+ d1 d2)))
    (= d3 (+ (* n1 d1) (* n1 d2))) )


Disposition:	Resolved

<Down>
To: date-time-ftf@omg.org
Subject: Re: DTV issue 16689 - D0 should be quantified (and other fixes to 8.2.2
 axioms)
X-KeepSent: D0A0CF0C:FEE3EA1F-85257A4F:0043B501;
 type=4; name=$KeepSent
X-Mailer: Lotus Notes Release 8.5.3 September 15, 2011
From: Mark H Linehan <mlinehan@us.ibm.com>
Date: Fri, 3 Aug 2012 08:20:00 -0400
X-MIMETrack: Serialize by Router on D01ML604/01/M/IBM(Release 8.5.3HF266 | January 13, 2012) at
 08/03/2012 08:20:01,
        Serialize complete at 08/03/2012 08:20:01
X-Content-Scanned: Fidelis XPS MAILER
x-cbid: 12080312-7182-0000-0000-00000229619F


This looks good to me. 
--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        Mark H Linehan/Watson/IBM@IBMUS, 
Cc:        "date-time-ftf@omg.org" <date-time-ftf@omg.org> 
Date:        08/02/2012 06:55 PM 
Subject:        Re: DTV issue 16689 - D0 should be quantified (and other fixes to 8.2.2 axioms) 

--------------------------------------------------------------------------------



I accepted Mark's change, and then I realized that, having defined the CLIF functions, we can greatly simplify Axiom v.7.  So I added that change to the text.   

Is it soup yet?

-Ed

Mark H Linehan wrote: 
I made one very minor change, which is to add 'd2' as a quantified variable in the final axiom.   
--------------------------------
Mark H. Linehan
STSM, IBM Research 



From:        Ed Barkmeyer <edbark@nist.gov> 
To:        OMG DateTimeVoc FTF <date-time-ftf@omg.org>, 
Date:        07/30/2012 06:46 PM 
Subject:        DTV issue 16689 - D0 should be quantified (and other fixes to 8.2.2 axioms) 

--------------------------------------------------------------------------------



I attach what I hope is the final revision of DTV Issue 16689 per 
today's conference call.

-Ed

-- 
Edward J. Barkmeyer                        Email: edbark@nist.gov
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                Cel: +1 240-672-5800



[attachment "DTV Issue 16689-D0 should be quantified-d3.docx" deleted by Mark H Linehan/Watson/IBM] 
[attachment "DTV Issue 16689-D0 should be quantified-d4.docx" deleted by Mark H Linehan/Watson/IBM]