In computer science, confluence is a property of rewriting systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system.
The usual rules of elementary arithmetic form an abstract rewriting system. For example, the expression (11 + 9) × (2 + 4) can be evaluated starting either at the left or at the right parentheses; however, in both cases the same result is eventually obtained. If every arithmetic expression evaluates to the same result regardless of reduction strategy, the arithmetic rewriting system is said to be ground-confluent. Arithmetic rewriting systems may be confluent or only ground-confluent depending on details of the rewriting system. [1]
A second, more abstract example is obtained from the following proof of each group element equalling the inverse of its inverse: [2]
| A1 | 1 ⋅ a | = a |
| A2 | a−1 ⋅ a | = 1 |
| A3 | (a ⋅ b) ⋅ c | = a ⋅ (b ⋅ c) |
| a−1 ⋅ (a ⋅ b) | ||
| = | (a−1 ⋅ a) ⋅ b | by A3(r) |
| = | 1 ⋅ b | by A2 |
| = | b | by A1 |
| (a−1)−1 ⋅ 1 | ||
| = | (a−1)−1 ⋅ (a−1 ⋅ a) | by A2(r) |
| = | a | by R4 |
| (a−1)−1 ⋅ b | ||
| = | (a−1)−1 ⋅ (a−1 ⋅ (a ⋅ b)) | by R4(r) |
| = | a ⋅ b | by R4 |
| a ⋅ 1 | ||
| = | (a−1)−1 ⋅ 1 | by R10(r) |
| = | a | by R6 |
| (a−1)−1 | ||
| = | (a−1)−1 ⋅ 1 | by R11(r) |
| = | a | by R6 |
This proof starts from the given group axioms A1–A3, and establishes five propositions R4, R6, R10, R11, and R12, each of them using some earlier ones, and R12 being the main theorem. Some of the proofs require non-obvious, or even creative, steps, like applying axiom A2 in reverse, thereby rewriting "1" to "a−1 ⋅ a" in the first step of R6's proof. One of the historical motivations to develop the theory of term rewriting was to avoid the need for such steps, which are difficult to find by an inexperienced human, let alone by a computer program [ citation needed ].
If a term rewriting system is confluent and terminating , a straightforward method exists to prove equality between two expressions (also known as terms ) s and t: Starting with s, apply equalities [note 1] from left to right as long as possible, eventually obtaining a term s′. Obtain from t a term t′ in a similar way. If both terms s′ and t′ literally agree, then s and t are proven equal. More importantly, if they disagree, then s and t cannot be equal. That is, any two terms s and t that can be proven equal at all can be done so by that method.
The success of that method does not depend on a certain sophisticated order in which to apply rewrite rules, as confluence ensures that any sequence of rule applications will eventually lead to the same result (while the termination property ensures that any sequence will eventually reach an end at all). Therefore, if a confluent and terminating term rewriting system can be provided for some equational theory, [note 2] not a tinge of creativity is required to perform proofs of term equality; that task hence becomes amenable to computer programs. Modern approaches handle more general abstract rewriting systems rather than term rewriting systems; the latter are a special case of the former.
A rewriting system can be expressed as a directed graph in which nodes represent expressions and edges represent rewrites. So, for example, if the expression a can be rewritten into b, then we say that b is a reduct of a (alternatively, areduces tob, or a is an expansion of b). This is represented using arrow notation; a → b indicates that a reduces to b. Intuitively, this means that the corresponding graph has a directed edge from a to b.
If there is a path between two graph nodes c and d, then it forms a reduction sequence. So, for instance, if c → c′ → c′′ → ... → d′ → d, then we can write cd, indicating the existence of a reduction sequence from c to d. Formally, is the reflexive-transitive closure of →. Using the example from the previous paragraph, we have (11+9)×(2+4) → 20×(2+4) and 20×(2+4) → 20×6, so (11+9)×(2+4) 20×6.
With this established, confluence can be defined as follows. a ∈ S is deemed confluent if for all pairs b, c ∈ S such that ab and ac, there exists a d ∈ S with bd and cd (denoted ). If every a ∈ S is confluent, we say that → is confluent. This property is also sometimes called the diamond property, after the shape of the diagram shown on the right. Some authors reserve the term diamond property for a variant of the diagram with single reductions everywhere; that is, whenever a → b and a → c, there must exist a d such that b → d and c → d. The single-reduction variant is strictly stronger than the multi-reduction one.
A term rewriting system is ground confluent if every ground term is confluent, that is, every term without variables. [3]
An element a ∈ S is said to be locally confluent (or weakly confluent [5] ) if for all b, c ∈ S with a → b and a → c there exists d ∈ S with bd and cd. If every a ∈ S is locally confluent, then → is called locally confluent, or having the weak Church–Rosser property. This is different from confluence in that b and c must be reduced from a in one step. In analogy with this, confluence is sometimes referred to as global confluence.
The relation , introduced as a notation for reduction sequences, may be viewed as a rewriting system in its own right, whose relation is the reflexive-transitive closure of →. Since a sequence of reduction sequences is again a reduction sequence (or, equivalently, since forming the reflexive-transitive closure is idempotent), = . It follows that → is confluent if and only if is locally confluent.
A rewriting system may be locally confluent without being (globally) confluent. Examples are shown in picture 3 and 4. However, Newman's lemma states that if a locally confluent rewriting system has no infinite reduction sequences (in which case it is said to be terminating or strongly normalizing), then it is globally confluent.
A rewriting system is said to possess the Church–Rosser property if and only if implies for all objects x, y. Alonzo Church and J. Barkley Rosser proved in 1936 that lambda calculus has this property; [6] hence the name of the property. [7] (The fact that lambda calculus has this property is also known as the Church–Rosser theorem.) In a rewriting system with the Church–Rosser property the word problem may be reduced to the search for a common successor. In a Church–Rosser system, an object has at most one normal form; that is the normal form of an object is unique if it exists, but it may well not exist. In lambda calculus for instance, the expression (λx.xx)(λx.xx) does not have a normal form because there exists an infinite sequence of β-reductions (λx.xx)(λx.xx) → (λx.xx)(λx.xx) → ... [8]
A rewriting system possesses the Church–Rosser property if and only if it is confluent. [9] Because of this equivalence, a fair bit of variation in definitions is encountered in the literature. For instance, in "Terese" the Church–Rosser property and confluence are defined to be synonymous and identical to the definition of confluence presented here; Church–Rosser as defined here remains unnamed, but is given as an equivalent property; this departure from other texts is deliberate. [10]
The definition of local confluence differs from that of global confluence in that only elements reached from a given element in a single rewriting step are considered. By considering one element reached in a single step and another element reached by an arbitrary sequence, we arrive at the intermediate concept of semi-confluence: a ∈ S is said to be semi-confluent if for all b, c ∈ S with a → b and ac there exists d ∈ S with bd and cd; if every a ∈ S is semi-confluent, we say that → is semi-confluent.
A semi-confluent element need not be confluent, but a semi-confluent rewriting system is necessarily confluent, and a confluent system is trivially semi-confluent.
Strong confluence is another variation on local confluence that allows us to conclude that a rewriting system is globally confluent. An element a ∈ S is said to be strongly confluent if for all b, c ∈ S with a → b and a → c there exists d ∈ S with bd and either c → d or c = d; if every a ∈ S is strongly confluent, we say that → is strongly confluent.
A confluent element need not be strongly confluent, but a strongly confluent rewriting system is necessarily confluent.
Lambda 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 that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics.
Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely. The theory is computably axiomatizable; the axioms include a schema of induction.
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.
In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result.
Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.
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. In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.
In mathematics and computer science, a canonical, normal, or standardform of a mathematical object is a standard way of presenting that object as a mathematical expression. Often, it is one which provides the simplest representation of an object and allows it to be identified in a unique way. The distinction between "canonical" and "normal" forms varies from subfield to subfield. In most fields, a canonical form specifies a unique representation for every object, while a normal form simply specifies its form, without the requirement of uniqueness.
The Knuth–Bendix completion algorithm is a semi-decision algorithm for transforming a set of equations into a confluent term rewriting system. When the algorithm succeeds, it effectively solves the word problem for the specified algebra.
In computational mathematics, a word problem is the problem of deciding whether two given expressions are equivalent with respect to a set of rewriting identities. A prototypical example is the word problem for groups, but there are many other instances as well. A deep result of computational theory is that answering this question is in many important cases undecidable.
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms.
Orthogonality as a property of term rewriting systems (TRSs) describes where the reduction rules of the system are all left-linear, that is each variable occurs only once on the left hand side of each reduction rule, and there is no overlap between them, i.e. the TRS has no critical pairs. For example is not left-linear.
In mathematics, in the theory of rewriting systems, Newman's lemma, also commonly called the diamond lemma, states that a terminating abstract rewriting system (ARS), that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent. In fact a terminating ARS is confluent precisely when it is locally confluent.
In mathematical logic, the De Bruijn index is a tool invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms of lambda calculus without naming the bound variables. Terms written using these indices are invariant with respect to α-conversion, so the check for α-equivalence is the same as that for syntactic equality. Each De Bruijn index is a natural number that represents an occurrence of a variable in a λ-term, and denotes the number of binders that are in scope between that occurrence and its corresponding binder. The following are some examples:
In computer science, a computation is said to diverge if it does not terminate or terminates in an exceptional state. Otherwise it is said to converge. In domains where computations are expected to be infinite, such as process calculi, a computation is said to diverge if it fails to be productive.
In mathematical logic and theoretical computer science, an abstract rewriting system is a formalism that captures the quintessential notion and properties of rewriting systems. In its simplest form, an ARS is simply a set together with a binary relation, traditionally denoted with ; this definition can be further refined if we index (label) subsets of the binary relation. Despite its simplicity, an ARS is sufficient to describe important properties of rewriting systems like normal forms, termination, and various notions of confluence.
In the study of denotational semantics of the lambda calculus, Böhm trees, Lévy-Longo trees, and Berarducci trees are tree-like mathematical objects that capture the "meaning" of a term up to some set of "meaningless" terms.
Jan Willem Klop is a professor of applied logic at Vrije Universiteit in Amsterdam. He holds a Ph.D. in mathematical logic from Utrecht University. Klop is known for his work on the algebra of communicating processes, co-author of TeReSe and his fixed point combinator
A critical pair arises in a term rewriting system when two rewrite rules overlap to yield two different terms. In more detail, (t1, t2) is a critical pair if there is a term t for which two different applications of a rewrite rule (either the same rule applied differently, or two different rules) yield the terms t1 and t2.
In rewriting, 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.
| Authority control databases: National |
|---|
