Re: Can Motion 8.02 support proofs of correctness?

[John Pryce <j.d.pryce@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