zbMATH — the first resource for mathematics

Metaconfluence of calculi with explicit substitutions at a distance. (English) Zbl 1360.68324
Raman, Venkatesh (ed.) et al., 34th international conference on foundation of software technology and theoretical computer science, FSTTCS 2014, New Delhi, India, December 15–17, 2014. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-77-4). LIPIcs – Leibniz International Proceedings in Informatics 29, 391-402 (2014).
Summary: Confluence is a key property of rewriting calculi that guarantees uniqueness of normal-forms when they exist. Metaconfluence is even more general, and guarantees confluence on open/meta terms, i.e. terms with holes, called metavariables that can be filled up with other (open/meta) terms. The difficulty to deal with open terms comes from the fact that the structure of metaterms is only partially known, so that some reduction rules became blocked by the metavariables. In this work, we establish metaconfluence for a family of calculi with explicit substitutions (ES) that enjoy preservation of strong-normalization (PSN) and that act at a distance. For that, we first extend the notion of reduction on metaterms in such a way that explicit substitutions are never structurally moved, i.e. they also act at a distance on metaterms. The resulting reduction relations are still rewriting systems, i.e. they do not include equational axioms, thus providing for the first time an interesting family of \(\lambda\)-calculi with explicit substitutions that enjoy both PSN and metaconfluence without requiring sophisticated notions of reduction modulo a set of equations.
For the entire collection see [Zbl 1329.68036].

68N18 Functional programming and lambda calculus
68Q42 Grammars and rewriting systems
Full Text: DOI