Re: Can Motion 8.02 support proofs of correctness?
> 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.
I believe that can be made to apply to all our proposed
attributes & might help in the interpretation of their
meaning. Both for implementers & users.
There would have to be a priority of sorts among the states
in order to preserve the history of the computation & still
report the correct information for this interval. I can
see a framework for that but I haven't worked it out in my
head at the moment. Some of the attribute names may have
to be changed if the rule is to remain consistent.
I will work on that if this notion appeals to any of you.
Do you think this approach has any merit?
Yours,
Dan
P.S. - Never mind about the priority problem. I just worked
it out. The state transition diagram should be:
State Condition New State
----- --------- ---------
Not Attr happens True
Not Doesn't happen Not
Not Might Be True Might
True Attr happens True
True Doesn't happen Might
True Might Be True Might
Might Attr happens True
Might Doesn't happen Might
Might Might Be True Might
Some of the attribute names may have to be changed in order
to properly track what we are really interested in. So, for
example, you might want to change the name of 'bounded' to
'unbounded' so you can keep a record of past overflows.
Things like that.
The virgin state would be 'Not True' & computations get to
whittle away at that as they proceed.
I know, mixed metaphors. That's what I get for doing a bit
of technical thinking on a Saturday afternoon. :-)