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

Retraction of Claim: Completeness for Lazy Lambda Calculus

Date: Sat, 16 Nov 91 16:38:06 EST

	Retraction of Claim: Completeness for Lazy Lambda Calculus

In [2], we claimed the following result:

  CLAIM: For the sequent proof system contained in [2], an
  approximation between simply-typed lambda terms involving a
  divergent constant Omega is provable iff the approximation holds
  in the continuous lazy model.

Together with the following theorem from [1],

  THEOREM: The continuous lazy model is inequationally fully
  abstract for a LAZY version of PCF (where the language includes
  parallel facilities).

the Claim implied that the proof system was COMPLETE for proving
lazy observational approximations of terms with no constants
except Omega.  A similar result was announced in [3] for a sequent
proof system for proving approximations in a CALL-BY-VALUE version
of PCF.  Unfortunately, a gap in both proofs was discovered by
Eugenio Moggi.  Our attempts to repair the gap have so far been
unsuccessful; neither do we have any counterexamples to the
claims.

The following results (also announced in [2]) do hold for the
systems presented in the paper:

  THEOREM:  Fix a lazy sequent theory T.  Then T |= S  iff the
  sequent S is provable from T in lazy sequent logic.

  THEOREM: The set of approximations between simply-typed terms
  involving the constant Omega which hold in the continuous lazy
  model is co-r.e.

Similar theorems announced in [3] for the call-by-value case also
hold.  Full proofs are contained in [4], soon to be available as a
technical report from MIT.

-Stavros Cosmadakis
 Albert Meyer
 Jon Riecke
 



REFERENCES 

[1] Bard Bloom and Jon G. Riecke, "LCF Should Be Lifted", in
Teodor Rus, ed., _Proc. Conf. Algebraic Methodology and Software
Technology_, Department of Computer Science, University of Iowa,
1989, pages 133-136.

[2] Stavros S. Cosmadakis, Albert R. Meyer and Jon G. Riecke,
"Completeness for typed lazy inequalities (preliminary report)",
in _Fifth Symposium on Logic in Computer Science_, IEEE, 1990,
pages 312-320.

[3] Jon G. Riecke, "A Complete and Decidable Proof System for
Call-by-Value Equalities (Preliminary Report)", in M. S. Paterson,
ed., _Automata, Languages and Programming: $\it 17^{th}$
International Colloquium_, Lecture Notes in Computer Science,
Volume 443, Springer-Verlag, pages 20-31.

[4] Jon G. Riecke, _The Logic and Expressibility of Simply-typed
Call-by-Value and Lazy Languages_, Ph.D. thesis, Massachusetts
Institute of Technology, 1991.