Normalisation for Dynamic Pattern Calculi

Authors Eduardo Bonelli, Delia Kesner, Carlos Lombardi, Alejandro Rios

Thumbnail PDF


  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Eduardo Bonelli
Delia Kesner
Carlos Lombardi
Alejandro Rios

Cite AsGet BibTex

Eduardo Bonelli, Delia Kesner, Carlos Lombardi, and Alejandro Rios. Normalisation for Dynamic Pattern Calculi. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 117-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


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.
  • Pattern calculi
  • reduction strategies
  • sequentiality
  • neededness


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads