Intersection Types and Termination Properties

• Autorzy: Koletsos G.
• Języki publikacji: EN

Abstrakty

EN

We use the system of intersection types and the type assignment method to prove termination properties in λ-calculus. In the first part we deal with conservation properties. We give a type assignment proof of the classical conservation theorem for λI calculus and then we extend this method to the notion of the reduction β_I and β_S of de Groote [9]. We also give a direct type assignment proof of the extended conservation property according to which if a term is βI , βS- normalizable then it is β-strongly normalizable. We further extend the conservation theorem by introducing the notion of β-normal form. In the second part we prove that if Ω is not a substring of a λ-term M then M can be typed in the Krivine's system D of intersection types. In that way we obtain a type assignment proof of the Sorensen’s Ω-theorem.

Słowa kluczowe

EN

intersection types; termination properties

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

Twórcy

autor

Koletsos G.

• National Technical University of Athens Department of Computer Science Zografou Campus - 157 80 Athens - Greece,

Bibliografia

• [1] S. van Bakel. Complete restrictions of the intersection type discipline. Theoretical Computer Science, 102 (1): pp. 135 - 163, 1992.
• [2] H.P. Barendregt. The lambda calculus, its syntax and semantics. North-Holland, 1984.
• [3] H.P. Barendregt. Lambda calculi with types. Handbook of Logic in Computer science, Vol 2, Oxford 1992.
• [4] A. Church. The Calculi of Lambda Conversion, Princeton University Press, Princeton 1941.
• [5] M. Coppo, M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Logic, 21(4), 1980.
• [6] M. Dezani-Ciancaglini and S. Ghilezan. A lambda calculus model characterizing computational behavior of terms, in: Proc. International Workshop on Rewriting in Proof and Computation RPC '01, pp. 100 - 119,2001.
• [7] M. Dezani-Ciancaglini, S. Ghilezan and S. Likavec. Behavioural inverse limit models, Theor. Comput. Sci. 316(1 - 3) pp. 49 - 74, 2004.
• [8] S. Ghilezan and S. Likavec. Recucibility: A Ubiquitous Method in Lambda Calculus with Intersection Types. Electr. Notes Theor. Comput. Sci. 70 (1): 2002.
• [9] P. de Groote. The Conservation theorem revisited. Proceedings of the International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, Vol. 664, Springer-Verlag, 1993 pp. 163-178.
• [10] A.J. Kfoury, J.B. Wells. New Notions of Reduction and Non-Semantic Proofs of Strong Beta-Normalization in Typed Lambda Calculi, 10th Annual IEEE Symposium on Logic in Computer Scirence, LICS'95, 1995.
• [11] G. Koletsos and G. Stavrinos. The structure of reducibility proofs. G. Koletsos, Ph. Kolaitis (eds.), Proceedings of the Second Panhellenic Logic Symposium, Delphi 1999, pp. 138 - 143.
• [12] G. Koletsos and G. Stavrinos. Church-Rosser theorem for conjunctive type systems, in: A.K. Kakas, A. Sinachopoulos (eds.), Proceedings of the First Panhellenic Symposium on Logic, University of Cyprus (1997), pp. 25 - 37.
• [13] G. Koletsos and G. Stavrinos. Church-Rosser property and intersection types, Australasian Journal of Logic, Vol. 6, 2008.
• [14] J.L. Krivine. Lambda-calcul, types et modèles. Masson, 1990.
• [15] Sundeep Oberoi. lambda beta' - A - lambda-Calculus with a Generalized beta-Reduction Rule, Inf. Process. Lett. 54(1), pp. 45 - 53, 1995.
• [16] G. Pottinger. A type assignment for the strongly normalizable λ-terms, in: Seldin, J.P. and Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press 1980, pp. 561 - 577.
• [17] F. van Raamsdonk, P. Severi, M.H. Sørensen and H. Xi. Perpetual Reductions in λ-Calculus. Information and Computation 149, pp. 173 - 225 1999.
• [18] M. H. Sørensen. Properties of infinite reduction paths in untyped λ-calculus, in Proceedings, Tbilisi Symposium on Language, Logic and Computation (J. Ginzburg, Z. Khasidashvili, J. J. Lévy, E. Vogel and E. Vallduvi, (eds.), CLSI Lectures Notes 1996.