On abstract normalisation beyond neededness

DOI10.1016/J.TCS.2017.01.025zbMATH Open1387.68143arXiv1412.2118OpenAlexW2963588438MaRDI QIDQ683744FDOQ683744

Authors: Eduardo Bonelli, Delia Kesner, Carlos Lombardi, A. Ríos 

Publication date: 9 February 2018

Published in: Theoretical Computer Science (Search for Journal in Brave)

Abstract: We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focussing on the notion of necessary sets, those which contain at least one redex that cannot be avoided in order to reach a normal form. This is particularly appealing in the setting of non-sequential rewrite systems, in which terms that are not in normal form may not have any needed redex. We first prove a normalisation theorem for abstract rewrite systems (ARS), a general rewriting framework encompassing many rewriting systems developed by P-A.Melli`es in his PhD thesis. The theorem states that multistep strategies reducing so called necessary and never-gripping sets of redexes at a time are normalising in any ARS. Gripping refers to an abstract property reflecting the behavior of higher-order substitution. We then apply this result to the particular case of PPC, a calculus of patterns and to the lambda-calculus with parallel-or.

Full work available at URL: https://arxiv.org/abs/1412.2118

Recommendations

• Normalisation for dynamic pattern calculi
• Axiomatic rewriting theory II: the   -calculus enjoys finite normalisation cones
• Stable results and relative normalization
• On Normalisation of Infinitary Combinatory Reduction Systems
• scientific article; zbMATH DE number 6792365

zbMATH Keywords

rewritingneedednesssequentialitynormalisationpattern calculi

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computing in systems described by equations
• First-class patterns
• Pattern Calculus
• On equal \(\mu \)-terms
• Sequential evaluation strategies for parallel-or and related reduction systems
• A sequential reduction strategy
• Programming in equational logic: Beyond strong sequentiality
• Title not available (Why is that?)
• Title not available (Why is that?)
• Beta reduction is invariant, indeed
• Normalisation for dynamic pattern calculi
• A nonstandard standardization theorem
• Programming Languages and Systems

Cited In (5)

• Normalisation for dynamic pattern calculi
• Abstract strategies and coherence
• An abstract Böhm-normalization
• Factorization and normalization, essentially
• Pure pattern calculus à la de Bruijn

This page was built for publication: On abstract normalisation beyond neededness

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q683744)