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
Autores principales: Arbiser, A., Miquel, A., Ríos, A.
Formato: SER
Materias:
Artificial intelligence
Computer systems
Pattern matching
Theorem proving
Lambda-calculus
Separation theorems
Difference equations
Acceso en línea: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
Descripción
Sumario: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.

Ejemplares similares