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
We argue that
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: