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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Arbiser, Ariel
Publicado: 2006
Materias:
Artificial intelligence
Computer systems
Pattern matching
Theorem proving
Lambda-calculus
Separation theorems
Difference equations
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4098LNCS_n_p181_Arbiser
http://hdl.handle.net/20.500.12110/paper_03029743_v4098LNCS_n_p181_Arbiser
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_03029743_v4098LNCS_n_p181_Arbiser
record_format dspace
spelling paper:paper_03029743_v4098LNCS_n_p181_Arbiser2023-06-08T15:28:24Z A lambda-calculus with constructors Arbiser, Ariel 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. 2006 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4098LNCS_n_p181_Arbiser 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, Ariel
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.
author Arbiser, Ariel
author_facet Arbiser, Ariel
author_sort Arbiser, Ariel
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
publishDate 2006
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4098LNCS_n_p181_Arbiser
http://hdl.handle.net/20.500.12110/paper_03029743_v4098LNCS_n_p181_Arbiser
work_keys_str_mv AT arbiserariel alambdacalculuswithconstructors
AT arbiserariel lambdacalculuswithconstructors
_version_ 1768542789104041984

Ejemplares similares