Characterising Strongly Normalising Intuitionistic Terms

• Autorzy: Santo J. E. , Ivetić J. , Likavec S.
• Języki publikacji: EN

Abstrakty

EN

This paper gives a characterisation, via intersection types, of the strongly normalising proof-terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary λ-calculus. The completeness of the typing system is obtained from subject expansion at root position. Next we use our result to analyze the characterisation of strong normalisability for three classes of intuitionistic terms: ordinary λ-terms, ΛJ-terms (λ-terms with generalised application), and λx-terms (λ-terms with explicit substitution). We explain via our system why the type systems in the natural deduction format for ΛJ and λx known from the literature contain extra, exceptional rules for typing generalised application or substitution; and we show a new characterisation of the β-strongly normalising l-terms, as a corollary to a PSN-result, relating the λ-calculus and the intuitionistic sequent calculus. Finally, we obtain variants of our characterisation by restricting the set of assignable types to sub-classes of intersection types, notably strict types. In addition, the known characterisation of the b-strongly normalising l-terms in terms of assignment of strict types follows as an easy corollary of our results.

Słowa kluczowe

EN

sequent calculus; strong normalisation; intersection types; intuitionistic logic

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

Twórcy

autor

Santo J. E.

autor

Ivetić J.

autor

Likavec S.

• Centre of Mathematics, University of Minho, Portugal,

Bibliografia

• [1] H. P. Barendregt,M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931-940 (1984), 1983.
• [2] M. Coppo and M. Dezani-Ciancaglini. A new type-assignment for lambda terms. Archiv für Mathematische Logik, 19:139-156, 1978.
• [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 semantics. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 535-560. Academic Press, London, 1980.
• [5] P.-L. Curien and H. Herbelin. The duality of computation. In Proc. 5th ACM SIGPLAN International Conference on Functional Programming, ICFP 2000, pages 233-243,Montreal, Canada, 2000. ACM Press.
• [6] D. Dougherty, S. Ghilezan, and P. Lescanne. Intersection and union types in the μeμ-calculus. In M. Coppo and F. Damiani, editors, Intersection types and related systems ITRS 2004, volume 136 of ENTCS, pages 153-172. Elsevier, 2005.
• [7] D. Dougherty, S. Ghilezan, and P. Lescanne. Characterizing strong normalization in the curien-herbelin symmetric lambda calculus: Extending the Coppo-Dezani heritage. Theoretical Computer Science, 398(1-3):114-128, 2008. Festschrift Coppo, Dezani, Ronchi.
• [8] J. Espírito Santo. Completing Herbelin's programme. In S. Ronchi Della Rocca, editor, Proc. 8th International Conference on Typed Lambda Calculi and Applications TLCA 2007, volume 4583 of LNCS, pages 118-132. Springer-Verlag, 2007.
• [9] J. Espírito Santo. Delayed substitutions. In F. Baader, editor, Proc. 18th International Conference on Rewriting Techniques and Applications RTA 2007, volume 4533 of LNCS, pages 169-183. Springer-Verlag, 2007.
• [10] J. Espírito Santo. A note on preservation of strong normalization in the lambda-calculus", Theoretical Computer Science, 412(11): 1027-1032, 2011.
• [11] J. Espírito Santo, S. Ghilezan, and J. Iveti´c. Characterising strongly normalising intuitionistic sequent terms. In International Workshop TYPES 2007 (Selected Papers), volume 4941 of LNCS, pages 85-99. Springer-Verlag, 2008.
• [12] J. Espírito Santo, J. Ivetić, and S. Likavec. Intersection type assignment systems for intuitionistic sequent calculus. In 4th Workshop on Intersection Types and Related Systems ITRS 2008, 2008.
• [13] J. Espírito Santo and L. Pinto. Permutative conversions in intuitionistic multiary sequent calculi with cuts. In Proc. 6th International Conference on Typed Lambda Calculi and Applications TLCA 2003, volume 2071 of LNCS, pages 286-300, 2003.
• [14] H. Herbelin. A lambda calculus structure isomorphic to Gentzen-style sequent calculus structure. In Proc. 8th International Workshop on Computer Science Logic CSL 1994, volume 933 of LNCS, pages 61-75. Springer-Verlag, 1995.
• [15] J. Ivetić. Formal calculi for intuitionistic logic. Master's thesis, University of Novi Sad, 2008.
• [16] F. Joachimski and R.Matthes. Standardization and confluence for J. In Proc. 11th International Conference on Rewriting Techniques and Applications RTA 2000, volume 1833 of LNCS, pages 141-155. Springer- Verlag, 2000.
• [17] K. Kikuchi. Simple proofs of characterizing strong normalisation for explicit substitution calculi. In F. Baader, editor, Proc. 18th International Conference on Rewriting Techniques and Applications RTA 2007, volume 4533 of LNCS, pages 257-272. Springer-Verlag, 2007.
• [18] J.-L. Krivine. Lambda-calcul types et modèles. Masson, Paris, 1990.
• [19] S. Lengrand, P. Lescanne, D. Dougherty, M. Dezani-Ciancaglini, and S. van Bakel. Intersection types for explicit substitutions. Information and Computation, 189(1):17-42, 2004.
• [20] R. Matthes. Characterizing strongly normalizing terms of a -calculus with generalized applications via intersection types. In ICALP Satellite Workshops, pages 339-354, 2000.
• [21] P. M. Neergaard. Theoretical pearls: A bargain for intersection types: a simple strong normalization proof. Journal of Functional Programming, 15(5):669-677, 2005.
• [22] G. Pottinger. A type assignment for the strongly normalizable -terms. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 561-577. Academic Press, London, 1980.
• [23] S. Ronchi Della Rocca. Principal type scheme and unification for intersection type discipline. Theoretical Computer Science, 59:181-209, 1988.
• [24] K. Rose. Explicit substitutions: Tutorial & survey. Technical Report LS-96-3, BRICS, 1996.
• [25] P. Sallé. Une extension de la théorie des types en lambda-calcul. In G. Ausiello and C. Böhm, editors, Proc. 5th International Conference on Automata, Languages and Programming ICALP '78, volume 62 of LNCS, pages 398-410. Springer-Verlag, 1978.
• [26] H. Schwichtenberg. Termination of permutative conversions in intuitionistic Gentzen calculi. Theoretical Computer Science, 212(1-2):247-260, 1999.
• [27] S. van Bakel. Complete restrictions of the intersection type discipline. Theoretical Computer Science, 102(1):135-163, 1992.
• [28] S. van Bakel. Cut-elimination in the strict intersection type assignment system is strongly normalising. Notre Dame Journal of Formal Logic, 45(1), 2004.