[Prev][Next][Index][Thread]
Completeness Theorem for Typed Lambda-Omega Calculus
Yiannis: hard copy follows.
Regards, A.
---------------
August 10, 1989
(Abstract for Logic from Computer Science Workshop,
November, 1989 at Berkeley, MSRI)
Completeness for Flat, Simply Typed Lambda-Calculus
Albert R. Meyer*
MIT Lab. for Computer Science
Internet: meyer@lcs.mit.edu
Familiar beta-eta equational reasoning about pure terms in the simply
typed lambda-calculus is complete for
1. all models [4],
2. the classical model with integer base type [4],
3. the cpo model with flat integer base type [9, 10],
4. "observational congruence" with respect to integer outputs
(cf. [5]) in contexts of Scott's PCF augmented with a
"parallel-OR" combinator [8], and
5. observational congruence with respect to integer outputs in
contexts of Scott's original, ``sequential'' PCF.
Enriching the syntax of pure terms with a single base-type constant Omega,
denoting the "bottom" or "divergent" element, distinguishes these cases.
We may consider whether an equation between such pure lambda-Omega-terms
is valid in
(1.1-Om) all monotone models (with bottom elements),
(1.2-Om) all monotone models with flat base type,
(2-Om) the standard monotone model with flat integer base type and
function spaces taken to be all monotone functions,
(3-Om) the cpo model with flat integer base type,
(4-Om) observational congruence wrt PCF plus parallel-OR, and
(5-Om) observational congruence wrt sequential PCF.
We show that familiar beta-eta equational reasoning is complete for
proving (1.1-Om)-valid equations. However, we observe that (1.1-Om) implies
(1.2-Om) but not conversely, since for example the equation
f (f Omega) = f Omega
is valid when the base type is flat, but not in general.
We prove that (1.2-Om)-(4-Om) equational validities coincide, but no
EQUATIONAL axiomatization is complete for proving all the equations
implied by a set of equations. We then present an axiomatization--which
includes nonequational, disjunctive inference rules--of a quantifier-free
sequent calculus whose atomic formulas are inequalities, M < N , between
typed lambda-Omega-terms. We show our sequent calculus is complete for
(1.2-Om)-validity of sequents, and a fortiori complete for flat-valid
lambda-Omega-equations.
For general sequents with nonempty antecedents, (1.2-Om)-validity is
undecidable, and by completeness, so also is provability in our sequent
calculus. We observe, however, that the flat-valid EQUATIONS are
decidable.
We remark that for general sequents, (1.2-Om)-(4-Om) validities no longer
coincide. In particular, (1.2-Om)-validity implies (2-Om)-validity, but
not conversely. (3-Om)-validity of sequents is Pi^0_2-complete, and hence
not axiomatizable.
This is joint work with Stavros Cosmadakis, IBM Watson Research Center,
and Jon Riecke, MIT Lab. for Computer Science. It is motivated by,
and leads to a completeness theorem for, the logic of pure, typed "lazy"
lambda-calculus, when not just integers, but termination--even of
higher-order terms--is taken to be an observable result of a computation
[5, 7, 6, 1, 2, 3].
References
[1] B. Bloom and J. G. Riecke. LCF should be lifted. In T. Rus, editor,
Proc. Conf. AMAST, pages 133-136, Dept. Computer Sci., U. Iowa,
1989.
[2] S. S. Cosmadakis. Computing with recursive types. In 4th Symp. Logic
in Computer Science, pages 24-38, IEEE, 1989.
[3] S. S. Cosmadakis, A. R. Meyer, and J. G. Riecke. Completeness for
equations between lazy terms. In 16th Symp. Principles of Programming
Languages, ACM, 1990. Submitted, July, 1989.
[4] H. Friedman. Equality between functionals. In R. Parikh, editor, Logic
Coll. '73, pages 22-37, Volume 453 of Lect. Notes in Math., Springer-
Verlag, 1975.
[5] A. R. Meyer. Semantical paradigms: notes for an invited lecture, with
two appendices by Stavros S. Cosmadakis. In 3rd Symp. Logic in Com-
puter Science, pages 236-255, IEEE, 1988.
[6] C. L. Ong. Fully abstract models of the lazy lambda calculus. In 29th
Symp. Foundations of Computer Science, pages 368-376, IEEE, 1988.
[7] C. L. Ong. The Lazy Lambda Calculus: An Investigation into the Foun-
dations of Functional Programming. Ph.D. thesis, Imperial College, U.
London, 1988.
[8] G. D. Plotkin. LCF considered as a programming language. Theoretical
Computer Sci., 5:223-257, 1977.
[9] G. D. Plotkin. Notes on completeness of the full continuous type hier-
archy. Nov. 1982. Unpublished manuscript, MIT.
[10] R. Statman. Equality between functionals revisited. In L. Harrington,
et al., editor, Harvey Friedman's Research on the Foundations of Math-
ematics, pages 331-338, Volume 117 of Studies in Logic, North-Holland,
1985.
________________________________
* Supported by NSF Grant Nos. 8511190-DCR and 8819761-CCR, and ONR grant No.
N00014-83-K-0125.