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-7nwHvcHdrJGVc3sceRu5cw@xxxxxxxxxxxxxxxx

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.