In
rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a well-formed formula, formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewr ...
, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation.
Some authors use the term to refer to an
evaluation strategy
In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the f ...
.
Definitions
Formally, for an
abstract rewriting system
In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviated ARS) is a formalism that captures the quintessential notion and properties of rewriting s ...
, a reduction strategy
is a
binary relation
In mathematics, a binary relation associates elements of one set, called the ''domain'', with elements of another set, called the ''codomain''. A binary relation over Set (mathematics), sets and is a new set of ordered pairs consisting of ele ...
on
with
, where
is the
transitive closure
In mathematics, the transitive closure of a binary relation on a set is the smallest relation on that contains and is transitive. For finite sets, "smallest" can be taken in its usual sense, of having the fewest related pairs; for infinite ...
of
(but not the reflexive closure).
In addition the normal forms of the strategy must be the same as the normal forms of the original rewriting system, i.e. for all
, there exists a
with
iff
.
A ''one step'' reduction strategy is one where
. Otherwise it is a ''many step'' strategy.
A ''deterministic'' strategy is one where
is a
partial function
In mathematics, a partial function from a set to a set is a function from a subset of (possibly itself) to . The subset , that is, the domain of viewed as a function, is called the domain of definition of . If equals , that is, if is de ...
, i.e. for each
there is at most one
such that
. Otherwise it is a ''nondeterministic'' strategy.
[
]
Term rewriting
In a term rewriting system
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or red ...
a rewriting strategy specifies, out of all the reducible subterms ( redexes), which one should be reduced (''contracted'') within a term.
One-step strategies for term rewriting include:[
* leftmost-innermost: in each step the leftmost of the innermost redexes is contracted, where an innermost redex is a redex not containing any redexes]
* leftmost-outermost: in each step the leftmost of the outermost redexes is contracted, where an outermost redex is a redex not contained in any redexes
* rightmost-innermost, rightmost-outermost: similarly
Many-step strategies include:[
* parallel-innermost: reduces all innermost redexes simultaneously. This is well-defined because the redexes are pairwise disjoint.
* parallel-outermost: similarly
* Gross-Knuth reduction, also called full substitution or Kleene reduction:][ all redexes in the term are simultaneously reduced
Parallel outermost and Gross-Knuth reduction are ''hypernormalizing'' for all almost-orthogonal term rewriting systems, meaning that these strategies will eventually reach a normal form if it exists, even when performing (finitely many) arbitrary reductions between successive applications of the strategy.
Stratego is a ]domain-specific language
A domain-specific language (DSL) is a computer language specialized to a particular application domain. This is in contrast to a general-purpose language (GPL), which is broadly applicable across domains. There are a wide variety of DSLs, ranging f ...
designed specifically for programming term rewriting strategies.
Lambda calculus
In the context of the lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
, ''normal-order reduction'' refers to leftmost-outermost reduction in the sense given above. Normal-order reduction is normalizing, in the sense that if a term has a normal form, then normal‐order reduction will eventually reach it, hence the name normal. This is known as the standardization theorem.
''Leftmost reduction'' is sometimes used to refer to normal order reduction, as with a pre-order traversal
In computer science, tree traversal (also known as tree search and walking the tree) is a form of graph traversal and refers to the process of visiting (e.g. retrieving, updating, or deleting) each node in a tree data structure, exactly once. S ...
the notions coincide, and similarly the leftmost-outermost redex is the redex with leftmost starting character when the lambda term is considered as a string of characters. When "leftmost" is defined using an in-order traversal
In computer science, tree traversal (also known as tree search and walking the tree) is a form of graph traversal and refers to the process of visiting (e.g. retrieving, updating, or deleting) each node in a tree data structure, exactly once. S ...
the notions are distinct. For example, in the term with defined here
Here is an adverb that means "in, on, or at this place". It may also refer to:
Software
* Here Technologies, a mapping company
* Here WeGo (formerly Here Maps), a mobile app and map website by Here Technologies, Here
Television
* Here TV (form ...
, the leftmost redex of the in-order traversal is while the leftmost-outermost redex is the entire expression.
''Applicative order reduction'' refers to leftmost-innermost reduction.
In contrast to normal order, applicative order reduction may not terminate, even when the term has a normal form. For example, using applicative order reduction, the following sequence of reductions is possible:
But using normal-order reduction, the same starting point reduces quickly to normal form:
''Full β-reduction'' refers to the nondeterministic one-step strategy that allows reducing any redex at each step. Takahashi's ''parallel β-reduction'' is the strategy that reduces all redexes in the term simultaneously.
Weak reduction
Normal and applicative order reduction are strong in that they allow reduction under lambda abstractions. In contrast, ''weak'' reduction does not reduce under a lambda abstraction. ''Call-by-name reduction'' is the weak reduction strategy that reduces the leftmost outermost redex not inside a lambda abstraction, while ''call-by-value reduction'' is the weak reduction strategy that reduces the leftmost innermost redex not inside a lambda abstraction. These strategies were devised to reflect the call-by-name and call-by-value evaluation strategies. In fact, applicative order reduction was also originally introduced to model the call-by-value parameter passing technique found in Algol 60 and modern programming languages. When combined with the idea of weak reduction, the resulting call-by-value reduction is indeed a faithful approximation.
Unfortunately, weak reduction is not confluent, and the traditional reduction equations of the lambda calculus are useless, because they suggest relationships that violate the weak evaluation regime. However, it is possible to extend the system to be confluent by allowing a restricted form of reduction under an abstraction, in particular when the redex does not involve the variable bound by the abstraction. For example, is in normal form for a weak reduction strategy because the redex is contained in a lambda abstraction. But the term can still be reduced under the extended weak reduction strategy, because the redex does not refer to .
Optimal reduction
Optimal reduction is motivated by the existence of lambda terms where there does not exist a sequence of reductions which reduces them without duplicating work. For example, consider
((λg.(g(g(λx.x))))
(λh.((λf.(f(f(λz.z))))
(λw.(h(w(λy.y)))))))
It is composed of three nested terms, , , and . There are only two possible β-reductions to be done here, on x and on y. Reducing the outer x term first results in the inner y term being duplicated, and each copy will have to be reduced, but reducing the inner y term first will duplicate its argument z, which will cause work to be duplicated when the values of h and w are made known.
Optimal reduction is not a reduction strategy for the lambda calculus in a narrow sense because performing β-reduction loses the information about the substituted redexes being shared. Instead it is defined for the ''labelled lambda calculus'', an annotated lambda calculus which captures a precise notion of the work that should be shared.
Labels consist of a countably infinite set of atomic labels, and concatenations , overlinings and underlinings of labels. A labelled term is a lambda calculus term where each subterm has a label. The standard initial labeling of a lambda term gives each subterm a unique atomic label. Labelled β-reduction is given by: