[Prev][Next][Index][Thread]
Re: specification logic and call by name
Kurt: I'll go along with value phrases being IMPORTANT, not just
CONVENIENT. But I don't see that the "questionable" axioms are
unnecessary with value phrases. A typical example of the use of
Strong Constancy is with binary search, where the assertion that is
"factored out" of the pre and post-conditions is that the array being
searched is sorted; this is clearly state-dependent. And Reynolds'
example of Non-Interference Composition also involves a state-dependent
expression.
In fact, I believe that the possible-world idea behind the
"questionable" axioms may be even more necessary in specification logic
than Reynolds thought. One problem is with the non-interference
decomposition axioms for HIGHER-ORDER phrases, such as
G#P1 & G#P2 => G#(P1 op P2)
when G is of type, say, comm->comm. I can't see that ANY natural
interpretation of non-interference can validate this, if one uses the
definition G#P == all C:comm. C#P => G(C)#P. One needs
C#(P1 op P2) => C#Pi ! The only avenue I see is to replace those axioms
by axioms that, in effect, incorporate C#(P1 op P2) => C#Pi as an
assumption to HOARE-TRIPLE reasoning, much like Reynolds'
Non-interference Composition axiom. But this is very speculative.
Are there languages with deferred evaluation and state-independent
value phrases? Of course: any lazily-evaluated functional language,
such as Miranda. But such languages don't have state-dependent
expressions and commands. I don't see why a language can't have both.
Note, however, that in Reynolds' framework, there cannot be a
coercion from (state-dependent) expressions to value phrases, because
the resulting value must depend on the current state, and not just
on the meaning of the expression; of course, a coercion the other way
is not a problem.
Small point: I think the specification of P in your example
should have had the form
all Q. (all c. {.} Q {.} ) => (all c. {.} P(Q) {.} )
This probably doesn't affect your argument.
---Regards, Bob.