The -λ Calculus with constructors: Syntax, confluence and separation
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 us...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , |
| Formato: | Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2009
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 05277caa a22006137a 4500 | ||
|---|---|---|---|
| 001 | PAPER-8534 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518203820.0 | ||
| 008 | 190411s2009 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-74049112161 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Arbiser, A. | |
| 245 | 1 | 4 | |a The -λ Calculus with constructors: Syntax, confluence and separation |
| 260 | |c 2009 | ||
| 270 | 1 | 0 | |m Arbiser, A.; Departamento de Computacin, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos AiresArgentina; email: arbiser@dc.uba.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a 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 | ||
| 504 | |a Baader, F., Nipkow, T., (1999) Rewriting and All That, , Addison-Wesley | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a Cerrito, S., Kesner, D., Pattern matching as cut elimination (1999) Logics in Computer Science (LICS'99), pp. 98-108. , IEEE Computer Society | ||
| 504 | |a Church, A., The calculi of lambda-conversion (1941) Annals of Mathematical Studies, 6. , Princeton | ||
| 504 | |a Cirstea, H., Kirchner, C., Rho-calculus, the rewriting calculus (1998) Fifth International Workshop on Constraints in Computational Logics, , Jerusalem, Israel | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a Jay, C.B., The pattern calculus (2004) ACM Trans. Program. Lang. Syst., 26 (6), pp. 911-937 | ||
| 504 | |a Jay, C.B., Kesner, D., Pure pattern calculus (2006) Lecture Notes in Computer Science, 3924, pp. 100-114. , Sestoft, P. (ed), Springer | ||
| 504 | |a Kahl, W., Basic pattern matching calculi: Syntax, reduction, confluence, and normalisation (2003) Technical Report 16, , Software Quality Research Laboratory, McMaster University | ||
| 504 | |a Leroy, X., The Objective Caml system release 3.11 (2008) Documentation and User's Manual, , http://caml.inria.fr/ | ||
| 504 | |a Milner, R., Tofte, M., Harper, R., (1990) The Definition of Standard ML, , MIT Press | ||
| 504 | |a Ŕios, A., (1993) Contribution ̀a l'́Etude des λ-calculs Avec Substitutions Explicites, , PhD thesis, Universit́e Paris 7 | ||
| 504 | |a 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 | ||
| 504 | |a Van Oostrom, V., Lambda calculus with patterns (1990) Technical Report IR-228, , Vrije Universiteit | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Departamento de Computacin, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina | ||
| 593 | |a PPS and Universit Paris 7 Case 7014, 2 Place Jussieu, 75251 PARIS Cedex 05, France | ||
| 690 | 1 | 0 | |a CHURCH-ROSSER PROPERTY |
| 690 | 1 | 0 | |a CONSTRUCTION PERMITS |
| 690 | 1 | 0 | |a DIVIDE-AND-CONQUER TECHNIQUE |
| 690 | 1 | 0 | |a REDUCTION RULES |
| 690 | 1 | 0 | |a SEMI-AUTOMATICS |
| 690 | 1 | 0 | |a SEPARATION THEOREM |
| 690 | 1 | 0 | |a PATTERN MATCHING |
| 690 | 1 | 0 | |a CALCULATIONS |
| 700 | 1 | |a Miquel, A. | |
| 700 | 1 | |a Ros, A. | |
| 773 | 0 | |d 2009 |g v. 19 |h pp. 581-631 |k n. 5 |p J. Funct. Program. |x 09567968 |w (AR-BaUEN)CENRE-1632 |t Journal of Functional Programming | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-74049112161&doi=10.1017%2fS0956796809007369&partnerID=40&md5=d113bfe0a677b6b8c43f69cced0490cf |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1017/S0956796809007369 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_09567968_v19_n5_p581_Arbiser |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_09567968_v19_n5_p581_Arbiser |y Registro en la Biblioteca Digital |
| 961 | |a paper_09567968_v19_n5_p581_Arbiser |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/article |a info:ar-repo/semantics/artículo |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 69487 | ||