Reducibility Proofs in the λ-Calculus

• Autorzy: Kamareddine F. , Rahli V. , Wells J. B.
• Języki publikacji: EN

Abstrakty

EN

Reducibility, despite being quite mysterious and inflexible, has been used to prove a number of properties of the λ-calculus and is well known to offer general proofs which can be applied to a number of instantiations. In this paper, we look at two related but different results in λ-calculi with intersection types. 1. We show that one such result (which aims at giving reducibility proofs of Church-Rosser, standardisation and weak normalisation for the untyped λ-calculus) faces serious problems which break the reducibility method. We provide a proposal to partially repair the method. 2. We consider a second result whose purpose is to use reducibility for typed terms in order to show the Church-Rosser of &lbeta;-developments for the untyped terms (and hence the Church- Rosser of β-reduction). In this second result, strong normalisation is not needed. We extend the second result to encompass both βI- and βη-reduction rather than simply β-reduction.

Słowa kluczowe

EN

lambda calculus; reducibility; Church-Rosser theorem; development

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 121, nr 1/4
• Strony: 121--152
• Opis fizyczny: Bibliogr. 20 poz.

Twórcy

autor

Kamareddine F.

autor

Rahli V.

autor

Wells J. B.

• ULTRA Group (Useful Logics, Types, Rewriting, and their Automation), Heriot-Watt University, School of Mathematical and Computer Sciences, Mountbatten building, Edinburgh EH14 4AS, UK,

Bibliografia

• [1] H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North-Holland, revised edition, 1984.
• [2] H. Barendregt, J. A. Bergstra, J. W. Klop, and H. Volken. Degrees, reductions and representability in the lambda calculus. Technical Report Preprint no. 22, University of Utrecht, Department of Mathematics, 1976.
• [3] M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic., 21(4):685-693, 1980.
• [4] M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and λ-calculus semantic. In J. P. Seldin J. R. Hindley, editor, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.
• [5] M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Mathematische Logik Und Grundlagen der Mathematik, 27:45-58, 1981.
• [6] H. B. Curry and R. Feys. Combinatory Logic, vol. 1. Elsevier, 1958.
• [7] J. Gallier. On Girard's "candidats de reductibilité". In P. Odifreddi, editor, Logic and Computer Science, pages 123-203. Academic Press, 1990.
• [8] J. Gallier. On the correspondance between proofs and λ-terms. Cahiers du centre de logique, 1997. Available at http://www.cis.upenn.edu/~jean/gbooks/logic.html (last visited 2008-02-6).
• [9] J. Gallier. Typing untyped λ-terms, or reducibility strikes again!. Annals of Pure and Applied Logic, 91(2-3):231-270, 1998.
• [10] J.-Y. Girard. Interprétation Fonctionnelle et Elimination des Coupures de l'Arithmétique d'Ordre Supérieur. PhD thesis, Université Paris 7, 1972.
• [11] S. Ghilezan and S. Likavec. Reducibility: A ubiquitous method in lambda calculus with intersection types. Electronic Notes in Theoretical Compututer Science, 70(1), 2002.
• [12] S. C. Kleene. On the interpretation of intuitionistic number theory. The Journal of Symbolic Logic, 10(4):109-124, 1945.
• [13] J.W. Klop. Combinatory Reductions Systems. PhD thesis, Mathematisch Centrum, Amsterdam, 1980.
• [14] G. Koletsos. Church-Rosser theorem for typed functional systems. Journal of Symbolic Logic, 50(3):782-790, 1985.
• [15] J. L. Krivine. Lambda-calcul, types et modèles. Masson, 1990.
• [16] G. Koletsos and G. Stavrinos. Church-Rosser property and intersection types. Australian Journal of Logic, 6:37-54, 2008.
• [17] John C. Mitchell. Type systems for programming languages. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 365-458. MIT press, 1990.
• [18] John C. Mitchell. Foundations for programming languages. Foundation of computing series. MIT Press, 1996.
• [19] Richard Statman. Logical relations and the typed lambda-calculus. Information and Control, 65(2/3):85-97, 1985.
• [20] W. W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):198-212, 1967.