On abstract normalisation beyond neededness

DOI10.1016/J.TCS.2017.01.025MaRDI QIDQ683744zbMATH OpenOpenAlexFDO

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)

Full work available at URL https://arxiv.org/abs/1412.2118, http://hdl.handle.net/11336/72890

zbMATH Keywords

rewritingneedednesssequentialitynormalisationpattern calculi

Mathematics Subject Classification ID

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

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.

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

Cites work

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

Cited in

(5)

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

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)