[Prev][Next][Index][Thread]

comp adequacy and soundness

I have been looking at the denotational semantics of syntactically
restricted subsets of Idealized Algol like that proposed by J. Reynolds
in his 1978 POPL paper "Syntactic Control of Interference". Some
interesting semantic problems have popped up, one of which I would
like to share.

        Let me follow Albert on some terminology:
 - a denotational semantics [[.]] is COMPUTATIONALLY ADEQUATE iff
for all closed programs P, [[P]] = bottom iff P fails to terminate
 - two terms M and N are observationally equivalent (==) iff
for all program contexts C[.], C[M] terminates iff C[N] does.

        Of course, here we have some operational semantics
in mind which defines "termination".  Also, call a denotational
semantics SOUND if semantic equality implies observation
equivalence. In studying restricted languages, I have found
a counter-example to the assertion

 (*) Any computationally adequate semantics is sound.

        Note that, implicit in the definition of observation
equivalence is that if M==N, we have

 (**) for all C[.] C[M] is well-formed iff C[N] is.

This is needed to ensure that equivalent terms can be interchanged
in any context.

        I don't know if (*) is widely held, but let me push on and
explain why it fails.

        Consider L to be the set of well-formed phrases of
some language, and let RL be some syntactically restricted
subset of L. Moreover, suppose L comes with some operational
semantics which cuts down to an operational semantics for RL;
i.e. an RL program is executed just as if it were an L-program.
>From this assumption it follows that

Lemma 1: Any computationally adequate denotational semantics for L
cuts down to a computationally adequate denotational demantics for
RL.

        Now, (*) might fail for the restricted language RL just because
there may be 2 well-formed phrases M and N that are observationally
equivalent in L, but not in RL: the syntactic restriction on RL
might force (**) to fail for M and N, even though they behave
equivalently in all program contexts where both are defined. So,
any adequate model for L which equates M and N will be
adequate for RL (Lemma 1) but unsound wrt observation equivalence
in RL.

        For a concrete example, let us (informally) imagine a subset of
idealized Algol with application restricted so that there is never any aliasing
between different formal parameters of procedures. I will allow "tagged"
products, much as in the restricted language of Reynolds, so aliasing
is present but only between distinct elements from the same collection.
A term M of idealized Algol  is well-formed in the restricted language
iff there exists a program context C[.] such that C[M] has no aliasing
of formal parameters. Execution of a well-formed program in the
restricted language is defined exactly as when it is thought of
as an Idealized Algol program.  Let

 A = (lambda p:PI(a:int,b:int). ((lambda x.lambda y. x:=y+1) p.a p.b))
and
 B = (lambda p:PI(a:int,b:int).  p.a:=p.b+1)

A and B are observationally equivalent in Idealized Algol, and are
semantically equal in the models of, say, Oles, Tennent, and
Meyer and Sieber (extended to cover tagged products). Consider, however,
the context

 C[.] = new x in
             x:=2; [.] <x,x> end

Here, the <> braces say that what is enclosed is part of a product and
PI tells us that the type is a product. The dot notation "p.a" is a
projection to the "a" component of p. C[B] is well-formed in the restricted
language while C[A] is not. This is because p.a and p.b are not formal
parameters in B, so the restriction isn't violated. In A, however, the
formal parameters x and y from the innermost lambda-expression are
aliases in C[A], so C[A] isn't well-formed.  This shows that A and B
are not observationally equivalent in the restricted language, even though
they can be semantically equal in an adequate semantics, by
Lemma 1 above. Therefore, the assertion (*) fails for the restricted language.

        I don't know if the potential unsoundness of adequate
models has been mentioned before, or is well-known, but the consequences
should be clear independently of whether or not one has sympathy for the
kind of restrictions described above. In basing ,say, program-proving rules
or code transformations on an adequate semantics one must be careful
to make sure that the semantics is sound, it is not a given. While
the failure of (*) for a language may point out some lack of uniformity,
it should be noted that in many REAL programming languages, such as
FORTRAN, EUCLID, and TURING, there are syntactic restrictions which
would make the validity of (*) questionable.

        As for general conditions on a language to make (*) hold,
I can suggest that the language must be "suitably uniform"
so as to guarantee that (**) holds for any two terms that are
semantically equal. Most theoretical "idealized" languages have
this kind of uniformity, but I don't know exactly what "suitably uniform"
should mean in general.

Regards -- Peter