[Prev][Next][Index][Thread]
313 lines about full abstraction from Stoughton and Meyer
Date: Tue, 5 Apr 88 13:47:18 BST
From: allen <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:allen@csta.uucp (Allen Stoughton)>
To: meyer <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:meyer@theory.lcs.mit.edu>
Subject: Adequacy, Full Abstraction and Contextual Full Abstraction
Albert,
Glancing through your paper "Semantic Paradigms: Notes for an Invited
Lecture", it became clear to me that you misunderstand what I use the term
"full abstraction" to mean in my monograph ("Fully abstract models of
programming languages", Pitman/Wiley, 1988). You say on page 6 that:
One warning though: Stoughton follows what I consider the unfortunate
terminology of (Hennessy and Plotkin, Full abstraction for a simple
parallel programming language) and calls "full abstraction" a property
that is actually equivalent to what I call adequacy---his "contextual
full abstraction" is my full abstraction.
Informally, I say (page 2) that a model is fully abstract wrt a notion
of program equivalence iff it identifies exactly the equivalent terms.
Program equivalences (page 1) are substitutive equivalence relations
(or congruences); typically, two terms are defined to be equivalent iff
they have the same behaviour in all program contexts. Hennessy and Plotkin,
in the paper mentioned above, also mean by "full abstraction" that two terms
have the same meaning in the model iff they have the same behaviour in
all program contexts, which in their case means in all contexts.
Thus my and Hennessy/Plotkin's notion of full abstraction seems to
coincide with your usage of the term, and to be different from what
you call adequacy.
"Contextual full abstraction" is the generalization of full abstraction
>from ordinary terms to contexts, i.e., to derived operators. Here one
demands that any two derived operators will be interpreted as the same
derived operation in the model iff they have the same behaviour when filled
with arbitrary terms in all program contexts. For a language like PCF
with a binding mechanism for identifiers of all types or sorts, contextual
and ordinary full abstraction will coincide (assuming that models are required
to be combinatory algebras), but this may not be true for languages like
Hennessy/Plotkin's parallel programming language which lack such a
binding mechanism.
In summary, we mean the same thing by "full abstraction", and "contextual
full abstraction" is (depending upon the language considered) a stronger
requirement.
Looking forward to your reply. You can send this out on the mail lists if
you wish.
Allen
---------------------------------------------
Date: Fri, 8 Apr 88 13:25:33 EST
From: meyer
To: allen <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:allen@csta.uucp>
In-reply-to: allen's message of Fri, 8 Apr 88 18:19:36 BST <8804081719.AA15049@sun.uucp>
Subject: Full abstraction and ....
....
Responding briefly now to your email of 5 April, I don't think I
misunderstood you this time, but I certainly haven't made myself clear. I'm
in the midst of preparing an expansion of point 1 below which I will send
asap. Then I'll send both your 5 April comment and my response to TYPES and
LOGIC.
Regards, A.
----------------
Date: Wed, 30 Mar 88 10:45:56 EST
From: meyer
To: jcm@ra.stanford.edu
In-reply-to: John Mitchell's message of Tue, 29 Mar 88 12:10:06 PST <8803292010.AA09966@ra.stanford.edu>
Subject: LICS88 paper
cc: stavros@ibm.com, bard, riecke, lalita
Thanks for your remarks. I agree that the discussion of full abstraction
needs more work; I hope I'll have time to make the improvement you suggest in
the TM version of the paper---which I might distribute at LICS if it's
merited. Actually there were a few more remarks I regret not having had time
to put in, and I'll take this opportunity to make some notes for myself which
you're welcome to read:
1. Adequacy is closely related---in ways which merit brief spelling out
in the paper---to semantic equality and obs-cong coinciding on CLOSED terms
of OBSERVABLE type. full abstraction is when they coincide on OPEN
terms---once they're open, it generally doesn't matter whether one looks at
observable or all types.
2. Full abstraction corresponds to ``reduced'' automata or ``final''
algebras. The elements of the domains correspond to automaton states, the
output of a state is its observable equivalence (not congruence) class,
e.g., whether or not it is 0, the ``inputs'' are the given operations of the
expression language, and ``input sequences'' are taken to be compositions of
algebra operations, viz., unary operations DEFINABLE by expressions.
(Higher-order lambda calculus fits this setup if viewed simply as a
multi-sorted algebra.) An automaton is reduced iff any two states are
distinguishable by some input sequence.
I found it interesting that this correspondence actually highlights
two versions of full abstraction: the general version above says that ANY
PAIR of distinct elements must be distinguishable by a DEFINABLE OPERATION.
A weaker condition says merely that any pair of DEFINABLE ELEMENTS must be
distinguishable by a definable operation; call this full-abs-for-definables.
Plotkin's results (and those in Appendix A of my paper with Stavros) yield
general full abstraction via showing that all finite elements are definable.
Wadsworth's results yield f-a-for-defbles in the pure untyped lambda calculus
observing head normal forms; general full-abs does not hold in the Wadsworth
setup, and a quite different Bohm-tree style proof is needed.
3. There is a whole further discussion I considered including highlighting
the fact that observational congruence should be understood to be
parameterized by the choice of observations made AND the choice of contexts
considered. The paper currently looks only at choices of
observations---observable ``numerals'', observable termination, termination
of arbitrary terms.
Allowing smaller or larger contexts than those of the kernel expression
language leads to another a series of issues concerning conservative
extension of theories and corresponding faithful embeddings of domains. For
example, there are (I thought we had some two weeks ago anyway) two untyped
terms with the SAME most general ML typing which are obscong wrt to all
TYPABLE contexts, but NOT wrt to an untyped context (observing nondivergence,
say).
This example highlights for me the contrast between trying to understand ML
typing as deducing facts about the untyped meaning of terms versus trying to
figure out whether some raw syntax is meaningful at all (``Curry versus
Church'' as Barendregt put it in his talk Monday). The two perspectives have
some commonality---in both, Hindley-Milner type reconstruction is taken as
central---but the computational notions of obs-cong and the semantical
domains needed to capture these notions are quite different. Truth is, the
centrality of Hindley-Milner reconstruction is not persuasive in the Curry
approach, since convertible terms are not treated the same by the Hindley
algorithm while the Curry view offers little explanation of which terms, among
a class of mutually convertable terms, are Hindley typable.
Another example of changing contexts is when call-cc is added to, say,
untyped call-by-name lambda calculus; terms that were obs-cong in all
non-call-cc contexts can be distinguished by call-cc contexts.
4. Enough for now.
Regards, A.
---------------------------------------------
Date: Mon, 11 Apr 88 10:56:32 BST
From: allen <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:allen@csta.uucp (Allen Stoughton)>
To: meyer <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:meyer@theory.lcs.mit.edu>
Subject: Full abstraction
Albert,
Thanks for your reply. Let me add one thing before waiting for your
more detailed response. Let's take the Hennessy/Plotkin result again.
Here theorem 5.5 is their adequacy result, which says that the flattening
of the meaning of a term (all terms are observable) is the same as its
input/output behaviour as defined via the operational semantics.
Theorem 5.7 is their full abstraction result: part 1 being what I would
call equational (or ordinary) full abstraction, and part 2 inequational
full abstraction. I have not thought about whether their semantics is
also contextually fully abstract, but it seems likely that it would be.
You may well be right that contextual full abstraction, in the sense of
my thesis, is the right full abstraction notion to look for. I'm just
concerned that you see the fundamental difference between their two theorems.
Theorem 5.5 would also hold for a conventional resumption semantics, i.e.,
a semantics not using their inovation of nondeterministic domain to
achieve a greater degree of abstraction. Such a model would not, of course,
be fully abstract in their (and my) sense.
Allen
----------------------------------
Date: Mon, 9 May 88 14:35:03 BST
From: allen <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:allen@csta.uucp (Allen Stoughton)>
To: meyer <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:meyer@theory.lcs.mit.edu>
Subject: Full abstraction
Albert,
I take it that you haven't produced your promised response to various
peoples comments on full abstraction and your LICS paper yet? If this
is correct, no reply is necessary; otherwise, can I please have a copy?
Cheers,
Allen
------------------------------
Date: Mon, 9 May 88 12:07:53 EST
From: meyer
To: allen%cvaxa.sussex.ac.uk@nss.cs.ucl.ac.uk
allen <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:allen@csta.uucp>
In-reply-to: allen's message of Mon, 9 May 88 14:35:03 BST <8805091335.AA12289@sun.uucp>
Subject: Full abstraction
My reply by interrupted by the complication noted at the end. Here fyi is
the draft I was working on. Regards, A.
--------------------
-----------------
In summary, we mean the same thing by "full abstraction", and "contextual
full abstraction" is (depending upon the language considered) a stronger
requirement.
Allen
----------------
DRAFT REPLY to allen by meyer
My exposition of this subtle but important point about contextual versus full
abstraction is sketchy and needs more work, and I hope it does not end up
more a liability for the confusion it causes than an asset for the
distinction it highlights. Which is to say that I don't think I
misunderstood the situation, but I did explain it poorly.
Let me try to clarify my point with an example along the lines of Apt/Plotkin
but simpler: assigning state-to-state transformations as the meaning of
deterministic while-programs over the integers.
One way this is typically done is by defining an interpreter which does the
step by step assignment and test operations whose cumulative effect on any
given start state yield the final state, i.e., an ``operational'' semantics.
Another standard way is to define a denotational semantics. Now connecting
the two involves a small ``apples and oranges'' comparison, because states in
the operational setup are typically finite data structures---say, lists of
identifier-integer pairs---and program meanings operationally are literally
PARTIAL FUNCTIONS on these finite data structures. On the other hand, in the
denotational setup, states are typically TOTAL functions from the infinite
set of all identifiers to the integers union a special ``unused'' storable
value; meanings of programs are TOTAL MONOTONE FUNCTIONS on the flat cpo of
states.
Of course the correspondence in this case between these operational and
denotational versions of state-transforms is so straightforward that it seems
picky to emphasize the distinction between. But in analogous examples
involving Algol-like languages, the correspondence is considerably more
elaborate: the denotational meaning in Oles', Tennent's, and my and Sieber's
work, is, e.g., a functor on a category whose objects are abstract
``state-shapes'' into the category of cpo's. In cases like these, one needs
theoretical guidance to avoid ad hoc, possibly misguided, notions of what a
``good'' correspondence between operational and denotational
``state-transforms'' might be.
So I want a common ``observation'' which can be extracted with a minimum of
arbitrary choice from whichever kind of program meanings one has. In this
case, I propose observing TERMINATION.
Let me introduce a little bit of terminology here. A CLOSED while-program is
one whose only free identifiers are ``first-order'' variables taking integer
values, eg,
WHILE x > 1 DO y:=y+1; x:=x-1 OD.
An OPEN while-program may have free identifiers of other sensible
phrase-types, eg,
WHILE x > 1 DO B(Y, x:=x-1) OD
where Y is of type ``program'' and B is of type ``program x program -->
program''. Instances of B(Y,Z) might be Y;Z or IF x=2 then X else Y IF.
Finally, I want to talk about COMPLETELY CLOSED programs, or more precisely,
since we have no way to bind location identifiers in simple while-programs,
let's look at completely INITIALIZED closed programs which begin with a
series of assignment statements assigning integer constants to all
identifiers, eg,
x:=3; y:=5; WHILE x > 1 DO y:=y+1; x:=x-1 OD.
Clearly, a completely closed program is state independent and can only diverge
identically in all states, or terminate in all states leaving every starting
state unchanged.
Now I can define the purely operational notion of ``obervational congruence''
between two programming language phrases of the same phrase-type. F and G
are OBSCONG precisely when, for all closed substitutions, sigma, for the free
non-first-order identifiers in F and G, and all completely closing program
contexts C[.],
C[sigma(F)] terminates in some (equivalently all) states iff
C[sigma(G)] does so.
I say a denotational semantics is ADEQUATE for an operational semantics
when for all COMPLETELY CLOSED programs, P,
P terminates in some (equivalently all) states iff
the denotational meaning of P does not equal ``bottom'',
where ``bottom'' is the appropriate semantical value which, in all the case
studies so far, has been obviously identifiable with a minimum of
arbitrariness.
Now by definition of ``denotational'' style, denotational equality is a
congruence wrt to definable operations and substitutions, so we immediately
have that
LEMMA. If two phrases P, Q are denotationally equal in an adequate semantics,
then P, Q are obscong.
But note that the converse in fact holds automatically when P,Q are CLOSED
programs:
LEMMA. If two closed while-programs P and Q are obscong, then in any
adequate denotational semantics, the meanings of P and Q are equal
------------------------------
ALLEN: the problem I realized is that this lemma of course ain't true without
some further hypotheses about `sensible' semantics relating the meanings of
a closed program P and the completely closed programs x1:=c1;...xn:=cn;P
where x1 are the free variable of P and c1,...cn are numerals. These
hypotheses amoount to assuming full abstraction at this level, and I now
think the point I was trying to make relating adequacy and full abstraction
of closed terms of lowest type is not worth emphasizing---since it only seems
to hold in general for flat types. Anyway, it need more thought.
Since it's now end-of-term rush combined with overdue proposal time, research
is on the back burner for another couple of weeks. Nice to hear from you.
Regards, A.