Basic Pattern Matching Calculi: Syntax, Reduction, Confluence, and Normalisation

The pattern matching calculus is a refinement of λ-calculus that integrates mechanisms appropriate for fine-grained modelling of non-strict pattern matching. In comparison with the functional rewriting strategy that is usually employed to define the operational semantics of pattern-matching in non-strict functional programming languages like Haskell or Clean, the pattern matching calculus allows simpler and more local definitions to achieve the same effects. The main device of the calculus is to further emphasise the clear distinction between matching failure and undefinedness already discussed in the literature by embedding into expressions the separate syntactic category of matchings. This separation is also important to properly restrain the possible effects of the non-monotonicity that a naïve treatment of matching alternatives would exhibit. The language arising from that distinction turns out to naturally encompass the pattern guards of Peyton Jones and Erwig and conventional Boolean guards as special cases of the intermediate stages of matching reduction. By allowing a confluent reduction system and a normalising strategy, the pattern matching calculu