A lambda-calculus with constructors
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 u...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
Springer Verlag
2006
|
| Acceso en línea: | Registro en Scopus Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 04795caa a22005777a 4500 | ||
|---|---|---|---|
| 001 | PAPER-6938 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518203639.0 | ||
| 008 | 190411s2006 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-33749412088 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Arbiser, A. | |
| 245 | 1 | 2 | |a A lambda-calculus with constructors |
| 260 | |b Springer Verlag |c 2006 | ||
| 270 | 1 | 0 | |m Arbiser, A.; Departamento de Computación, 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., Ríos, A., (2006) A λ-Calculus with Constructors, , Manuscript, available from the web pages of the authors | ||
| 504 | |a Baader, F., Nipkow, T., (1999) Rewriting and All That, , Addison-Wesley | ||
| 504 | |a Barendregt, H., (1984) Studies in Logic and the Foundations of Mathematics, 103. , The Lambda Calculus: Its Syntax and Semantics, North-Holland | ||
| 504 | |a 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 | ||
| 504 | |a Cerrito, S., Kesner, D., Pattern matching as cut elimination (1999) Logics in Computer Science (LICS'99), pp. 98-108 | ||
| 504 | |a Church, A., (1941) Annals of Mathematical Studies, 6. , The calculi of lambda-conversion, Princeton | ||
| 504 | |a Cirstea, H., Kirchner, C., Rho-calculus, the rewriting calculus (1998) 5th International Workshop on Constraints in Computational Logics | ||
| 504 | |a 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 | ||
| 504 | |a Jay, C.B., The pattern calculus (2004) ACM Transactions on Programming Languages and Systems, 26 (6), pp. 911-937 | ||
| 504 | |a Jones, S.P., (2003) The Revised Haskell 98 Report, , http://haskell.org/, Cambridge Univ. Press | ||
| 504 | |a 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 | ||
| 504 | |a Milner, R., Tofte, M., Harper, R., (1990) The Definition of Standard ML, , MIT Press | ||
| 504 | |a The Objective Caml Language, , http://caml.inria.fr/ | ||
| 504 | |a Van Oostrom, V., Lambda calculus with patterns (1990) Technical Report, IR-228. , Vrije Universiteit, AmsterdamA4 - | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina | ||
| 593 | |a PPS, Université Paris 7, Case 7014, 2 Place Jussieu, 75251 PARIS Cedex 05, France | ||
| 690 | 1 | 0 | |a ARTIFICIAL INTELLIGENCE |
| 690 | 1 | 0 | |a COMPUTER SYSTEMS |
| 690 | 1 | 0 | |a PATTERN MATCHING |
| 690 | 1 | 0 | |a THEOREM PROVING |
| 690 | 1 | 0 | |a LAMBDA-CALCULUS |
| 690 | 1 | 0 | |a SEPARATION THEOREMS |
| 690 | 1 | 0 | |a DIFFERENCE EQUATIONS |
| 700 | 1 | |a Miquel, A. | |
| 700 | 1 | |a Ríos, A. | |
| 711 | 2 | |c Seattle, WA |d 12 August 2006 through 14 August 2006 |g Código de la conferencia: 68260 | |
| 773 | 0 | |d Springer Verlag, 2006 |g v. 4098 LNCS |h pp. 181-196 |p Lect. Notes Comput. Sci. |n Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |x 03029743 |w (AR-BaUEN)CENRE-983 |z 3540368345 |z 9783540368342 |t 17th International Conference on Term Rewriting and Applications, RTA 2006 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-33749412088&partnerID=40&md5=077555d73eb0ad51e4507b734542b4e7 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_03029743_v4098LNCS_n_p181_Arbiser |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4098LNCS_n_p181_Arbiser |y Registro en la Biblioteca Digital |
| 961 | |a paper_03029743_v4098LNCS_n_p181_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 | ||
| 963 | |a VARI | ||
| 999 | |c 67891 | ||