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:
| Autores principales: | , , |
|---|---|
| Formato: | SER |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_03029743_v4098LNCS_n_p181_Arbiser |
| Aporte de: |
| id |
todo:paper_03029743_v4098LNCS_n_p181_Arbiser |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_03029743_v4098LNCS_n_p181_Arbiser2023-10-03T15:18:58Z A lambda-calculus with constructors Arbiser, A. Miquel, A. Ríos, A. Artificial intelligence Computer systems Pattern matching Theorem proving Lambda-calculus Separation theorems Difference equations 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. Fil:Arbiser, A. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v4098LNCS_n_p181_Arbiser |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Artificial intelligence Computer systems Pattern matching Theorem proving Lambda-calculus Separation theorems Difference equations |
| spellingShingle |
Artificial intelligence Computer systems Pattern matching Theorem proving Lambda-calculus Separation theorems Difference equations Arbiser, A. Miquel, A. Ríos, A. A lambda-calculus with constructors |
| topic_facet |
Artificial intelligence Computer systems Pattern matching Theorem proving Lambda-calculus Separation theorems Difference equations |
| description |
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. |
| format |
SER |
| author |
Arbiser, A. Miquel, A. Ríos, A. |
| author_facet |
Arbiser, A. Miquel, A. Ríos, A. |
| author_sort |
Arbiser, A. |
| title |
A lambda-calculus with constructors |
| title_short |
A lambda-calculus with constructors |
| title_full |
A lambda-calculus with constructors |
| title_fullStr |
A lambda-calculus with constructors |
| title_full_unstemmed |
A lambda-calculus with constructors |
| title_sort |
lambda-calculus with constructors |
| url |
http://hdl.handle.net/20.500.12110/paper_03029743_v4098LNCS_n_p181_Arbiser |
| work_keys_str_mv |
AT arbisera alambdacalculuswithconstructors AT miquela alambdacalculuswithconstructors AT riosa alambdacalculuswithconstructors AT arbisera lambdacalculuswithconstructors AT miquela lambdacalculuswithconstructors AT riosa lambdacalculuswithconstructors |
| _version_ |
1782030796159188992 |