The -λ Calculus with constructors: Syntax, confluence and separation

We present an extension of the λ(n)-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 ChurchRosser property us...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Arbiser, A., Miquel, A., Ros, A.
Formato: JOUR
Materias:
Church-Rosser property
Construction permits
Divide-and-conquer technique
Reduction rules
Semi-automatics
Separation theorem
Pattern matching
Calculations
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_09567968_v19_n5_p581_Arbiser
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_09567968_v19_n5_p581_Arbiser
record_format dspace
spelling todo:paper_09567968_v19_n5_p581_Arbiser2023-10-03T15:52:18Z The -λ Calculus with constructors: Syntax, confluence and separation Arbiser, A. Miquel, A. Ros, A. Church-Rosser property Construction permits Divide-and-conquer technique Reduction rules Semi-automatics Separation theorem Pattern matching Calculations We present an extension of the λ(n)-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 ChurchRosser 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 Bhm's theorem for the whole formalism. © 2009 Cambridge University Press. Fil:Arbiser, A. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_09567968_v19_n5_p581_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 Church-Rosser property
Construction permits
Divide-and-conquer technique
Reduction rules
Semi-automatics
Separation theorem
Pattern matching
Calculations
spellingShingle Church-Rosser property
Construction permits
Divide-and-conquer technique
Reduction rules
Semi-automatics
Separation theorem
Pattern matching
Calculations
Arbiser, A.
Miquel, A.
Ros, A.
The -λ Calculus with constructors: Syntax, confluence and separation
topic_facet Church-Rosser property
Construction permits
Divide-and-conquer technique
Reduction rules
Semi-automatics
Separation theorem
Pattern matching
Calculations
description We present an extension of the λ(n)-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 ChurchRosser 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 Bhm's theorem for the whole formalism. © 2009 Cambridge University Press.
format JOUR
author Arbiser, A.
Miquel, A.
Ros, A.
author_facet Arbiser, A.
Miquel, A.
Ros, A.
author_sort Arbiser, A.
title The -λ Calculus with constructors: Syntax, confluence and separation
title_short The -λ Calculus with constructors: Syntax, confluence and separation
title_full The -λ Calculus with constructors: Syntax, confluence and separation
title_fullStr The -λ Calculus with constructors: Syntax, confluence and separation
title_full_unstemmed The -λ Calculus with constructors: Syntax, confluence and separation
title_sort -λ calculus with constructors: syntax, confluence and separation
url http://hdl.handle.net/20.500.12110/paper_09567968_v19_n5_p581_Arbiser
work_keys_str_mv AT arbisera thelcalculuswithconstructorssyntaxconfluenceandseparation
AT miquela thelcalculuswithconstructorssyntaxconfluenceandseparation
AT rosa thelcalculuswithconstructorssyntaxconfluenceandseparation
AT arbisera lcalculuswithconstructorssyntaxconfluenceandseparation
AT miquela lcalculuswithconstructorssyntaxconfluenceandseparation
AT rosa lcalculuswithconstructorssyntaxconfluenceandseparation
_version_ 1782030144289898496

Ejemplares similares