most general unifier
   HOME

TheInfoList



OR:

In
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from prem ...
and
computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, unification is an algorithmic process of solving equations between symbolic expressions. Depending on which expressions (also called ''terms'') are allowed to occur in an equation set (also called ''unification problem''), and which expressions are considered equal, several frameworks of unification are distinguished. If higher-order variables, that is, variables representing
function Function or functionality may refer to: Computing * Function key, a type of key on computer keyboards * Function model, a structured representation of processes in a system * Function object or functor or functionoid, a concept of object-oriente ...
s, are allowed in an expression, the process is called higher-order unification, otherwise first-order unification. If a solution is required to make both sides of each equation literally equal, the process is called syntactic or free unification, otherwise semantic or equational unification, or E-unification, or unification modulo theory. A ''solution'' of a unification problem is denoted as a
substitution Substitution may refer to: Arts and media *Chord substitution, in music, swapping one chord for a related one within a chord progression *Substitution (poetry), a variation in poetic scansion * "Substitution" (song), a 2009 song by Silversun Pic ...
, that is, a mapping assigning a symbolic value to each variable of the problem's expressions. A unification algorithm should compute for a given problem a ''complete'' and ''minimal'' substitution set, i.e., a set containing all of the problem's solutions and no redundant members. Depending on the framework, a complete and minimal substitution set may have at most one, at most finitely many, or possibly infinitely many members, or may not exist at all.in this case, still a complete substitution set exists (e.g. the set of all solutions at all); however, each such set contains redundant members. In some frameworks it is generally impossible to decide whether any solution exists. For first-order syntactical unification, Martelli and Montanari gave an algorithm that reports unsolvability or computes a complete and minimal singleton substitution set containing the so-called most general unifier. For example, using ''x'',''y'',''z'' as variables, the singleton equation set is a syntactic first-order unification problem that has the substitution as its only solution. The syntactic first-order unification problem has no solution over the set of
finite terms In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a wh ...
; however, it has the single solution over the set of infinite trees. The semantic first-order unification problem has each substitution of the form as a solution in a
semigroup In mathematics, a semigroup is an algebraic structure consisting of a set together with an associative internal binary operation on it. The binary operation of a semigroup is most often denoted multiplicatively: ''x''·''y'', or simply ''xy'', ...
, i.e. if (⋅) is considered
associative In mathematics, the associative property is a property of some binary operations, which means that rearranging the parentheses in an expression will not change the result. In propositional logic, associativity is a valid rule of replacement ...
; the same problem, viewed in an
abelian group In mathematics, an abelian group, also called a commutative group, is a group in which the result of applying the group operation to two group elements does not depend on the order in which they are written. That is, the group operation is comm ...
, where (⋅) is considered also
commutative In mathematics, a binary operation is commutative if changing the order of the operands does not change the result. It is a fundamental property of many binary operations, and many mathematical proofs depend on it. Most familiar as the name of ...
, has any substitution at all as a solution. The singleton set is a syntactic second-order unification problem, since ''y'' is a function variable. One solution is ; another one is . A unification algorithm was first discovered by
Jacques Herbrand Jacques Herbrand (12 February 1908 – 27 July 1931) was a French mathematician. Although he died at age 23, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse and Richard Coura ...
, while a first formal investigation can be attributed to
John Alan Robinson John Alan Robinson (9 March 1930 – 5 August 2016) was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University. Alan Robinson's major contribution is to the foundations of automated theorem pr ...
,; Here: sect.5.8, p.32 who used first-order syntactical unification as a basic building block of his resolution procedure for first-order logic, a great step forward in
automated reasoning In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer prog ...
technology, as it eliminated one source of combinatorial explosion: searching for instantiation of terms. Today, automated reasoning is still the main application area of unification. Syntactical first-order unification is used in
logic programming Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic pro ...
and programming language
type system In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progra ...
implementation, especially in Hindley–Milner based
type inference Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistic ...
algorithms. Semantic unification is used in
SMT solver In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvi ...
s,
term rewriting 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 r ...
algorithms and
cryptographic protocol A security protocol (cryptographic protocol or encryption protocol) is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol descri ...
analysis. Higher-order unification is used in proof assistants, for example
Isabelle Isabel is a female name of Spanish origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of ''Elizabeth (given name), Elisabeth'' (ultimately Hebrew ''Elisheba, Elisheva''), Arising in ...
and
Twelf Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory. Introduction At i ...
, and restricted forms of higher-order unification (higher-order pattern unification) are used in some programming language implementations, such as lambdaProlog, as higher-order patterns are expressive, yet their associated unification procedure retains theoretical properties closer to first-order unification.


Formal definition


Prerequisites

Formally, a unification approach presupposes * An infinite set V of variables. For higher-order unification, it is convenient to choose V disjoint from the set of
lambda-term bound variables 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 tha ...
. * A set T of terms such that V \subseteq T. For first-order unification, T is usually the set of first-order terms (terms built from variable and function symbols). For higher-order unification T consists of first-order terms and
lambda terms 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 th ...
(terms containing some higher-order variables). * A mapping ''vars'': T \rightarrow \mathbb(V), assigning to each term t the set \text(t) \subsetneq V of free variables occurring in t. * An
equivalence relation In mathematics, an equivalence relation is a binary relation that is reflexive, symmetric and transitive. The equipollence relation between line segments in geometry is a common example of an equivalence relation. Each equivalence relatio ...
\equiv on T, indicating which terms are considered equal. For first-order E-unification, \equiv reflects the background knowledge about certain function symbols; for example, if \oplus is considered commutative, t\equiv u if u results from t by swapping the arguments of \oplus at some (possibly all) occurrences. E.g. ''a'' ⊕ (''b'' ⊕ ''f''(''x'')) ≡ ''a'' ⊕ (''f''(''x'') ⊕ ''b'') ≡ (''b'' ⊕ ''f''(''x'')) ⊕ ''a'' ≡ (''f''(''x'') ⊕ ''b'') ⊕ ''a'' In the most typical case that there is no background knowledge at all, then only literally, or syntactically, identical terms are considered equal. In this case, ≡ is called the
free theory Free may refer to: Concept * Freedom, having the ability to do something, without having to obey anyone/anything * Freethought, a position that beliefs should be formed only on the basis of logic, reason, and empiricism * Emancipate, to procure ...
(because it is a
free object In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. Informally, a free object over a set ''A'' can be thought of as being a "generic" algebraic structure over ''A'': the only equations that hold between eleme ...
), the empty theory (because the set of equational
sentences ''The Four Books of Sentences'' (''Libri Quattuor Sententiarum'') is a book of theology written by Peter Lombard in the 12th century. It is a systematic compilation of theology, written around 1150; it derives its name from the '' sententiae'' ...
, or the background knowledge, is empty), the theory of
uninterpreted function In mathematical logic, an uninterpreted function or function symbol is one that has no other property than its name and ''n-ary'' form. Function symbols are used, together with constants and variables, to form terms. The theory of uninterpreted fu ...
s (because unification is done on uninterpreted terms), or the theory of constructors (because all function symbols just build up data terms, rather than operating on them). For higher-order unification, usually t\equiv u if t and u are alpha equivalent.


Substitution

A substitution is a mapping \sigma: V\rightarrow T from variables to terms; the notation \ refers to a substitution mapping each variable x_i to the term t_i, for i=1,...,k, and every other variable to itself. Applying that substitution to a term t is written in
postfix notation Reverse Polish notation (RPN), also known as reverse Łukasiewicz notation, Polish postfix notation or simply postfix notation, is a mathematical notation in which operators ''follow'' their operands, in contrast to Polish notation (PN), in w ...
as t \; it means to (simultaneously) replace every occurrence of each variable x_i in the term t by t_i. The result t\tau of applying a substitution \tau to a term t is called an instance of that term t. As a first-order example, applying the substitution to the term


Generalization, specialization

If a term t has an instance equivalent to a term u, that is, if t\sigma \equiv u for some substitution \sigma, then t is called more general than u, and u is called more special than, or subsumed by, t. For example, x\oplus a is more general than a\oplus b if ⊕ is
commutative In mathematics, a binary operation is commutative if changing the order of the operands does not change the result. It is a fundamental property of many binary operations, and many mathematical proofs depend on it. Most familiar as the name of ...
, since then (x\oplus a) \ = b\oplus a\equiv a\oplus b. If ≡ is literal (syntactic) identity of terms, a term may be both more general and more special than another one only if both terms differ just in their variable names, not in their syntactic structure; such terms are called variants, or renamings of each other. For example, f(x_1, a, g(z_1), y_1) is a variant of f(x_2, a, g(z_2), y_2), since
f(x_1, a, g(z_1), y_1) \ = f(x_2, a, g(z_2), y_2)
and
f(x_2, a, g(z_2), y_2) \ = f(x_1, a, g(z_1), y_1).
However, f(x_1, a, g(z_1), y_1) is ''not'' a variant of f(x_2, a, g(x_2), x_2), since no substitution can transform the latter term into the former one. The latter term is therefore properly more special than the former one. For arbitrary \equiv, a term may be both more general and more special than a structurally different term. For example, if ⊕ is
idempotent Idempotence (, ) is the property of certain operations in mathematics and computer science whereby they can be applied multiple times without changing the result beyond the initial application. The concept of idempotence arises in a number of pl ...
, that is, if always x \oplus x \equiv x, then the term x\oplus y is more general than z,since (x\oplus y) \ = z\oplus z \equiv z and vice versa,since although x\oplus y and z are of different structure. A substitution \sigma is more special than, or subsumed by, a substitution \tau if t\sigma is more special than t\tau for each term t. We also say that \tau is more general than \sigma. For instance \ is more special than \tau = \, but \sigma = \ is not, as f(x, y)\sigma = f(a, y) is not more special than f(x, y) \tau = f(y, y).


Unification problem, solution set

A unification problem is a finite set of potential equations, where . A substitution σ is a solution of that problem if for i = 1, ..., n. Such a substitution is also called a unifier of the unification problem. For example, if ⊕ is
associative In mathematics, the associative property is a property of some binary operations, which means that rearranging the parentheses in an expression will not change the result. In propositional logic, associativity is a valid rule of replacement ...
, the unification problem has the solutions , , , etc., while the problem has no solution. For a given unification problem, a set ''S'' of unifiers is called complete if each solution substitution is subsumed by some substitution σ ∈ ''S''; the set ''S'' is called minimal if none of its members subsumes another one.


Syntactic unification of first-order terms

''Syntactic unification of first-order terms'' is the most widely used unification framework. It is based on ''T'' being the set of ''first-order terms'' (over some given set ''V'' of variables, ''C'' of constants and ''F''''n'' of ''n''-ary function symbols) and on ≡ being ''syntactic equality''. In this framework, each solvable unification problem has a complete, and obviously minimal,
singleton Singleton may refer to: Sciences, technology Mathematics * Singleton (mathematics), a set with exactly one element * Singleton field, used in conformal field theory Computing * Singleton pattern, a design pattern that allows only one instance ...
solution set . Its member is called the most general unifier (mgu) of the problem. The terms on the left and the right hand side of each potential equation become syntactically equal when the mgu is applied i.e. . Any unifier of the problem is subsumedformally: each unifier τ satisfies for some substitution ρ by the mgu . The mgu is unique up to variants: if ''S''1 and ''S''2 are both complete and minimal solution sets of the same syntactical unification problem, then ''S''1 = and ''S''2 = for some substitutions and and is a variant of for each variable ''x'' occurring in the problem. For example, the unification problem has a unifier , because : This is also the most general unifier. Other unifiers for the same problem are e.g. , , and so on; there are infinitely many similar unifiers. As another example, the problem ''g''(''x'',''x'') ≐ ''f''(''y'') has no solution with respect to ≡ being literal identity, since any substitution applied to the left and right hand side will keep the outermost ''g'' and ''f'', respectively, and terms with different outermost function symbols are syntactically different.


A unification algorithm

The first algorithm given by Robinson (1965) was rather inefficient; cf. box. The following faster algorithm originated from Martelli, Montanari (1982).Alg.1, p.261. Their rule (a) corresponds to rule swap here, (b) to delete, (c) to both decompose and conflict, and (d) to both eliminate and check. This paper also lists preceding attempts to find an efficient syntactical unification algorithm, and states that linear-time algorithms were discovered independently by Martelli, Montanari (1976) and Paterson, Wegman (1976, 1978). Given a finite set G = \ of potential equations, the algorithm applies rules to transform it to an equivalent set of equations of the form where ''x''1, ..., ''x''''m'' are distinct variables and ''u''1, ..., ''u''''m'' are terms containing none of the ''x''''i''. A set of this form can be read as a substitution. If there is no solution the algorithm terminates with ⊥; other authors use "Ω", "", or "''fail''" in that case. The operation of substituting all occurrences of variable ''x'' in problem ''G'' with term ''t'' is denoted ''G'' . For simplicity, constant symbols are regarded as function symbols having zero arguments. :


Occurs check

An attempt to unify a variable ''x'' with a term containing ''x'' as a strict subterm ''x'' ≐ ''f''(..., ''x'', ...) would lead to an infinite term as solution for ''x'', since ''x'' would occur as a subterm of itself. In the set of (finite) first-order terms as defined above, the equation ''x'' ≐ ''f''(..., ''x'', ...) has no solution; hence the ''eliminate'' rule may only be applied if ''x'' ∉ ''vars''(''t''). Since that additional check, called ''occurs check'', slows down the algorithm, it is omitted e.g. in most Prolog systems. From a theoretical point of view, omitting the check amounts to solving equations over infinite trees, see #Unification of infinite terms below.


Proof of termination

For the proof of termination of the algorithm consider a triple \langle n_, n_, n_\rangle where is the number of variables that occur more than once in the equation set, is the number of function symbols and constants on the left hand sides of potential equations, and is the number of equations. When rule ''eliminate'' is applied, decreases, since ''x'' is eliminated from ''G'' and kept only in . Applying any other rule can never increase again. When rule ''decompose'', ''conflict'', or ''swap'' is applied, decreases, since at least the left hand side's outermost ''f'' disappears. Applying any of the remaining rules ''delete'' or ''check'' can't increase , but decreases . Hence, any rule application decreases the triple \langle n_, n_, n_\rangle with respect to the
lexicographical order In mathematics, the lexicographic or lexicographical order (also known as lexical order, or dictionary order) is a generalization of the alphabetical order of the dictionaries to sequences of ordered symbols or, more generally, of elements of ...
, which is possible only a finite number of times.
Conor McBride Conor McBride (born 18 February 1973) is a Reader in the department of Computer and Information Sciences at the University of Strathclyde. In 1999, he completed a Doctor of Philosophy (Ph.D.) in ''Dependently Typed Functional Programs and thei ...
observes that "by expressing the structure which unification exploits" in a dependently typed language such as
Epigram An epigram is a brief, interesting, memorable, and sometimes surprising or satirical statement. The word is derived from the Greek "inscription" from "to write on, to inscribe", and the literary device has been employed for over two mill ...
, Robinson's unification algorithm can be made recursive on the number of variables, in which case a separate termination proof becomes unnecessary.


Examples of syntactic unification of first-order terms

In the Prolog syntactical convention a symbol starting with an upper case letter is a variable name; a symbol that starts with a lowercase letter is a function symbol; the comma is used as the logical ''and'' operator. For mathematical notation, ''x,y,z'' are used as variables, ''f,g'' as function symbols, and ''a,b'' as constants. The most general unifier of a syntactic first-order unification problem of
size Size in general is the magnitude or dimensions of a thing. More specifically, ''geometrical size'' (or ''spatial size'') can refer to linear dimensions ( length, width, height, diameter, perimeter), area, or volume. Size can also be me ...
may have a size of . For example, the problem has the most general unifier , cf. picture. In order to avoid exponential time complexity caused by such blow-up, advanced unification algorithms work on
directed acyclic graph In mathematics, particularly graph theory, and computer science, a directed acyclic graph (DAG) is a directed graph with no directed cycles. That is, it consists of vertices and edges (also called ''arcs''), with each edge directed from one ...
s (dags) rather than trees.


Application: unification in logic programming

The concept of unification is one of the main ideas behind
logic programming Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic pro ...
, best known through the language
Prolog Prolog is a logic programming language associated with artificial intelligence and computational linguistics. Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...
. It represents the mechanism of binding the contents of variables and can be viewed as a kind of one-time assignment. In Prolog, this operation is denoted by the equality symbol =, but is also done when instantiating variables (see below). It is also used in other languages by the use of the equality symbol =, but also in conjunction with many operations including +, -, *, /.
Type inference Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistic ...
algorithms are typically based on unification. In Prolog: # A variable which is uninstantiated—i.e. no previous unifications were performed on it—can be unified with an atom, a term, or another uninstantiated variable, thus effectively becoming its alias. In many modern Prolog dialects and in
first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
, a variable cannot be unified with a term that contains it; this is the so-called '' occurs check''. # Two atoms can only be unified if they are identical. # Similarly, a term can be unified with another term if the top function symbols and arities of the terms are identical and if the parameters can be unified simultaneously. Note that this is a recursive behavior.


Application: type inference

Unification is used during type inference, for instance in the functional programming language
Haskell Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lan ...
. On one hand, the programmer does not need to provide type information for every function, on the other hand it is used to detect typing errors. The Haskell expression True : x', 'y', 'z'/code> is not correctly typed. The list construction function (:) is of type a -> -> /code>, and for the first argument True the polymorphic type variable a has to be unified with True's type, Bool. The second argument, x', 'y', 'z'/code>, is of type har/code>, but a cannot be both Bool and Char at the same time. Like for Prolog, an algorithm for type inference can be given: # Any type variable unifies with any type expression, and is instantiated to that expression. A specific theory might restrict this rule with an occurs check. # Two type constants unify only if they are the same type. # Two type constructions unify only if they are applications of the same type constructor and all of their component types recursively unify. Due to its declarative nature, the order in a sequence of unifications is (usually) unimportant. Note that in the terminology of
first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
, an atom is a basic proposition and is unified similarly to a Prolog term.


Application: Feature Structure Unification

See
Feature_structure In phrase structure grammars, such as generalised phrase structure grammar, head-driven phrase structure grammar and lexical functional grammar, a feature structure is essentially a set of attribute–value pairs. For example, the attribute name ...
. Unification has been used in different research areas of computational linguistics.


Order-sorted unification

''
Order-sorted logic Many-sorted logic can reflect formally our intention not to handle the universe as a homogeneous collection of objects, but to partition it in a way that is similar to types in typeful programming. Both functional and assertive "parts of speech" ...
'' allows one to assign a ''sort'', or ''type'', to each term, and to declare a sort ''s''1 a ''subsort'' of another sort ''s''2, commonly written as ''s''1 ⊆ ''s''2. For example, when reаsoning about biological creatures, it is useful to declare a sort ''dog'' to be a subsort of a sort ''animal''. Wherever a term of some sort ''s'' is required, a term of any subsort of ''s'' may be supplied instead. For example, assuming a function declaration ''mother'': ''animal'' → ''animal'', and a constant declaration ''lassie'': ''dog'', the term ''mother''(''lassie'') is perfectly valid and has the sort ''animal''. In order to supply the information that the mother of a dog is a dog in turn, another declaration ''mother'': ''dog'' → ''dog'' may be issued; this is called ''function overloading'', similar to overloading in programming languages.
Walther Walther is a masculine given name and a surname. It is a German form of Walter, which is derived from the Old High German ''Walthari'', containing the elements ''wald'' -"power", "brightness" or "forest" and ''hari'' -"warrior". The name was fi ...
gave a unification algorithm for terms in order-sorted logic, requiring for any two declared sorts ''s''1, ''s''2 their intersection ''s''1 ∩ ''s''2 to be declared, too: if ''x''1 and ''x''2 is a variable of sort ''s''1 and ''s''2, respectively, the equation ''x''1 ≐ ''x''2 has the solution , where ''x'': ''s''1 ∩ ''s''2. After incorporating this algorithm into a clause-based automated theorem prover, he could solve a benchmark problem by translating it into order-sorted logic, thereby boiling it down an order of magnitude, as many unary predicates turned into sorts. Smolka generalized order-sorted logic to allow for
parametric polymorphism In programming languages and type theory, parametric polymorphism allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed. Parametrically polymorph ...
. In his framework, subsort declarations are propagated to complex type expressions. As a programming example, a parametric sort ''list''(''X'') may be declared (with ''X'' being a type parameter as in a
C++ template Templates are a feature of the C++ programming language that allows functions and classes to operate with generic types. This allows a function or class to work on many different data types without being rewritten for each one. The C++ Standa ...
), and from a subsort declaration ''int'' ⊆ ''float'' the relation ''list''(''int'') ⊆ ''list''(''float'') is automatically inferred, meaning that each list of integers is also a list of floats. Schmidt-Schauß generalized order-sorted logic to allow for term declarations. As an example, assuming subsort declarations ''even'' ⊆ ''int'' and ''odd'' ⊆ ''int'', a term declaration like ∀ ''i'' : ''int''. (''i'' + ''i'') : ''even'' allows to declare a property of integer addition that could not be expressed by ordinary overloading.


Unification of infinite terms

Background on infinite trees: * * * Unification algorithm, Prolog II: * * Applications: *


E-unification

E-unification is the problem of finding solutions to a given set of
equations In mathematics, an equation is a formula that expresses the equality of two expressions, by connecting them with the equals sign . The word ''equation'' and its cognates in other languages may have subtly different meanings; for example, in ...
, taking into account some equational background knowledge ''E''. The latter is given as a set of universal equalities. For some particular sets ''E'', equation solving
algorithms In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
(a.k.a. ''E-unification algorithms'') have been devised; for others it has been proven that no such algorithms can exist. For example, if and are distinct constants, the
equation In mathematics, an equation is a formula that expresses the equality of two expressions, by connecting them with the equals sign . The word ''equation'' and its cognates in other languages may have subtly different meanings; for example, in F ...
has no solution with respect to purely syntactic unification, where nothing is known about the operator . However, if the is known to be
commutative In mathematics, a binary operation is commutative if changing the order of the operands does not change the result. It is a fundamental property of many binary operations, and many mathematical proofs depend on it. Most familiar as the name of ...
, then the substitution solves the above equation, since : The background knowledge ''E'' could state the commutativity of by the universal equality " for all ".


Particular background knowledge sets E

It is said that ''unification is decidable'' for a theory, if a unification algorithm has been devised for it that terminates for ''any'' input problem. It is said that ''unification is semi-decidable'' for a theory, if a unification algorithm has been devised for it that terminates for any ''solvable'' input problem, but may keep searching forever for solutions of an unsolvable input problem. Unification is decidable for the following theories: * * , * ,,F. Fages, ''Associative-Commutative Unification'', J. Symbolic Comput., vol.3, no.3, pp. 257–275, 1987 * ,,in the presence of equality , equalities and are equivalent, similar for and * , * , (monoid) * *
Boolean ring In mathematics, a Boolean ring ''R'' is a ring for which ''x''2 = ''x'' for all ''x'' in ''R'', that is, a ring that consists only of idempotent elements. An example is the ring of integers modulo 2. Every Boolean ring gives rise to a Boolean al ...
s *
Abelian group In mathematics, an abelian group, also called a commutative group, is a group in which the result of applying the group operation to two group elements does not depend on the order in which they are written. That is, the group operation is comm ...
s, even if the signature is expanded by arbitrary additional symbols (but not axioms)Baader and Snyder (2001), p. 486. * K4 modal algebras Unification is semi-decidable for the following theories: * , * ,, *
Commutative ring In mathematics, a commutative ring is a ring in which the multiplication operation is commutative. The study of commutative rings is called commutative algebra. Complementarily, noncommutative algebra is the study of ring properties that are not ...
s


One-sided paramodulation

If there is a convergent term rewriting system ''R'' available for ''E'', the one-sided paramodulation algorithm can be used to enumerate all solutions of given equations. Starting with ''G'' being the unification problem to be solved and ''S'' being the identity substitution, rules are applied nondeterministically until the empty set appears as the actual ''G'', in which case the actual ''S'' is a unifying substitution. Depending on the order the paramodulation rules are applied, on the choice of the actual equation from ''G'', and on the choice of ''R''s rules in ''mutate'', different computations paths are possible. Only some lead to a solution, while others end at a ''G'' ≠ where no further rule is applicable (e.g. ''G'' = ). For an example, a term rewrite system ''R'' is used defining the ''append'' operator of lists built from ''cons'' and ''nil''; where ''cons''(''x'',''y'') is written in infix notation as ''x''.''y'' for brevity; e.g. ''app''(''a''.''b''.''nil'',''c''.''d''.''nil'') → ''a''.''app''(''b''.''nil'',''c''.''d''.''nil'') → ''a''.''b''.''app''(''nil'',''c''.''d''.''nil'') → ''a''.''b''.''c''.''d''.''nil'' demonstrates the concatenation of the lists ''a''.''b''.''nil'' and ''c''.''d''.''nil'', employing the rewrite rule 2,2, and 1. The equational theory ''E'' corresponding to ''R'' is the
congruence closure In mathematics, a subset of a given set is closed under an operation of the larger set if performing that operation on members of the subset always produces a member of that subset. For example, the natural numbers are closed under addition, but ...
of ''R'', both viewed as binary relations on terms. For example, ''app''(''a''.''b''.''nil'',''c''.''d''.''nil'') ≡ ''a''.''b''.''c''.''d''.''nil'' ≡ ''app''(''a''.''b''.''c''.''d''.''nil'',''nil''). The paramodulation algorithm enumerates solutions to equations with respect to that ''E'' when fed with the example ''R''. A successful example computation path for the unification problem is shown below. To avoid variable name clashes, rewrite rules are consistently renamed each time before their use by rule ''mutate''; ''v''2, ''v''3, ... are computer-generated variable names for this purpose. In each line, the chosen equation from ''G'' is highlighted in red. Each time the ''mutate'' rule is applied, the chosen rewrite rule (''1'' or ''2'') is indicated in parentheses. From the last line, the unifying substitution ''S'' = can be obtained. In fact, ''app''(''x'',''app''(''y'',''x'')) = ''app''(''a''.''nil'',''app''(''nil'',''a''.''nil'')) ≡ ''app''(''a''.''nil'',''a''.''nil'') ≡ ''a''.''app''(''nil'',''a''.''nil'') ≡ ''a''.''a''.''nil'' solves the given problem. A second successful computation path, obtainable by choosing "mutate(1), mutate(2), mutate(2), mutate(1)" leads to the substitution ''S'' = ; it is not shown here. No other path leads to a success.


Narrowing

If ''R'' is a convergent term rewriting system for ''E'', an approach alternative to the previous section consists in successive application of "narrowing steps"; this will eventually enumerate all solutions of a given equation. A narrowing step (cf. picture) consists in * choosing a nonvariable subterm of the current term, * syntactically unifying it with the left hand side of a rule from ''R'', and * replacing the instantiated rule's right hand side into the instantiated term. Formally, if is a renamed copy of a rewrite rule from ''R'', having no variables in common with a term ''s'', and the subterm is not a variable and is unifiable with via the mgu , then can be narrowed to the term , i.e. to the term , with the subterm at ''p'' replaced by . The situation that ''s'' can be narrowed to ''t'' is commonly denoted as ''s'' ↝ ''t''. Intuitively, a sequence of narrowing steps ''t''1 ↝ ''t''2 ↝ ... ↝ ''t''''n'' can be thought of as a sequence of rewrite steps ''t''1 → ''t''2 → ... → ''t''''n'', but with the initial term ''t''1 being further and further instantiated, as necessary to make each of the used rules applicable. The above example paramodulation computation corresponds to the following narrowing sequence ("↓" indicating instantiation here): The last term, ''v''2.''v''2.''nil'' can be syntactically unified with the original right hand side term ''a''.''a''.''nil''. The ''narrowing lemma'' ensures that whenever an instance of a term ''s'' can be rewritten to a term ''t'' by a convergent term rewriting system, then ''s'' and ''t'' can be narrowed and rewritten to a term and , respectively, such that is an instance of . Formally: whenever holds for some substitution σ, then there exist terms such that and and for some substitution τ.


Higher-order unification

Many applications require one to consider the unification of typed lambda-terms instead of first-order terms. Such unification is often called ''higher-order unification''. Higher-order unification is undecidable, and such unification problems do not have most general unifiers. For example, the unification problem , where the only variable is ''f'', has the solutions , , , , and . A well studied branch of higher-order unification is the problem of unifying simply typed lambda terms modulo the equality determined by αβη conversions. Gérard Huet gave a semi-decidable (pre-)unification algorithm that allows a systematic search of the space of unifiers (generalizing the unification algorithm of Martelli-Montanari with rules for terms containing higher-order variables) that seems to work sufficiently well in practice. Huet and Gilles Dowek have written articles surveying this topic. Several subsets of higher-order unification are well-behaved, in that they are decidable and have a most-general unifier for solvable problems. One such subset is the previously described first-order terms. Higher-order pattern unification, due to Dale Miller, is another such subset. The higher-order logic programming languages
λProlog λProlog, also written lambda Prolog, is a logic programming language featuring polymorphic typing, modular programming, and higher-order programming. These extensions to Prolog are derived from the higher-order hereditary Harrop formulas u ...
and
Twelf Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory. Introduction At i ...
have switched from full higher-order unification to implementing only the pattern fragment; surprisingly pattern unification is sufficient for almost all programs, if each non-pattern unification problem is suspended until a subsequent substitution puts the unification into the pattern fragment. A superset of pattern unification called functions-as-constructors unification is also well-behaved. The Zipperposition theorem prover has an algorithm integrating these well-behaved subsets into a full higher-order unification algorithm. In computational linguistics, one of the most influential theories of elliptical construction is that ellipses are represented by free variables whose values are then determined using Higher-Order Unification (HOU). For instance, the semantic representation of "Jon likes Mary and Peter does too" is and the value of R (the semantic representation of the ellipsis) is determined by the equation . The process of solving such equations is called Higher-Order Unification.
Wayne Snyder Wayne Snyder is an associate professor at Boston University known for his work in E-unification theory. He was raised in Yardley, Pennsylvania, worked in his father's aircraft shop, attended the Berklee School of Music, and obtained an MA in A ...
gave a generalization of both higher-order unification and E-unification, i.e. an algorithm to unify lambda-terms modulo an equational theory.


See also

*
Rewriting 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 reduc ...
* Admissible rule *
Explicit substitution In computer science, lambda calculus, lambda calculi are said to have explicit substitutions if they pay special attention to the formalization of the process of substitution of variables, substitution. This is in contrast to the standard lambda cal ...
in
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 th ...
*Mathematical
equation solving In mathematics, to solve an equation is to find its solutions, which are the values (numbers, functions, sets, etc.) that fulfill the condition stated by the equation, consisting generally of two expressions related by an equals sign. When s ...
* Dis-unification: solving inequations between symbolic expression * Anti-unification: computing a least general generalization (lgg) of two terms, dual to computing a most general instance (mgu) *
Subsumption lattice A subsumption lattice is a mathematical structure used in the theoretical background of automated theorem proving and other symbolic computation applications. Definition A Term (logic), term ''t''1 is said to ''subsume'' a term ''t''2 if a Substi ...
, a lattice having unification as meet and anti-unification as join *
Ontology alignment Ontology alignment, or ontology matching, is the process of determining correspondences between concepts in ontologies. A set of correspondences is also called an alignment. The phrase takes on a slightly different meaning, in computer science, ...
(use ''unification'' with
semantic equivalence {{about, semantic equivalence of metadata, the concept in mathematical logic, Logical equivalence In computer metadata, semantic equivalence is a declaration that two data elements from different vocabularies contain data that has similar meaning. ...
)


Notes


References


Further reading

*
Franz Baader Franz Baader (15 June 1959, Spalt) is a German computer scientist at Dresden University of Technology. He received his PhD in Computer Science in 1989 from the University of Erlangen-Nuremberg, Germany, where he was a teaching and research assis ...
and
Wayne Snyder Wayne Snyder is an associate professor at Boston University known for his work in E-unification theory. He was raised in Yardley, Pennsylvania, worked in his father's aircraft shop, attended the Berklee School of Music, and obtained an MA in A ...
(2001)
"Unification Theory"
. In
John Alan Robinson John Alan Robinson (9 March 1930 – 5 August 2016) was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University. Alan Robinson's major contribution is to the foundations of automated theorem pr ...
and
Andrei Voronkov Andrei Anatolievič Voronkov (born 1959) is a Professor of Formal methods in the Department of Computer Science, University of Manchester, Department of Computer Science at the University of Manchester. Education Voronkov was educated at Novosibir ...
, editors, ''
Handbook of Automated Reasoning The ''Handbook of Automated Reasoning'' (, 2128 pages) is a collection of survey articles on the field of automated reasoning. Published in June 2001 by MIT Press, it is edited by John Alan Robinson and Andrei Voronkov. Volume 1 describes method ...
'', volume I, pages 447–533. Elsevier Science Publishers. * Gilles Dowek (2001)
"Higher-order Unification and Matching"
In ''Handbook of Automated Reasoning''. * Franz Baader and
Tobias Nipkow Tobias Nipkow (born 1958) is a German computer scientist. Career Nipkow received his Diplom (MSc) in computer science from the Department of Computer Science of the Technische Hochschule Darmstadt in 1982, and his Ph.D. from the University o ...
(1998)
''Term Rewriting and All That''
Cambridge University Press. * Franz Baader and (1993). "Unification Theory". In ''Handbook of Logic in Artificial Intelligence and Logic Programming''. * Jean-Pierre Jouannaud and
Claude Kirchner Claude Kirchner (February 11, 1916 – March 8, 1993), was an American television announcer and personality whose 50-year career in radio and television included hosting popular children's programs in Chicago and New York City from 1949 until 19 ...
(1991). "Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification". In ''Computational Logic: Essays in Honor of Alan Robinson''. *
Nachum Dershowitz Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the multiset path ordering used to prove termination of term rewrite systems. He obtained his B.Sc. summa cum laude in 1974 in Computer Scien ...
and Jean-Pierre Jouannaud, ''Rewrite Systems'', in:
Jan van Leeuwen Jan van Leeuwen (born December 17, 1946, in Waddinxveen) is a Dutch computer scientist and Emeritus professor of computer science at the Department of Information and Computing Sciences at Utrecht University.
(ed.), '' Handbook of Theoretical Computer Science'', volume B ''Formal Models and Semantics'', Elsevier, 1990, pp. 243–320 * Jörg H. Siekmann (1990). "Unification Theory". In
Claude Kirchner Claude Kirchner (February 11, 1916 – March 8, 1993), was an American television announcer and personality whose 50-year career in radio and television included hosting popular children's programs in Chicago and New York City from 1949 until 19 ...
(editor) ''Unification''. Academic Press. * * Gérard Huet and Derek C. Oppen (1980)
"Equations and Rewrite Rules: A Survey"
Technical report. Stanford University. * {{cite journal , last1 = Raulefs , first1 = Peter , last2 = Siekmann , first2 = Jörg , last3 = Szabó , first3 = P. , last4 = Unvericht , first4 = E. , year = 1979 , title = A short survey on the state of the art in matching and unification problems , journal = ACM SIGSAM Bulletin , volume = 13 , issue = 2 , pages = 14–20 , doi = 10.1145/1089208.1089210 , s2cid = 17033087 * Claude Kirchner and Hélène Kirchner. ''Rewriting, Solving, Proving''. In preparation. Automated theorem proving Logic programming Rewriting systems Logic in computer science Type theory