The Pattern Matching Calculus

The operational semantics of functional programming languages is usually explained via special kinds of lambda-calculi and term rewriting systems (TRSs). One way to look at the relation between these two approaches is to consider lambda-calculi as internalisations of term rewriting systems: A function definable by a certain kind of term rewriting system, i.e., by a set of term rewriting rules, can be represented by a single expression in an appropriate lambda-calculus.

For example, simple applicative term rewriting is internalised by lambda-abstraction, and recursion is internalised by fixed-point combinators.

For definitions by pattern matching, so far the only available internalisation are case expressions.

We argue that case expressions mix too many different aspects of rewriting into a single syntactic construct, and propose pattern matching calculi as a more attractive alternative:

• Two separate syntactic categories: expressions and matchings
• Argument supply inside matchings liberated from its fixed position in case expressions
• Standard reduction rules exactly mirror the pattern matching semantics of Haskell
• PMC reduction is confluent and has a normalising strategy
• Changing a single rule allows interpretation of matching failure as an exception that may be caught in outer matchings, similar to the proposal of Erwig and Peyton Jones (2000); PMC allows a simple, direct definition of this idea.

Currently, the following material is available:

• The FLOPS 2004 paper Basic Pattern Matching Calculi: A Fresh View on Matching Failure
• The confluence proof.
• The technical report Basic Pattern Matching Calculi: Syntax, Reduction, Confluence, and Normalisation, a longer version of the FLOPS 2004 paper
• The MPC 2006 paper Bimonadic Semantics for Basic Pattern Matching Calculi, and a longer technical report containing all the proofs