Pattern calculus bases all computation on
pattern matching
In computer science, pattern matching is the act of checking a given sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually must be exact: "either it will or will not be a ...
of a very general kind. Like
lambda calculus
In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...
, it supports a
uniform treatment of
function evaluation. Also, it allows functions to be
passed as arguments and returned as results. In addition, pattern calculus supports
uniform access to the internal structure of arguments, be they pairs
or
list
A list is a Set (mathematics), set of discrete items of information collected and set forth in some format for utility, entertainment, or other purposes. A list may be memorialized in any number of ways, including existing only in the mind of t ...
s or
tree
In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, e.g., including only woody plants with secondary growth, only ...
s. Also, it allows patterns to be passed as arguments and
returned as results. Uniform access is illustrated by a
pattern-matching function that computes the size of an
arbitrary
data structure
In computer science, a data structure is a data organization and storage format that is usually chosen for Efficiency, efficient Data access, access to data. More precisely, a data structure is a collection of data values, the relationships amo ...
. In the notation of the
programming language
A programming language is a system of notation for writing computer programs.
Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
bondi, it is given by the
recursive function
let rec size =
, x y -> (size x) + (size y)
, x -> 1
The second, or ''default case'' matches the pattern
against the argument and returns . This
case is used only if the matching failed in the first case. The
first, or ''special case'' matches against any ''compound'', such
as a non-empty list, or pair. Matching binds to the left component
and to the right component. Then the body of the case adds the
sizes of these components together.
Similar techniques yield generic queries for searching and updating. Combining recursion and decomposition in this way yields ''
path polymorphism''.
The ability to pass patterns as parameters (''pattern polymorphism'') is illustrated by defining a
generic eliminator. Suppose given constructors for creating
the leaves of a tree, and for converting numbers into
counters. The corresponding eliminators are then
elimLeaf = , Leaf y -> y
elimCount = , Count y -> y
For example, evaluates to as does .
These examples can be produced by applying the generic eliminator
to the constructors in question. It is defined by
elim = , x -> , x y -> y
Now evaluates to
, Leaf y -> y which is equivalent to . Also is equivalent to .
In general, the curly braces contain the bound variables of the
pattern, so that is free and is bound in
, x y -> y.
External links
Archive mirror of the links below (which are no longer online)* — the original paper, but not most general.
*
*
bondi programming language research site*
{{refend
Lambda calculus