Skip to main content
SpringerLink
Log in
Book cover

International Conference on Rewriting Techniques and Applications

RTA 1993: Rewriting Techniques and Applications pp 137–151Cite as

Some lambda calculi with categorical sums and products

  • Conference paper

  • 211 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 690))

Abstract

We consider the simply typed λ-calculus with primitive recursion operators and types corresponding to categorical products and coproducts.. The standard equations corresponding to extensionality and to surjectivity of pairing and its dual are oriented as expansion rules. Strong normalization and ground (base-type) confluence is proved for the full calculus; full confluence is proved for the calculus omitting the rule for strong sums. In the latter case, fixed-point constructors may be added while retaining confluence.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Y. Akama. On Mint's Reduction for ccc-Calculus. Proc. Typed Lambda Calculus and Applications 1993.

    Google Scholar 

  2. H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1981. Revised edition, 1984.

    Google Scholar 

  3. P-L Curien, R. Di Cosmo. A confluent reduction system for the λ-calculus with surjective pairing and terminal object, in Leach et. al. (eds.), Int'l. Conf. on Automata, Languages, and Programming, LNCS 510, 291–302, Springer Verlag 1991.

    Google Scholar 

  4. D. Cubric. Embedding of a free cartesian closed category into the category of Sets. Manuscript, McGill University 1992.

    Google Scholar 

  5. R. Di Cosmo, D. Kesner. Simulating expansions without expansions. Tech Rep, INRIA 1993.

    Google Scholar 

  6. R. Di Cosmo, D. Kesner. A confluent reduction system for the extensional λ-calculus with pairs, sums, recursion and terminal object. Proc ICALP 1993.

    Google Scholar 

  7. N. Dershowitz, J.-P. Jounnaud. Term Rewriting Systems, in Handbook of Theoretical Computer Science, 243–320, North-Holland, Amsterdam, 1991.

    Google Scholar 

  8. D. J. Dougherty. Some reduction properties of a λ-calculus with categorical sums and products. Manuscript, Wesleyan University 1990.

    Google Scholar 

  9. R. O. Gandy. Proofs of strong normalization, in J. P. Seldin and J. R. Hindley (eds.) To H. B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, 1980.

    Google Scholar 

  10. C. Barry Jay. Long β-normal forms and confluence. Manuscript, University of Edinburgh, 1991.

    Google Scholar 

  11. J. W. Klop. Combinatory Reduction Systems. Mathematical Centre Tracts, v. 127. Centre for Mathematics and Computer Science, Amsterdam 1980.

    Google Scholar 

  12. J. W. Klop, R.C. DeVrijer. Unique normal forms for lambda calculus with surjective pairing. Information and Computation, v.80 no. 2, 97–113, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  13. J. Lambek, P. Scott. Introduction to Higher-order Categorical Logic. Cambridge Studies in Advanced Mathematics 7. Cambridge University Press 1986.

    Google Scholar 

  14. F. W. Lawvere. Diagonal arguments and cartesian closed categories, in Category Theory, Homology Theory, and Their Applications II, LNM 92, Springer-Verlag, 1969.

    Google Scholar 

  15. G. E. Mints. Category Theory and Proof Theory. In Aktualnie Voprosi Logiki i Metodologiinauki (Russian) 252–278. Kiev, 1980.

    Google Scholar 

  16. M. Okada, P. Scott. Rewriting theory for uniqueness conditions: coproducts. Talk presented First Montreal Workshop on Programming Language Theory, April 1991.

    Google Scholar 

  17. D. Prawitz. Ideas and Results in Proof Theory, in J. E. Fenstad, ed., Proceedings of the Second Scandinavian Logic Symposium. North-Holland, Amsterdam, 1971.

    Google Scholar 

  18. A. Poigné, J. Voss. On the implementation of Abstract Data Types by Programming Language Constructs. Journal of Computer and System Science 34 (1987), 340–376.

    Article  MATH  Google Scholar 

  19. W. W. Tait. Intensional interpretation of functionals of finite type I, J. Symbolic Logic 32, pp. 198–212, 1967.

    Article  MATH  MathSciNet  Google Scholar 

  20. R. C. de Vrijer, Strong Normalization in N — HA ω. Proc. Koninklijke Nederlandse Akademie van Wetenschappen Series A, 90/4, pp. 473–478, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Mathematics, Wesleyan University, 06459, Middletown, CT, USA

    Daniel J. Dougherty

Authors
  1. Daniel J. Dougherty
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. INRIA Lorraine and CRIN, 615 Rue du Jardin Botanique, F-54602, Villers les Nancy Cedex, France

    Claude Kirchner

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dougherty, D.J. (1993). Some lambda calculi with categorical sums and products. In: Kirchner, C. (eds) Rewriting Techniques and Applications. RTA 1993. Lecture Notes in Computer Science, vol 690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-21551-7_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-21551-7_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56868-1

  • Online ISBN: 978-3-662-21551-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation