Re: Can Motion 8.02 support proofs of correctness?

[Arnold Neumaier <Arnold.Neumaier@xxxxxxxxxxxx>]

John Pryce wrote:

> Motion 8 §1.2 says that a decoration trit "characterizes part of the 
> history of a computation", which is fine by me. Every boolean attribute 
> of a segment of computation history, that I can think of, can be 
> regarded as an event. So a trit is supposed to say "between points A and 
> B of the history, event E did happen (+); or didn't happen (-); or I'm 
> not sure if it happened or not (0)".
>
> But 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;

Maybe you can suggest a formulation that is less ambiguous.


Arnold Neumaier