[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.