2026-07-26T20:56:34Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3488 2024-03-06T10:34:16Z ddc:004 open_access

Normalisation for Dynamic Pattern Calculi Bonelli, Eduardo Kesner, Delia Lombardi, Carlos Rios, Alejandro Pattern calculi reduction strategies sequentiality neededness The Pure Pattern Calculus (PPC) extends the lambda-calculus, as well as the family of algebraic pattern calculi, with first-class patterns; that is, patterns can be passed as arguments, evaluated and returned as results. The notion of matching failure of the PPC not only provides a mechanism to define functions by pattern matching on cases but also supplies PPC with parallel-or-like, non-sequential behaviour. Therefore, devising normalising strategies for PPC to obtain well-behaved implementations turns out to be challenging. This paper focuses on normalising reduction strategies for PPC. We define a (multistep) strategy and show that it is normalising. The strategy generalises the leftmost-outermost strategy for lambda-calculus and is strictly finer than parallel-outermost. The normalisation proof is based on the notion of necessary set of redexes, a generalisation of the notion of needed redex encompassing non-sequential reduction systems. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Eduardo Bonelli and Delia Kesner and Carlos Lombardi and Alejandro Rios 2012 Is Part Of LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2012.117 urn:nbn:de:0030-drops-34889 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.117 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode