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

imprecise definitions, dubious results, and embarrassment


Some researchers (C.K.Gomard, F.Henglein, C.Mossin,...) have published
informal definitions of two-level denotational semantics and proved
theorems about them (see [Gom91,Gom92,HM94]).  Moreover, this seems to
have been considered acceptable or overlooked by others (such as
N.D.Jones, C.Talcott, anonymous referees, and other readers).

I started to read papers on the subject only one year ago, so my
impressions are based on a fairly limited sample of the literature
[HM94,Gom92,GJ91] and few e-mail exchanges.  What follows illustrates
the specific case in brief.

According to the bibliographic references it seems that the source of
the problem can be identified in [Gom92], and more specifically in the
imprecise definition of the semantics for a two-level language given
in [Gom92]: the interpretation of dynamic lambda was defined only
"informally" ([Gom91,GJ91] have exactly the same problem).

After some clarifying e-mail exchanges with F.Henglein, O.Danvy,
N.D.Jones I was able to reconstruct the intended semantics that Gomard
had in mind.  Any expert in the area could probably read between the
lines what was meant, but I think that it should have been spelled out
at least in [Gom92] (which gives the most "detailed" published proof
of correctness) and in Gomard's PhD thesis [Gom91].

However, the intended semantics uses more complex domains than the
informal one, and so the proof of the main result in [Gom92] (a
correctness theorem) need to be adjusted, too.  At this point my
e-mail correspondents were no longer able to say what the "intended
proof" should be!

The ultimate cause of this embarrassing situation was not a mistake in
some complex proof (this is certainly excusable), but the attempt to
prove a theorem about an interpretation defined only informally (I
find this rather deplorable).

Some of these complaints are in my MFPS'97 paper, but I advice to look
at "http://www.disi.unige.it/person/MoggiE/GOMARD/" for a more
up-to-date account, including a technical note proposing an
alternative semantics and a correctness proof (A preliminary version
of this note was rejected by ICALP'97).

Thanks for the your attention
Eugenio Moggi

PS: of course, I would be interested to know if there is a way to fix
the correctness proof in [Gom92] for the intended semantics.

--

COMMENTED BIBLIOGRAPHIC REFERENCES

[Gom92] C.K.Gomard, A Self-applicable Partial Evaluator for the
   Lambda Calculus: Correctness and Pragmatics, ACM TOPLAS, 14(2),
   pp.147-172, April 1992.

   page 156.  The author comments on the clause for interpreting
   dynamic lambda (which uses a "newname" name generator informally),
   and warns that a formal semantics would requires the use of a name
>  counter.  This means that the domain Code should be N->Exp,
>  instead of Exp (like in the informal semantics).

   page 160, Definition 1, case 2.b.  It is unclear how to change the
>  definition of the "logical relation" R at type code in order to
>  prove correctness of the formal semantics.

   page 171, ACKNOWLEDGMENTS.  "...Thanks to P.Wadler and J.Hughes for
   suggesting a simplification of the main induction hypothesis.  Last
   but not least, thanks to the referees whose thorough reports
   pointed out several deficiencies and typos in the original
>  manuscript.  Special thanks go to the reviewer who found an
>  embarrassing blunder in the correctness proof."

[Gom91] C.K.Gomard. Program Analysis Matters. November, 1991. PhD Thesis.
   Supervisor: N.D.Jones,
   External examiner: C.Talcott.
   It includes [Gom92] as a chapter.

[GJ91] C.K.Gomard and N.D.Jones.  A partial evaluator for the untyped
   lambda calculus.  J. of Func. Program., 1(1), 1991.

   This is a very broad paper, which quotes definitions and results in
   [Gom92], and refers to it for detailed proofs.

[HM94] F.Henglein, C.Mossin.  Polymorphic Binding-Time Analysis.  In
   Proceedings of European Symposium on Programming (D.Sannella, ed.),
   pp. 287-301. LNCS 788, 1994.

   The authors adopt an interpretation that differs from that in
   [Gom92] (since it does not use "newname"), and which is obviously
   wrong (again the sore point is dynamic lambda).  When contacted
   F.Henglein admits that the definition is an "unforgivable mistake
   on several counts", and proposes two way to fix it, one of them is
   to use newname as in [Gom92].

--