Abstract:
The pure pattern calculus generalises the pure lambda-calculus
by basing computation on pattern-matching instead of beta-reduction.
The simplicity and power of the calculus derive from allowing any
term to be a pattern. As well as supporting a uniform approach to functions,
it supports a uniform approach to data structures which underpins
two new forms of polymorphism. Path polymorphism supports searches
or queries along all paths through an arbitrary data structure. Pattern
polymorphism supports the dynamic creation and evaluation of patterns,
so that queries can be customised in reaction to new information about
the structures to be encountered. In combination, these features provide
a natural account of tasks such as programming with XML paths.
As the variables used in matching can now be eliminated by reduction
it is necessary to separate them from the binding variables used to
control scope. Then standard techniques suffice to ensure that reduction
progresses and to establish confluence of reduction.
