Subject: lazy lambda calculus references - msg#00006

Previous Message by Date:

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.

Next Message by Date:

[wand-DMTVktDHDm5ObnrBt4yx7uYMHaKe9WOTpQNEQKNNdayskDOk/GSq1Q@xxxxxxxxxxxxxxxx]

Date: Mon, 14 Aug 89 15:47:08 EDT From: Mitchell Wand <wand-DMTVktDHDm5ObnrBt4yx7uYMHaKe9WOTlXN7HHkbuXM@xxxxxxxxxxxxxxxx> To: lieber-DMTVktDHDm5ObnrBt4yx7uYMHaKe9WOTlXN7HHkbuXM@xxxxxxxxxxxxxxxx, abbas@xxxxxxxxxxxxxxxxxxxxxxxxxxx, zywang-dryMzwA+bZdoAL7LN7WEl4dd74u8MsAO@xxxxxxxxxxxxxxxx, woolf@xxxxxxxxxxxxxxxx, oliva-DMTVktDHDm5ObnrBt4yx7uYMHaKe9WOTlXN7HHkbuXM@xxxxxxxxxxxxxxxx, holland@xxxxxxxxxxxxxxxxxxxxxxxxxxx, riel-DMTVktDHDm5ObnrBt4yx7uYMHaKe9WOTlXN7HHkbuXM@xxxxxxxxxxxxxxxx, bwhite@xxxxxxx, muller@xxxxxxxxxxxx, kfoury-yxhbIRfuK6b2fBVCVOL8/A@xxxxxxxxxxxxxxxx, raf@xxxxxxxxxxxx, snyder@xxxxxxxxxxxx, trung-yxhbIRfuK6b2fBVCVOL8/A@xxxxxxxxxxxxxxxx, Esler%bucsf.bu.edu@xxxxxxxxxxxx, dsmith-psjVXkmwMxnkRhP8+e8VMA@xxxxxxxxxxxxxxxx, jmiller@xxxxxxxxxxxxxxx, mairson-psjVXkmwMxnkRhP8+e8VMA@xxxxxxxxxxxxxxxx, pmo%icad.uucp@xxxxxxxxxxxx, attend-types-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx, attend-logic@xxxxxxxxxxxxxxxxxx, farmer-jkL4ws/oz7h2KNKLiPMURA@xxxxxxxxxxxxxxxx, lalita@xxxxxxxxxxxxxxxxxx Subject: [riecke-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx: This week's meeting] Return-Path: <riecke-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx> Date: Mon, 14 Aug 89 13:42:47 EDT From: riecke-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx To: logic-seminar-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx Subject: This week's meeting The logic and types seminar will meet WEDNESDAY, August 16, from 12:30-2pm. Albert will discuss work by Phil Wadler and others on using logical relations to prove "parametrically polymorphic" equations in the typed lambda calculus. The seminar will NOT meet Friday; we hope to meet once per week until the end of the summer. -Jon

Previous Message by 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-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.

Next Message by Thread:

[wand-DMTVktDHDm5ObnrBt4yx7uYMHaKe9WOTpQNEQKNNdayskDOk/GSq1Q@xxxxxxxxxxxxxxxx]

Date: Mon, 14 Aug 89 15:47:08 EDT From: Mitchell Wand <wand-DMTVktDHDm5ObnrBt4yx7uYMHaKe9WOTlXN7HHkbuXM@xxxxxxxxxxxxxxxx> To: lieber-DMTVktDHDm5ObnrBt4yx7uYMHaKe9WOTlXN7HHkbuXM@xxxxxxxxxxxxxxxx, abbas@xxxxxxxxxxxxxxxxxxxxxxxxxxx, zywang-dryMzwA+bZdoAL7LN7WEl4dd74u8MsAO@xxxxxxxxxxxxxxxx, woolf@xxxxxxxxxxxxxxxx, oliva-DMTVktDHDm5ObnrBt4yx7uYMHaKe9WOTlXN7HHkbuXM@xxxxxxxxxxxxxxxx, holland@xxxxxxxxxxxxxxxxxxxxxxxxxxx, riel-DMTVktDHDm5ObnrBt4yx7uYMHaKe9WOTlXN7HHkbuXM@xxxxxxxxxxxxxxxx, bwhite@xxxxxxx, muller@xxxxxxxxxxxx, kfoury-yxhbIRfuK6b2fBVCVOL8/A@xxxxxxxxxxxxxxxx, raf@xxxxxxxxxxxx, snyder@xxxxxxxxxxxx, trung-yxhbIRfuK6b2fBVCVOL8/A@xxxxxxxxxxxxxxxx, Esler%bucsf.bu.edu@xxxxxxxxxxxx, dsmith-psjVXkmwMxnkRhP8+e8VMA@xxxxxxxxxxxxxxxx, jmiller@xxxxxxxxxxxxxxx, mairson-psjVXkmwMxnkRhP8+e8VMA@xxxxxxxxxxxxxxxx, pmo%icad.uucp@xxxxxxxxxxxx, attend-types-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx, attend-logic@xxxxxxxxxxxxxxxxxx, farmer-jkL4ws/oz7h2KNKLiPMURA@xxxxxxxxxxxxxxxx, lalita@xxxxxxxxxxxxxxxxxx Subject: [riecke-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx: This week's meeting] Return-Path: <riecke-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx> Date: Mon, 14 Aug 89 13:42:47 EDT From: riecke-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx To: logic-seminar-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx Subject: This week's meeting The logic and types seminar will meet WEDNESDAY, August 16, from 12:30-2pm. Albert will discuss work by Phil Wadler and others on using logical relations to prove "parametrically polymorphic" equations in the typed lambda calculus. The seminar will NOT meet Friday; we hope to meet once per week until the end of the summer. -Jon