Navegar

Colección

Datos Estadísticas

Artículo

Barenbaum, P.; Ciruelos, G.; Ryu S. "Factoring Derivation Spaces via Intersection Types" (2018) 16th Asian Symposium on Programming Languages and Systems, APLAS 2018. 11275 LNCS:24-44
El editor solo permite decargar el artículo en su versión post-print desde el repositorio. Por favor, si usted posee dicha versión, enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

In typical non-idempotent intersection type systems, proof normalization is not confluent. In this paper we introduce a confluent non-idempotent intersection type system for the -calculus. Typing derivations are presented using proof term syntax. The system enjoys good properties: subject reduction, strong normalization, and a very regular theory of residuals. A correspondence with the -calculus is established by simulation theorems. The machinery of non-idempotent intersection types allows us to track the usage of resources required to obtain an answer. In particular, it induces a notion of garbage: a computation is garbage if it does not contribute to obtaining an answer. Using these notions, we show that the derivation space of a -term may be factorized using a variant of the Grothendieck construction for semilattices. This means, in particular, that any derivation in the -calculus can be uniquely written as a garbage-free prefix followed by garbage. © 2018, Springer Nature Switzerland AG.

Registro:

Documento: Artículo
Título:Factoring Derivation Spaces via Intersection Types
Autor:Barenbaum, P.; Ciruelos, G.; Ryu S.
Filiación:Departamento de Computación, FCEyN, UBA, Buenos Aires, Argentina
IRIF, Université Paris 7, Paris, France
Palabras clave:Derivation space; Intersection types; Lambda calculus; Computation theory; Differentiation (calculus); Machinery; Derivation space; Garbage-free; Intersection types; Lambda calculus; Semilattices; Simulation theorem; Strong normalization; Subject reduction; Calculations
Año:2018
Volumen:11275 LNCS
Página de inicio:24
Página de fin:44
DOI: http://dx.doi.org/10.1007/978-3-030-02768-1_2
Título revista:16th Asian Symposium on Programming Languages and Systems, APLAS 2018
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v11275LNCS_n_p24_Barenbaum

Referencias:

  • Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C., (2014) A Nonstandard Standardization Theorem, pp. 659-670. , POPL 2014, 20–21 January 2014, San Diego, CA, USA
  • Asperti, A., Lévy, J., The cost of usage in the lambda-calculus (2013) 28Th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pp. 293-300. , 25–28 June 2013, New Orleans, LA, USA
  • Barendregt, H.P., Kennaway, J.R., Klop, J.W., Sleep, M.R., Needed reduction and spine strategies for the lambda calculus (1987) Inf. Comput., 75 (3), pp. 191-231
  • Barendregt, H., (1984) The Lambda Calculus: Its Syntax and Semantics, 103. , vol., Elsevier, Amsterdam
  • Bernadet, A., Lengrand, S.J., (2013) Non-Idempotent Intersection Types and Strong Normalisation, , arXiv preprint arXiv
  • Boudol, G., The lambda-calculus with multiplicities (1993) CONCUR 1993. LNCS, 715, pp. 1-6. , https://doi.org/10.1007/3-540-57208-21, In: Best, E. (ed.), Springer, Heidelberg
  • Bucciarelli, A., Kesner, D., Ronchi Della Rocca, S., The inhabitation problem for non-idempotent intersection types (2014) TCS 2014. LNCS, 8705, pp. 341-354. , https://doi.org/10.1007/978-3-662-44602-726, Diaz, J., Lanese, I., Sangiorgi, D. (eds.), pp., Springer, Heidelberg
  • Bucciarelli, A., Kesner, D., Ventura, D., Non-idempotent intersection types for the lambda-calculus (2017) Log. J. IGPL, 25 (4), pp. 431-464
  • Carvalho, D.D., (2007) Sémantiques De La Logique linéaire Et Temps De Calcul, , Ph.D. thesis, Ecole Doctorale Physique et Sciences de la Matière (Marseille)
  • Church, A., Rosser, J.B., Some properties of conversion (1936) Trans. Am. Math. Soc., 39 (3), pp. 472-482
  • Rodríguez, G.C., Factorización de derivaciones a través de tipos intersección. Mas-ter’s thesis, Facultad de Ciencias Exactas y Naturales (2018) Universidad De Buenos Aires, , http://www.dc.uba.ar/academica/tesis-de-licenciatura/2018/ciruelos.pdf
  • Coppo, M., Dezani-Ciancaglini, M., A new type assignment for lambda-terms (1978) Arch. Math. Log., 19 (1), pp. 139-156
  • Curry, H., Feys, R., (1958) Combinatory Logic, 1. , North-Holland Publishing Company, Amsterdam
  • Dershowitz, N., Jouannaud, J.-P., Klop, J.W., Open problems in rewriting (1991) RTA 1991. LNCS, 488, pp. 445-456. , https://doi.org/10.1007/3-540-53904-2120, Book, R.V. (ed.), pp., Springer, Heidelberg
  • Ehrhard, T., Collapsing non-idempotent intersection types (2012) Lipics-Leibniz International Proceedings in Informatics, 16. , vol., Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik
  • Ehrhard, T., Regnier, L., The differential lambda-calculus (2003) Theor. Comput. Sci., 309, pp. 1-41
  • Ehrhard, T., Regnier, L., Uniformity and the taylor expansion of ordinary lambda-terms (2008) Theor. Comput. Sci., 403 (2-3), pp. 347-372
  • Gardner, P., Discovering needed reductions using type theory (1994) TACS 1994. LNCS, 789, pp. 555-574. , https://doi.org/10.1007/3-540-57887-0115, Hagiya, M., Mitchell, J.C. (eds.), pp., Springer, Heidelberg
  • Girard, J.Y., Linear logic (1987) Theor. Comput. Sci., 50 (1), pp. 1-101
  • Kesner, D., Reasoning about call-by-need by means of types (2016) Fossacs 2016. LNCS, 9634, pp. 424-441. , https://doi.org/10.1007/978-3-662-49630-525, Jacobs, B., Löding, C. (eds.), pp., Springer, Heidelberg
  • Kesner, D., Lengrand, S., Resource operators for λ-calculus (2007) Inf. Comput., 205 (4), pp. 419-473
  • Kesner, D., Renaud, F., The prismoid of resources (2009) MFCS 2009. LNCS, 5734, pp. 464-476. , https://doi.org/10.1007/978-3-642-03816-740, Královič, R., Niwiński, D. (eds.), pp., Springer, Heidelberg
  • Kesner, D., Ríos, A., Viso, A., Call-by-need, neededness and all that (2018) Fossacs 2018. LNCS, 10803, pp. 241-257. , https://doi.org/10.1007/978-3-319-89366-213, Baier, C., Dal Lago, U. (eds.), pp., Springer, Cham
  • Kfoury, A.J., A linearization of the lambda-calculus and consequences. Technical report, Boston University (1996) Computer Science Department
  • Laneve, C., Distributive evaluations of λ-calculus (1994) Fundam. Inform., 20 (4), pp. 333-352
  • Lévy, J.J., Réductions correctes et optimales dans le lambda-calcul. Ph.D. thesis (1978) Université De Paris, p. 7
  • Lévy, J.J., Redexes are stable in the λ-calculus (2017) Math. Struct. Comput. Sci., 27 (5), pp. 738-750
  • Mazza, D., Pellissier, L., Vial, P., (2018) Polyadic Approximations, Fibrations and Intersection Types. Proc. ACM Program. Lang. 2(POPL), 6
  • Melliès, P.A., (1996) Description Abstraite Des systèmes De réécriture. Ph.D. Thesis, , Université Paris 7, December
  • Melliès, P.-A., A factorisation theorem in rewriting theory (1997) CTCS 1997. LNCS, 1290, pp. 49-68. , https://doi.org/10.1007/BFb0026981, Moggi, E., Rosolini, G. (eds.), pp., Springer, Heidelberg
  • Melliès, P.-A., Axiomatic rewriting theory VI: Residual theory revisited (2002) RTA 2002. LNCS, 2378, pp. 24-50. , https://doi.org/10.1007/3-540-45610-44, Tison, S. (ed.), pp., Springer, Heidelberg
  • Melliès, P.-A., Axiomatic rewriting theory I: A diagrammatic standardization theorem (2005) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, 3838, pp. 554-638. , https://doi.org/10.1007/1160154823, Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.), pp., Springer, Heidelberg
  • Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science (2003) Cambridge University Press, 55
  • Vial, P., (2017) Non-Idempotent Typing Operators, beyond the Lambda-Calculus. Ph.D. Thesis, , Université Paris 7, December
  • Zilli, M.V., Reduction graphs in the lambda calculus (1984) Theor. Comput. Sci., 29, pp. 251-275. , https://doi.org/10.1016/0304-3975(84)90002-1

Citas:

---------- APA ----------
Barenbaum, P., Ciruelos, G. & Ryu S. (2018) . Factoring Derivation Spaces via Intersection Types. 16th Asian Symposium on Programming Languages and Systems, APLAS 2018, 11275 LNCS, 24-44.
http://dx.doi.org/10.1007/978-3-030-02768-1_2
---------- CHICAGO ----------
Barenbaum, P., Ciruelos, G., Ryu S. "Factoring Derivation Spaces via Intersection Types" . 16th Asian Symposium on Programming Languages and Systems, APLAS 2018 11275 LNCS (2018) : 24-44.
http://dx.doi.org/10.1007/978-3-030-02768-1_2
---------- MLA ----------
Barenbaum, P., Ciruelos, G., Ryu S. "Factoring Derivation Spaces via Intersection Types" . 16th Asian Symposium on Programming Languages and Systems, APLAS 2018, vol. 11275 LNCS, 2018, pp. 24-44.
http://dx.doi.org/10.1007/978-3-030-02768-1_2
---------- VANCOUVER ----------
Barenbaum, P., Ciruelos, G., Ryu S. Factoring Derivation Spaces via Intersection Types. Lect. Notes Comput. Sci. 2018;11275 LNCS:24-44.
http://dx.doi.org/10.1007/978-3-030-02768-1_2