Skip to main content
SpringerLink
Log in

Syntactic equivalences inducing semantic equivalences

  • Constructive And Combinatory Logic
  • Conference paper
  • First Online:
EUROCAL '85 (EUROCAL 1985)

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

Included in the following conference series:

Abstract

Following the idea behind algebraic theories we define a fairly general notion of equivalence between two many-sorted equational presentations s.t. an equivalence is induced on the corresponding categories of models. This definition allows to bring down to a symbolic level some equivalences known to model theorists. We illustrate this for the known connection between λ-calculus and cartesian closed categories. We present a syntactic equivalence between an "untyped" version of cartesian closed categories (i.e. where objects are dropped), and cartesian closed categories with a universal object, isomorphic to its product and function spaces, thus relating at a purely syntactic level an untyped calculus and a typed calculus. Direct syntactic equivalences between λ-calculus and cartesian closed categories are explored in companion papers: the direction from cartesian closed categories may be used for an elegant solution of the word problem of cartesian closed categories, whereas the direction to cartesian closed categories offer simple and efficient techniques for implementing functional programming languages, well suited for special VLSI design.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. T. Adachi, A Categorical Characterization of Lambda-Calculus Models, Research Report C-49, Department of Information Sciences, Tokyo Institute of Technology (1983).

    Google Scholar 

  2. G. Berry, Some Syntactic and Categorical Constructions of Lambda-calculus models, Rapport INRIA 80 (1981).

    Google Scholar 

  3. G. Berry, Modèles Complètement Adéquats et Stables des Lambda-calculus typés, Thèse de Doctorat d'Etat, Université Paris VII (Mars 1979).

    Google Scholar 

  4. R. Burstall, J. Goguen, Introducing Institutions, SRI International and University of Edinburgh (1983).

    Google Scholar 

  5. G. Cousineau, P-L. Curien, M. Mauny, The Categorical Abstract Machine, Rapport LITP 85-8, Université Paris VII (January 1985).

    Google Scholar 

  6. P.L. Curien, Categorical Combinatory Logic, ICALP 85 (Nafplion).

    Google Scholar 

  7. P-L. Curien, Typed Categorical Combinatory Logic, CAAP 85 (Berlin).

    Google Scholar 

  8. P-L. Curien, Combinateurs Catégoriques, Algorithmes Séquentiels et Programmation Applicative, Thèse d'Etat, Université Paris VII (Dec. 1983), improved version as Rapport LITP (1984), to be published in english as a monograph.

    Google Scholar 

  9. P.L. Curien, Algorithmes Séquentiels sur Structures de Données Concrètes, Thèse de Troisième Cycle, Université Paris VII (Mars 1979).

    Google Scholar 

  10. J.A.Goguen, J.Meseguer, An Initiality Primer, to appear in the Proc. of the French-US Symp. on the Applications of Algebra to Language Definition and Compilation, Fontainebleau, (June 1982), to appear at Cambridge University Press.

    Google Scholar 

  11. G. Huet, D. Oppen, Equations and Rewrite Rules: a Survey, in Formal Language Theory: Perspectives and Open Problems, R.Book Ed., Academic Press, 349–405 (1980).

    Google Scholar 

  12. C. Koymans, Models of the Lambda Calculus, PhD Thesis, Utrecht (May 1984).

    Google Scholar 

  13. J. Lambek, From Lambda-calculus to Cartesian Closed Categories, in To H.B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, ed. J.P. Seldin and J.R. Hindley, Academic Press (1980).

    Google Scholar 

  14. J. Lambek and P. Scott, Introduction to Higher Order Categorical Logic, to be published by Cambridge University Press (1984).

    Google Scholar 

  15. D. Scott, Relating Theories of the Lambda-calculus, cf. [Lam].

    Google Scholar 

  16. Szabo, The Algebra of Proofs, Studies in Logic 83, North Holland (1978).

    Google Scholar 

  17. H. Yokouchi, Cartesian Closed Structures in Models of the Lambda Calculus, Department of Information Sciences, Tokyo Institute of Technology (1983).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Tour 55-56 1er étage, CNRS-Université Paris VII, LITP, 2 Place Jussieu, 75221, Paris Cedex 05

    P-L. Curien

Authors
  1. P-L. Curien
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Bob F. Caviness

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Curien, PL. (1985). Syntactic equivalences inducing semantic equivalences. In: Caviness, B.F. (eds) EUROCAL '85. EUROCAL 1985. Lecture Notes in Computer Science, vol 204. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15984-3_259

Download citation

  • DOI: https://doi.org/10.1007/3-540-15984-3_259

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-39685-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation