×

Intersection types for the resource control lambda calculi. (English) Zbl 1351.03008

Cerone, Antonio (ed.) et al., Theoretical aspects of computing – ICTAC 2011. 8th international colloquium, Johannesburg, South Africa, August 31 – September 2, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-23282-4/pbk). Lecture Notes in Computer Science 6916, 116-134 (2011).
Summary: We propose intersection type assignment systems for two resource control term calculi: the lambda calculus and the sequent lambda calculus with explicit operators for weakening and contraction. These resource control calculi, \(\lambda _{\circledR }\) and \(\lambda_\circledR^{\mathrm{Gtz}}\), respectively, capture the computational content of intuitionistic natural deduction and intuitionistic sequent logic with explicit structural rules. Our main contribution is the characterisation of strong normalisation of reductions in both calculi. We first prove that typability implies strong normalisation in \(\lambda _{\circledR }\) by adapting the reducibility method. Then we prove that typability implies strong normalisation in \(\lambda_\circledR^{\mathrm{Gtz}}\) by using a combination of well-orders and a suitable embedding of \(\lambda_\circledR^{\mathrm{Gtz}}\)-terms into \(\lambda _{\circledR }\)-terms which preserves types and enables the simulation of all its reductions by the operational semantics of the \(\lambda _{\circledR }\)-calculus. Finally, we prove that strong normalisation implies typability in both systems using head subject expansion.
For the entire collection see [Zbl 1229.68001].

MSC:

03B40 Combinatory logic and lambda calculus

Software:

Automath; CRSX
PDF BibTeX XML Cite
Full Text: DOI Link

References:

[1] Abramsky, S.: Computational interpretations of linear logic. Theor. Comput. Sci. 111(1&2), 3–57 (1993) · Zbl 0791.03003
[2] Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, UK (1998) · Zbl 0948.68098
[3] Barbanera, F., Berardi, S.: A symmetric lambda calculus for classical program extraction. Inform. Comput. 125(2), 103–117 (1996) · Zbl 0853.68159
[4] Barendregt, H.P.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984), revised edition · Zbl 0551.03007
[5] Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, pp. 117–309. Oxford University Press, UK (1992)
[6] Barendregt, H.P., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symb. Logic 48(4), 931–940 (1984) (1983) · Zbl 0545.03004
[7] Benton, N., Bierman, G., de Paiva, V., Hyland, M.: A term calculus for intuitionistic linear logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 75–90. Springer, Heidelberg (1993) · Zbl 0795.68127
[8] Bloo, R., Rose, K.H.: Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In: Computer Science in the Netherlands, CSN 1995, pp. 62–72 (1995)
[9] Coppo, M., Dezani-Ciancaglini, M.: A new type-assignment for lambda terms. Archiv für Mathematische Logik 19, 139–156 (1978) · Zbl 0418.03010
[10] Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the {\(\lambda\)}-calculus. Notre Dame J. Formal Logic 21(4), 685–693 (1980) · Zbl 0423.03010
[11] Curien, P.-L., Herbelin, H.: The duality of computation. In: 5th International Conference on Functional Programming, ICFP 2000, pp. 233–243. ACM Press, New York (2000) · Zbl 1321.68146
[12] Dezani-Ciancaglini, M., Ghilezan, S., Likavec, S.: Behavioural Inverse Limit Models. Theor. Comput Sci. 316(1-3), 49–74 (2004) · Zbl 1055.03014
[13] Dougherty, D.J., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage. Theor. Comput Sci. 398, 114–128 (2008) · Zbl 1146.68028
[14] Espírito Santo, J.: Completing herbelin’s programme. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 118–132. Springer, Heidelberg (2007) · Zbl 1215.03023
[15] Espírito Santo, J., Ivetić, J., Likavec, S.: Characterising strongly normalising intuitionistic terms. Fundamenta Informaticae (to appear 2011) · Zbl 1277.03003
[16] Gallier, J.: Typing untyped {\(\lambda\)}-terms, or reducibility strikes again! Ann. Pure Appl. Logic 91, 231–270 (1998) · Zbl 0930.03011
[17] Ghilezan, S.: Strong normalization and typability with intersection types. Notre Dame J. Formal Logic 37(1), 44–52 (1996) · Zbl 0859.03007
[18] Ghilezan, S., Ivetić, J., Lescanne, P., Žunić, D.: Intuitionistic sequent-style calculus with explicit structural rules. In: Bezhanishvili, N. (ed.) TbiLLC 2009. LNCS, vol. 6618, pp. 101–124. Springer, Heidelberg (2011) · Zbl 1341.03019
[19] Ghilezan, S., Likavec, S.: Computational interpretations of logics. In: Ognjanović, Z. (ed.) Collection of Papers, Special issue Logic in Computer Science, vol. 20(12), pp. 159–215. Mathematical Institute of Serbian Academy of Sciences and Arts (2009) · Zbl 1313.03002
[20] Herbelin, H.: A lambda calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61–75. Springer, Heidelberg (1995) · Zbl 1044.03509
[21] Howard, W.A.: The formulas-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479–490. Academic Press, London (1980)
[22] Kesner, D., Lengrand, S.: Resource operators for lambda-calculus. Inform. Comput. 205(4), 419–473 (2007) · Zbl 1111.68018
[23] Kesner, D., Renaud, F.: The prismoid of resources. In: Královič, R., Niwiński, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 464–476. Springer, Heidelberg (2009) · Zbl 1250.03024
[24] Kikuchi, K.: Simple proofs of characterizing strong normalization for explicit substitution calculi. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 257–272. Springer, Heidelberg (2007) · Zbl 1203.68076
[25] Matthes, R.: Characterizing strongly normalizing terms of a {\(\lambda\)}-calculus with generalized applications via intersection types. In: Hindley, J.R., et al. (eds.) ICALP Workshops 2000. Carleton Scientific (2000)
[26] Neergaard, P.M.: Theoretical pearls: A bargain for intersection types: a simple strong normalization proof. J. Funct. Program. 15(5), 669–677 (2005) · Zbl 1104.68013
[27] Pagani, M., della Rocca, S.R.: Solvability in resource lambda-calculus. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 358–373. Springer, Heidelberg (2010) · Zbl 1246.68086
[28] Parigot, M.: Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992) · Zbl 0925.03092
[29] Pottinger, G.: A type assignment for the strongly normalizable {\(\lambda\)}-terms. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561–577. Academic Press, London (1980)
[30] Regnier, L.: Une équivalence sur les lambda-termes. Theor. Comput Sci. 126(2), 281–292 (1994) · Zbl 0801.03013
[31] Rose, K.H.: CRSX - Combinatory Reduction Systems with Extensions. In: Schmidt-Schauß, M. (ed.) 22nd International Conference on Rewriting Techniques and Applications, RTA 2011. Leibniz International Proceedings in Informatics (LIPIcs), vol. 10, pp. 81–90. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2011)
[32] Rose, K.H.: Implementation Tricks That Make CRSX Tick. Talk at IFIP 1.6 Workshop, RDP 2011 (May 2011)
[33] Sallé, P.: Une extension de la théorie des types en lambda-calcul. In: Ausiello, G., Böhm, C. (eds.) ICALP 1978. LNCS, vol. 62, pp. 398–410. Springer, Heidelberg (1978)
[34] Schroeder-Heister, P., Došen, K.: Substructural Logics. Oxford University Press, UK (1993)
[35] Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symb. Logic 32, 198–212 (1967) · Zbl 0174.01202
[36] van Bakel, S.: Complete restrictions of the intersection type discipline. Theor. Comput Sci. 102(1), 135–163 (1992) · Zbl 0762.03006
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.