Navegar

Colección

Datos Estadísticas

Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

We present an extension of the λ(n)-calculus with a case construct that propagates through functions like a head linear substitution, and show that this construction permits to recover the expressiveness of ML-style pattern matching. We then prove that this system enjoys the ChurchRosser property using a semi-automatic divide and conquer technique by which we determine all the pairs of commuting subsystems of the formalism (considering all the possible combinations of the nine primitive reduction rules). Finally, we prove a separation theorem similar to Bhm's theorem for the whole formalism. © 2009 Cambridge University Press.

Registro:

Documento: Artículo
Título:The -λ Calculus with constructors: Syntax, confluence and separation
Autor:Arbiser, A.; Miquel, A.; Ros, A.
Filiación:Departamento de Computacin, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina
PPS and Universit Paris 7 Case 7014, 2 Place Jussieu, 75251 PARIS Cedex 05, France
Palabras clave:Church-Rosser property; Construction permits; Divide-and-conquer technique; Reduction rules; Semi-automatics; Separation theorem; Pattern matching; Calculations
Año:2009
Volumen:19
Número:5
Página de inicio:581
Página de fin:631
DOI: http://dx.doi.org/10.1017/S0956796809007369
Título revista:Journal of Functional Programming
Título revista abreviado:J. Funct. Program.
ISSN:09567968
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_09567968_v19_n5_p581_Arbiser

Referencias:

  • Arbiser, A., Miquel, A., Ŕios, A., A λ-calculus with constructors (2006) Lecture Notes in Computer Science, 4098. , International Conference of Rewriting Techniques and Applications. Springer-Verlag
  • Baader, F., Nipkow, T., (1999) Rewriting and All That, , Addison-Wesley
  • Barendregt, H., The lambda calculus: Its syntax and semantics (1984) Studies in Logic and the Foundations of Mathematics, 103. , J. Barwise D. Kaplan, H. J. Keisler, P. Suppes and A. S. Troelstra (eds), North-Holland
  • B̈ohm, C., Dezani-Ciancaglini, M., Peretti, P., Ronchi Della Rocha, S., A discrimination algorithm inside lambda-beta-calculus (1979) Theor. Comput. Sci., 8 (3), pp. 265-291
  • Cerrito, S., Kesner, D., Pattern matching as cut elimination (1999) Logics in Computer Science (LICS'99), pp. 98-108. , IEEE Computer Society
  • Church, A., The calculi of lambda-conversion (1941) Annals of Mathematical Studies, 6. , Princeton
  • Cirstea, H., Kirchner, C., Rho-calculus, the rewriting calculus (1998) Fifth International Workshop on Constraints in Computational Logics, , Jerusalem, Israel
  • Girard, J.-Y., Locus solum: From the rules of logic to the logic of rules (2001) Math. Struct. Comput. Sci., 11 (3), pp. 301-506
  • Hudak, P., Peyton-Jones, S., Wadler, P., (1992) Report on the Programming Language Haskell, A Non-strict, Purely Functional Language, , (Version 1.2). Sigplan Notices
  • Jay, C.B., The pattern calculus (2004) ACM Trans. Program. Lang. Syst., 26 (6), pp. 911-937
  • Jay, C.B., Kesner, D., Pure pattern calculus (2006) Lecture Notes in Computer Science, 3924, pp. 100-114. , Sestoft, P. (ed), Springer
  • Kahl, W., Basic pattern matching calculi: Syntax, reduction, confluence, and normalisation (2003) Technical Report 16, , Software Quality Research Laboratory, McMaster University
  • Leroy, X., The Objective Caml system release 3.11 (2008) Documentation and User's Manual, , http://caml.inria.fr/
  • Milner, R., Tofte, M., Harper, R., (1990) The Definition of Standard ML, , MIT Press
  • Ŕios, A., (1993) Contribution ̀a l'́Etude des λ-calculs Avec Substitutions Explicites, , PhD thesis, Universit́e Paris 7
  • Terese, (2003) Term Rewriting Systems, p. 55. , Marc Bezem, Jan Willem Klop and Roel de Vrijer (eds), Cambridge University Press. Cambridge Tracts in Theoretical Computer Science
  • Van Oostrom, V., Lambda calculus with patterns (1990) Technical Report IR-228, , Vrije Universiteit

Citas:

---------- APA ----------
Arbiser, A., Miquel, A. & Ros, A. (2009) . The -λ Calculus with constructors: Syntax, confluence and separation. Journal of Functional Programming, 19(5), 581-631.
http://dx.doi.org/10.1017/S0956796809007369
---------- CHICAGO ----------
Arbiser, A., Miquel, A., Ros, A. "The -λ Calculus with constructors: Syntax, confluence and separation" . Journal of Functional Programming 19, no. 5 (2009) : 581-631.
http://dx.doi.org/10.1017/S0956796809007369
---------- MLA ----------
Arbiser, A., Miquel, A., Ros, A. "The -λ Calculus with constructors: Syntax, confluence and separation" . Journal of Functional Programming, vol. 19, no. 5, 2009, pp. 581-631.
http://dx.doi.org/10.1017/S0956796809007369
---------- VANCOUVER ----------
Arbiser, A., Miquel, A., Ros, A. The -λ Calculus with constructors: Syntax, confluence and separation. J. Funct. Program. 2009;19(5):581-631.
http://dx.doi.org/10.1017/S0956796809007369