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:

Currently, the following material is available:

Wolfram Kahl