Теңдеулерді шешудің алгоритмдік процесі

Algorithmic process of solving equations
In logic and computer science, specifically automated reasoning, 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, and taking f to be an uninterpreted function, the singleton equation set { f(1,y) = f(x,2) } is a syntactic first order unification problem that has the substitution { x ↦ 1, y ↦ 2 } as its only solution. Conventions differ on what values variables may assume and which expressions are considered equivalent. In first order syntactic unification, variables range over first order terms and equivalence is syntactic. This version of unification has a unique "best" answer and is used in logic programming and programming language type system implementation, especially in Hindley–Milner based type inference algorithms. In higher order unification, possibly restricted to higher order pattern unification, terms may include lambda expressions, and equivalence is up to beta reduction. This version is used in proof assistants and higher order logic programming, for example Isabelle, Twelf, and lambdaProlog. Finally, in semantic unification or E unification, equality is subject to background knowledge and variables range over a variety of domains. This version is used in SMT solvers, term rewriting algorithms, and cryptographic protocol analysis.

A unification problem is a finite set of equations to solve, where li, ri are in the set of terms or expressions. Depending on which expressions or terms are allowed to occur in an equation set or unification problem, and which expressions are considered equal, several frameworks of unification are distinguished. If higher order variables, that is, variables representing functions, 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. If the right side of each equation is closed (no free variables), the problem is called (pattern) matching. The left side (with variables) of each equation is called the pattern.

A substitution σ is a solution of the unification problem E if liσ ≡ riσ for Such a substitution is also called a unifier of E.
For example, if ⊕ is associative, the unification problem { x ⊕ a ≐ a ⊕ x } has the solutions {x ↦ a}, {x ↦ a ⊕ a}, {x ↦ a ⊕ a ⊕ a}, etc., while the problem { x ⊕ a ≐ a } has no solution. For a given unification problem E, a set S of unifiers is called complete if each solution substitution is subsumed by some substitution in S. A complete substitution set always exists (e. g. the set of all solutions), but in some frameworks (such as unrestricted higher order unification) the problem of determining whether any solution exists (i. e., whether the complete substitution set is nonempty) is undecidable. The set S is called minimal if none of its members subsumes another one. Depending on the framework, a complete and minimal substitution set may have zero, one, finitely many, or infinitely many members, or may not exist at all due to an infinite chain of redundant members. Thus, in general, unification algorithms compute a finite approximation of the complete set, which may or may not be minimal, although most algorithms avoid redundant unifiers when possible. gave an algorithm that reports unsolvability or computes a single unifier that by itself forms a complete and minimal substitution set, called the most general unifier.

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.

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. Prolog notation Mathematical notation Unifying substitution Explanation a = a { a = a } {} Succeeds. (tautology) a = b { a = b } ⊥ a and b do not match X = X { x = x } {} Succeeds. (tautology) a = X { a = x } { x ↦ a } x is unified with the constant a X = Y { x = y } { x ↦ y } x and y are aliased f(a,X) = f(a,b) { f(a,x) = f(a,b) } { x ↦ b } function and constant symbols match, x is unified with the constant b f(a) = g(a) { f(a) = g(a) } ⊥ f and g do not match f(X) = f(Y) { f(x) = f(y) } { x ↦ y } x and y are aliased f(X) = g(Y) { f(x) = g(y) } ⊥ f and g do not match f(X) = f(Y,Z) { f(x) = f(y,z) } ⊥ Fails. The f function symbols have different arity f(g(X)) = f(Y) { f(g(x)) = f(y) } { y ↦ g(x) } Unifies y with the term g(x) f(g(X),X) = f(Y,a) { f(g(x),x) = f(y,a) } { x ↦ a, y ↦ g(a) } Unifies x with constant a, and y with the term g(a) X = f(X) { x = f(x) } should be ⊥ Returns ⊥ in first order logic and many modern Prolog dialects (enforced by the occurs check). Succeeds in traditional Prolog and in Prolog II, unifying x with infinite term x=f(f(f(f( )))). X = Y, Y = a { x = y, y = a } { x ↦ a, y ↦ a } Both x and y are unified with the constant a a = Y, X = Y { a = y, x = y } { x ↦ a, y ↦ a } As above (order of equations in set doesn't matter) X = a, b = X { x = a, b = x } ⊥ Fails. a and b do not match, so x can't be unified with both

The most general unifier of a syntactic first order unification problem of size n may have a size of 2^(n). For example, the problem (((a*z)*y)*x)*w \doteq w*(x*(y*(z*a))) has the most general unifier \{ z \mapsto a, y \mapsto a*a, x \mapsto (a*a)*(a*a), w \mapsto ((a*a)*(a*a))*((a*a)*(a*a)) \} , cf. picture. In order to avoid exponential time complexity caused by such blow up, advanced unification algorithms work on directed acyclic graphs (dags) rather than trees.

Unification has been used in different research areas of computational linguistics.

Order sorted logic allows one to assign a sort, or type, to each term, and to declare a sort s1 a subsort of another sort s2, commonly written as s1 ⊆ s2. 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 gave a unification algorithm for terms in order sorted logic, requiring for any two declared sorts s1, s2 their intersection s1 ∩ s2 to be declared, too: if x1 and x2 is a variable of sort s1 and s2, respectively, the equation x1 ≐ x2 has the solution { x1 = x, x2 = x }, where x: s1 ∩ s2. 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 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), 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.