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