Document Open Access Logo

A Note on Logical PERs and Reducibility. Logical Relations Strike Again!

Author Jean Gallier

PDF
Thumbnail PDF

File

OASIcs.Tannen.7.pdf
  • Filesize: 0.56 MB
  • 12 pages

Document Identifiers

Author Details

Jean Gallier
  • University of Pennsylvania, Philadelphia, PA, USA

Cite AsGet BibTex

Jean Gallier. A Note on Logical PERs and Reducibility. Logical Relations Strike Again!. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 7:1-7:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/OASIcs.Tannen.7

Abstract

We prove a general theorem for establishing properties expressed by binary relations on typed (first-order) λ-terms, using a variant of the reducibility method and logical PERs. As an application, we prove simultaneously that β-reduction in the simply-typed λ-calculus is strongly normalizing, and that the Church-Rosser property holds (and similarly for βη-reduction).

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Type theory
  • Theory of computation → Complexity theory and logic
Keywords
  • Typed lambda-calculus
  • reducibility
  • logical relations
  • per’s
  • strong normalization
  • Church-Rosser property

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51:1-77, 1991. Google Scholar
  2. V. Breazu-Tannen and T. Coquand. Extensional models for polymorphism. Theoretical Computer Science, 59:85-114, 1988. Google Scholar
  3. P. Freyd, P. Mulry, G. Rosolini, and D. Scott. Extensional pers. Information and Computation, 98(2):211-227, 1992. Google Scholar
  4. H. Friedman. Equality between functionals. In R. Parikh, editor, Logic Colloquium, volume 453 of Lecture Notes in Math., pages 22-37. Springer-Verlag, 1975. Google Scholar
  5. Jean H. Gallier. On Girard’s "candidats de reductibilité". In P. Odifreddi, editor, Logic And Computer Science, pages 123-203. Academic Press, London, New York, May 1990. Google Scholar
  6. Jean H. Gallier. On the correspondence between proofs and λ-terms. In P. DeGroote, editor, The Curry-Howard Isomorphism, Cahiers du Centre de Logique, No. 8, pages 55-138. Université Catholique de Louvain, 1995. Google Scholar
  7. Jean H. Gallier. Proving properties of typed λ-terms using realizability, covers, and sheaves. Theoretical Computer Science, 142:299-368, 1995. Google Scholar
  8. Jean H. Gallier. Typing untyped lambda terms, or reducibility strikes again! Annals of Pure and Applied Logic, 91:231-270, 1998. Google Scholar
  9. Jean-Yves Girard. Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types. In J.E. Fenstad, editor, Proc. 2nd Scand. Log. Symp., pages 63-92. North-Holland, 1971. Google Scholar
  10. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université de Paris VII, June 1972. Thèse de Doctorat d'Etat. Google Scholar
  11. Gérard Huet. Initiation au λ-calcul. Technical report, Université Paris VII, Paris, 1991. Lectures Notes. Google Scholar
  12. J.M.E. Hyland. The effective topos. In A. S. Troelstra and D. Van Dalen, editors, L. E. J. Brouwer, Centenary Symposium, Studies in Logic. North-Holland, 1982. Google Scholar
  13. G. Koletsos. Church-Rosser theorem for typed functional systems. J. Symbolic Logic, 50(3):782-790, 1985. Google Scholar
  14. J.L. Krivine. Lambda-Calcul, types et modèles. Etudes et recherches en informatique. Masson, 1990. Google Scholar
  15. J. C. Mitchell. A type-inference approach to reduction properties and semantics of polymorphic expressions. In ACM Conference on LISP and Functional Programming, pages 308-319. ACM, 1986. Reprinted in Logical Foundations of Functional Programming, G. Huet, Ed., Addison Wesley, 1990, 195-212. Google Scholar
  16. J.C. Mitchell and E Moggi. Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic, 51:99-124, 1991. Google Scholar
  17. P. S. Mulry. Generalized Banach-Mazur functionals in the topos of recursive sets. J. Pure Appl. Alebra, 26, 1982. Google Scholar
  18. G.D. Plotkin. Lambda definability in the full type hierarchy. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363-373, London, 1980. Academic Press. Google Scholar
  19. R. Statman. Completeness, invariance, and λ-definability. J. Symbolic Logic, 47(1):17-26, 1982. Google Scholar
  20. R. Statman. Equality between functionals, revisited. In Harrington, Morley, Scedrov, and Simpson, editors, Harvey Friedman’s Research on the Foundations of Mathematics, pages 331-338. North-Holland, 1985. Google Scholar
  21. R. Statman. Logical Relations and the Typed λ-Calculus. Information and Control, 65(2/3):85-97, 1985. Google Scholar
  22. W.W. Tait. Intensional interpretation of functionals of finite type I. J. Symbolic Logic, 32:198-212, 1967. Google Scholar
  23. W.W. Tait. A realizability interpretation of the theory of species. In R. Parikh, editor, Logic Colloquium, volume 453 of Lecture Notes in Math., pages 240-251. Springer Verlag, 1975. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact