In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions, each of the form Left-hand side = Right-hand side. For example, using x,y,z as variables, the singleton equation set { cons(x,cons(x,nil)) = cons(2,y) } is a syntactic first-order unification problem that has the substitution { x ↦ 2, y ↦ cons(2,nil) } as its only solution.
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.
In mathematics, a binary relation R is called well-founded on a set or, more generally, a class X if every non-empty subset S ⊆ X has a minimal element with respect to R; that is, there exists an m ∈ S such that, for every s ∈ S, one does not have sRm. In other words, a relation is well founded if:
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, the axiom of dependent choice, denoted by , is a weak form of the axiom of choice that is still sufficient to develop much of real analysis. It was introduced by Paul Bernays in a 1942 article that explores which set-theoretic axioms are needed to develop analysis.
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.
Pregeometry, and in full combinatorial pregeometry, are essentially synonyms for "matroid". They were introduced by Gian-Carlo Rota with the intention of providing a less "ineffably cacophonous" alternative term. Also, the term combinatorial geometry, sometimes abbreviated to geometry, was intended to replace "simple matroid". These terms are now infrequently used in the study of matroids.
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.
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.
In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for each input. This means to determine whether the input program computes a total function.
In the mathematical subject of group theory, small cancellation theory studies groups given by group presentations satisfying small cancellation conditions, that is where defining relations have "small overlaps" with each other. Small cancellation conditions imply algebraic, geometric and algorithmic properties of the group. Finitely presented groups satisfying sufficiently strong small cancellation conditions are word hyperbolic and have word problem solvable by Dehn's algorithm. Small cancellation methods are also used for constructing Tarski monsters, and for solutions of Burnside's problem.
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 mathematics, the reflexive closure of a binary relation on a set is the smallest reflexive relation on that contains A relation is called reflexive if it relates every element of to itself.
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 mathematics, computer science and logic, convergence is the idea that different sequences of transformations come to a conclusion in a finite amount of time, and that the conclusion reached is independent of the path taken to get to it.
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 graph theory, a skew partition of a graph is a partition of its vertices into two subsets, such that the induced subgraph formed by one of the two subsets is disconnected and the induced subgraph formed by the other subset is the complement of a disconnected graph. Skew partitions play an important role in the theory of perfect graphs.
In theoretical computer science, in particular in automated reasoning about formal equations, reduction orderings are used to prevent endless loops. Rewrite orders, and, in turn, rewrite relations, are generalizations of this concept that have turned out to be useful in theoretical investigations.
Tobias Nipkow is a German computer scientist.
