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

[meyer: full abstraction]

Date: Mon, 16 May 88 10:56:03 EST
From: meyer
To: matthias@rice.edu
In-reply-to: Matthias Felleisen's message of Sun, 15 May 88 13:35:46 CDT <8805151835.AA01831@leto.rice.edu>
Subject: full abstraction
cc: plotkin@csli.stanford.edu, riecke

   Date: Sun, 15 May 88 13:35:46 CDT
   From: Matthias Felleisen <matthias@rice.edu>

   With regard to Gordon Plotkin's comments: Could it be that full
   abstraction is a red herring? That may sound like heresy but let me
   argue for it. As computer scientists, we are really interested in
   operational equivalence. The computer is operational and mathematics
   per se is irrelevant for us. Now, operational equivalence is a pretty
   strong theory and there is no hope that we can reason about all of its
   equalities. So what we are trying to do is to find ``reasonable''
   approximations.  Programming language calculi constitute one way. This
   yields a nice algebra, but no handle at ``computational'' induction.
   So, we also want mathematical models for the more serious problems.
   That's why we look into denotational semantics. But again, the goal is
   to find something like a theory such that M = N in this model implies
   M =~ N (opeq). In some cases we can go back, in others we can't. But,
   why should we care?  -- Matthias

-------------------
Full abstraction, like say, completeness of logical theories, is not a sine
qua non, but its failure means something is wrong relative to a (possibly
unachievable) ideal.  One may, on further examination, well decide that what
is wrong is irrelevant, but it seems prudent to check the situation out
before deciding these deviations from the ideal are not something to care
about.  Concretely in the case of your calculus, there are too many fairly
``natural'', even ``obvious'', equations it misses, so the failure of full
abstraction is too severe to ignore.

My views on the appropriateness of fully abstract models are not settled, by
the way, in light of my recent experience with Sieber trying to find models
for ALGOL-like languages.  A major point of it all is to have a proof
methodology for proving operational congruences all right, but it may not be
a good idea to insist that the methodology be formulated in terms of proving
semantical EQUALITIES in some (full abstract) model.  Specifically in the
case of ALGOL, it might be better to go with the standard marked-store model
for allocating local variables, and use an appropriate ``dynamic logic'' for
proving that programs which are semantically unequal---because their behavior
differs on improperly marked (irrelevant) stores---are equal on ``properly
marked'' stores.  I'm not sure about this, but we're planning to explore this
route.

Can I forward this to TYPES and LOGIC?

Regards, A. 

-----------
Date: Mon, 16 May 88 10:04:52 CDT
From: Matthias Felleisen <matthias@rice.edu>
To: meyer@theory.lcs.mit.edu
Cc: plotkin@csli.stanford.edu, riecke@theory.lcs.mit.edu
In-Reply-To: Albert R. Meyer's message of Mon, 16 May 88 10:56:07 ast <8805161456.AA15013@STORK.LCS.MIT.EDU>
Subject: full abstraction


I fully agree with your answer!

Yes, you can forward this to TYPES and LOGIC. 

-- Matthias