[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.