Artículo
Arbiser, A.; Miquel, A.; Ríos, A. "A lambda-calculus with constructors" (2006) 17th International Conference on Term Rewriting and Applications, RTA 2006. 4098 LNCS:181-196
Consulte la política de Acceso Abierto del editor
Abstract:
We present an extension of the λ(η)-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 Church-Rosser 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 Böhm's theorem for the whole formalism. © Springer-Verlag Berlin Heidelberg 2006.
Registro:
| Documento: | Artículo |
| Título: | A lambda-calculus with constructors |
| Autor: | Arbiser, A.; Miquel, A.; Ríos, A. |
| Ciudad: | Seattle, WA |
| Filiación: | Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina PPS, Université Paris 7, Case 7014, 2 Place Jussieu, 75251 PARIS Cedex 05, France |
| Palabras clave: | Artificial intelligence; Computer systems; Pattern matching; Theorem proving; Lambda-calculus; Separation theorems; Difference equations |
| Año: | 2006 |
| Volumen: | 4098 LNCS |
| Página de inicio: | 181 |
| Página de fin: | 196 |
| Título revista: | 17th International Conference on Term Rewriting and Applications, RTA 2006 |
| Título revista abreviado: | Lect. Notes Comput. Sci. |
| ISSN: | 03029743 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4098LNCS_n_p181_Arbiser |
Referencias:
- Arbiser, A., Miquel, A., Ríos, A., (2006) A λ-Calculus with Constructors, , Manuscript, available from the web pages of the authors
- Baader, F., Nipkow, T., (1999) Rewriting and All That, , Addison-Wesley
- Barendregt, H., (1984) Studies in Logic and the Foundations of Mathematics, 103. , The Lambda Calculus: Its Syntax and Semantics, North-Holland
- Böhm, C., Dezani-Ciancaglini, M., Peretti, P., Della Rocha, S.R., A discrimination algorithm inside lambda-beta-calculus (1979) Theoretical Computer Science, 8 (3), pp. 265-291
- Cerrito, S., Kesner, D., Pattern matching as cut elimination (1999) Logics in Computer Science (LICS'99), pp. 98-108
- Church, A., (1941) Annals of Mathematical Studies, 6. , The calculi of lambda-conversion, Princeton
- Cirstea, H., Kirchner, C., Rho-calculus, the rewriting calculus (1998) 5th International Workshop on Constraints in Computational Logics
- Girard, J.-Y., Locus solum: From the rules of logic to the logic of rules (2001) Mathematical Structures in Computer Science, 11 (3), pp. 301-506
- Jay, C.B., The pattern calculus (2004) ACM Transactions on Programming Languages and Systems, 26 (6), pp. 911-937
- Jones, S.P., (2003) The Revised Haskell 98 Report, , http://haskell.org/, Cambridge Univ. Press
- Kahl, W., Basic pattern matching calculi: A fresh view on matching failure (2004) LNCS, 2998, pp. 276-290. , Y. Kameyama and P. Stuckey, editors, Functional and Logic Programming, Proceedings of FLOPS 2004, Springer
- Milner, R., Tofte, M., Harper, R., (1990) The Definition of Standard ML, , MIT Press
- The Objective Caml Language, , http://caml.inria.fr/
- Van Oostrom, V., Lambda calculus with patterns (1990) Technical Report, IR-228. , Vrije Universiteit, AmsterdamA4 -
Citas:
---------- APA ----------
Arbiser, A., Miquel, A. & Ríos, A. (2006) . A lambda-calculus with constructors. 17th International Conference on Term Rewriting and Applications, RTA 2006, 4098 LNCS, 181-196.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4098LNCS_n_p181_Arbiser [ ]
---------- CHICAGO ----------
Arbiser, A., Miquel, A., Ríos, A. "A lambda-calculus with constructors" . 17th International Conference on Term Rewriting and Applications, RTA 2006 4098 LNCS (2006) : 181-196.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4098LNCS_n_p181_Arbiser [ ]
---------- MLA ----------
Arbiser, A., Miquel, A., Ríos, A. "A lambda-calculus with constructors" . 17th International Conference on Term Rewriting and Applications, RTA 2006, vol. 4098 LNCS, 2006, pp. 181-196.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4098LNCS_n_p181_Arbiser [ ]
---------- VANCOUVER ----------
Arbiser, A., Miquel, A., Ríos, A. A lambda-calculus with constructors. Lect. Notes Comput. Sci. 2006;4098 LNCS:181-196.Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4098LNCS_n_p181_Arbiser [ ]
