Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

Re: Can Motion 8.02 support proofs of correctness?

Dan Zuras Intervals wrote:

Cc: stds-1788 <stds-1788@xxxxxxxxxxxxxxxxx>
From: John Pryce <j.d.pryce@xxxxxxxxxxxx>
Subject: Re: Can Motion 8.02 support proofs of correctness?
Date: Sat, 31 Oct 2009 20:49:37 +0000
To: Arnold Neumaier <Arnold.Neumaier@xxxxxxxxxxxx>

Arnold

On 30 Oct 2009, at 17:19, Arnold Neumaier wrote:

John Pryce wrote:

... of the candidate trits in 3.4:
  Valid
  Defined
  Continuous
  Tight
  Bounded
  Standard
  Empty
  Entire
only the first four are attributes of a segment of computation history. Surely the others are attributes of the individual interval? Or is "Bounded" about the event "all the intervals produced (or used?) within the given segment were bounded"? -- that doesn't seem very useful. 
The interval [0,Inf] can have the trit PossiblyBounded or NotBounded
depending on its history. Thus it contains history-dependent information. (The same can occur for any of the last four cases.) 
More was not intended to be said here;
Ah yes. I see your point. [0,Inf] could also have the trit IsBounded surely, as in 
   xx = interval(0,MaxReal);
   yy = xx + xx;
where yy is now [0,Inf] but we know for sure that yy is bounded?

John


	Actually, I have been interpreting all of these attributes
	as indications of a computation's history.  (That, is the
	history of the computation of THIS result & no other.
	Just to lay to rest any issue of possible contamination
	by global flags.)

	But this discussion suggests to me a way of possibly
	reducing the ambiguity of this interpretation.

	My former thinking was that the interpretation of any
	given attribute is "This attribute {is, is not, might be}
	true for this interval or any in its history."

	But consider that the 'might be' case could change that
	interpretation to one of:
		IsTrue:   This attribute is true for this interval.
		IsNot:    This attribute is not true for this
			interval.
		Possibly: This attribute is true for some interval
			in the history of the computation of this
			interval or might be true for this interval.
Intended was that the interpretation of each trit holds for the particular variable enclosed in the current interval because of its history. Thus nothing is said about the status of intermediate results, except that these must be such that they guarantee that the interpretation of the present trit is correct for the present variable. 
This is the only sense in which trits are history-dependent.


Arnold Neumaier