Menu
Home Explore People Places Arts History Plants & Animals Science Life & Culture Technology
On this page
Anti-unification
Logical generalization for symbolic expressions

Anti-unification is the process of finding a generalization common to two symbolic expressions, related to unification. It varies by the types of terms allowed, distinguishing between first-order anti-unification (without function variables) and higher-order anti-unification (with function variables). When the generalization must exactly match instances of the inputs, it is called syntactical anti-unification; otherwise, it’s known as E-anti-unification or anti-unification modulo theory. Algorithms aim to compute a complete, minimal set of generalizations, which may be finite or infinite. For first-order syntactical anti-unification, Gordon Plotkin developed an algorithm yielding the least general generalization (lgg). Anti-unification is distinct from dis-unification, which involves solving inequations rather than finding generalizations.

We don't have any images related to Anti-unification yet.
We don't have any YouTube videos related to Anti-unification yet.
We don't have any PDF documents related to Anti-unification yet.
We don't have any Books related to Anti-unification yet.
We don't have any archived web articles related to Anti-unification yet.

Prerequisites

Formally, an anti-unification approach presupposes

  • An infinite set V of variables. For higher-order anti-unification, it is convenient to choose V disjoint from the set of lambda-term bound variables.
  • A set T of terms such that V ⊆ T. For first-order and higher-order anti-unification, T is usually the set of first-order terms (terms built from variable and function symbols) and lambda terms (terms containing some higher-order variables), respectively.
  • An equivalence relation ≡ {\displaystyle \equiv } on T {\displaystyle T} , indicating which terms are considered equal. For higher-order anti-unification, usually t ≡ u {\displaystyle t\equiv u} if t {\displaystyle t} and u {\displaystyle u} are alpha equivalent. For first-order E-anti-unification, ≡ {\displaystyle \equiv } reflects the background knowledge about certain function symbols; for example, if ⊕ {\displaystyle \oplus } is considered commutative, t ≡ u {\displaystyle t\equiv u} if u {\displaystyle u} results from t {\displaystyle t} by swapping the arguments of ⊕ {\displaystyle \oplus } at some (possibly all) occurrences.5 If there is no background knowledge at all, then only literally, or syntactically, identical terms are considered equal.

First-order term

Main article: Term (logic)

Given a set V {\displaystyle V} of variable symbols, a set C {\displaystyle C} of constant symbols and sets F n {\displaystyle F_{n}} of n {\displaystyle n} -ary function symbols, also called operator symbols, for each natural number n ≥ 1 {\displaystyle n\geq 1} , the set of (unsorted first-order) terms T {\displaystyle T} is recursively defined to be the smallest set with the following properties:6

  • every variable symbol is a term: V ⊆ T,
  • every constant symbol is a term: C ⊆ T,
  • from every n terms t1,...,tn, and every n-ary function symbol f ∈ Fn, a larger term f ( t 1 , … , t n ) {\displaystyle f(t_{1},\ldots ,t_{n})} can be built.

For example, if x ∈ V is a variable symbol, 1 ∈ C is a constant symbol, and add ∈ F2 is a binary function symbol, then x ∈ T, 1 ∈ T, and (hence) add(x,1) ∈ T by the first, second, and third term building rule, respectively. The latter term is usually written as x+1, using Infix notation and the more common operator symbol + for convenience.

Higher-order term

Main article: Lambda calculus

Substitution

Main article: Substitution (logic)

A substitution is a mapping σ : V ⟶ T {\displaystyle \sigma :V\longrightarrow T} from variables to terms; the notation { x 1 ↦ t 1 , … , x k ↦ t k } {\displaystyle \{x_{1}\mapsto t_{1},\ldots ,x_{k}\mapsto t_{k}\}} refers to a substitution mapping each variable x i {\displaystyle x_{i}} to the term t i {\displaystyle t_{i}} , for i = 1 , … , k {\displaystyle i=1,\ldots ,k} , and every other variable to itself. Applying that substitution to a term t is written in postfix notation as t { x 1 ↦ t 1 , … , x k ↦ t k } {\displaystyle t\{x_{1}\mapsto t_{1},\ldots ,x_{k}\mapsto t_{k}\}} ; it means to (simultaneously) replace every occurrence of each variable x i {\displaystyle x_{i}} in the term t by t i {\displaystyle t_{i}} . The result tσ of applying a substitution σ to a term t is called an instance of that term t. As a first-order example, applying the substitution { x ↦ h ( a , y ) , z ↦ b } {\displaystyle \{x\mapsto h(a,y),z\mapsto b\}} to the term

f(x, a, g(z), y)yields
f(h(a,y), a, g(b), y).

Generalization, specialization

If a term t {\displaystyle t} has an instance equivalent to a term u {\displaystyle u} , that is, if t σ ≡ u {\displaystyle t\sigma \equiv u} for some substitution σ {\displaystyle \sigma } , then t {\displaystyle t} is called more general than u {\displaystyle u} , and u {\displaystyle u} is called more special than, or subsumed by, t {\displaystyle t} . For example, x ⊕ a {\displaystyle x\oplus a} is more general than a ⊕ b {\displaystyle a\oplus b} if ⊕ {\displaystyle \oplus } is commutative, since then ( x ⊕ a ) { x ↦ b } = b ⊕ a ≡ a ⊕ b {\displaystyle (x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b} .

If ≡ {\displaystyle \equiv } 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 ) {\displaystyle f(x_{1},a,g(z_{1}),y_{1})} is a variant of f ( x 2 , a , g ( z 2 ) , y 2 ) {\displaystyle f(x_{2},a,g(z_{2}),y_{2})} , since f ( x 1 , a , g ( z 1 ) , y 1 ) { x 1 ↦ x 2 , y 1 ↦ y 2 , z 1 ↦ z 2 } = f ( x 2 , a , g ( z 2 ) , y 2 ) {\displaystyle f(x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})} and f ( x 2 , a , g ( z 2 ) , y 2 ) { x 2 ↦ x 1 , y 2 ↦ y 1 , z 2 ↦ z 1 } = f ( x 1 , a , g ( z 1 ) , y 1 ) {\displaystyle f(x_{2},a,g(z_{2}),y_{2})\{x_{2}\mapsto x_{1},y_{2}\mapsto y_{1},z_{2}\mapsto z_{1}\}=f(x_{1},a,g(z_{1}),y_{1})} . However, f ( x 1 , a , g ( z 1 ) , y 1 ) {\displaystyle f(x_{1},a,g(z_{1}),y_{1})} is not a variant of f ( x 2 , a , g ( x 2 ) , x 2 ) {\displaystyle f(x_{2},a,g(x_{2}),x_{2})} , since no substitution can transform the latter term into the former one, although { x 1 ↦ x 2 , z 1 ↦ x 2 , y 1 ↦ x 2 } {\displaystyle \{x_{1}\mapsto x_{2},z_{1}\mapsto x_{2},y_{1}\mapsto x_{2}\}} achieves the reverse direction. The latter term is hence properly more special than the former one.

A substitution σ {\displaystyle \sigma } is more special than, or subsumed by, a substitution τ {\displaystyle \tau } if x σ {\displaystyle x\sigma } is more special than x τ {\displaystyle x\tau } for each variable x {\displaystyle x} . For example, { x ↦ f ( u ) , y ↦ f ( f ( u ) ) } {\displaystyle \{x\mapsto f(u),y\mapsto f(f(u))\}} is more special than { x ↦ z , y ↦ f ( z ) } {\displaystyle \{x\mapsto z,y\mapsto f(z)\}} , since f ( u ) {\displaystyle f(u)} and f ( f ( u ) ) {\displaystyle f(f(u))} is more special than z {\displaystyle z} and f ( z ) {\displaystyle f(z)} , respectively.

Anti-unification problem, generalization set

An anti-unification problem is a pair ⟨ t 1 , t 2 ⟩ {\displaystyle \langle t_{1},t_{2}\rangle } of terms. A term t {\displaystyle t} is a common generalization, or anti-unifier, of t 1 {\displaystyle t_{1}} and t 2 {\displaystyle t_{2}} if t σ 1 ≡ t 1 {\displaystyle t\sigma _{1}\equiv t_{1}} and t σ 2 ≡ t 2 {\displaystyle t\sigma _{2}\equiv t_{2}} for some substitutions σ 1 , σ 2 {\displaystyle \sigma _{1},\sigma _{2}} . For a given anti-unification problem, a set S {\displaystyle S} of anti-unifiers is called complete if each generalization subsumes some term t ∈ S {\displaystyle t\in S} ; the set S {\displaystyle S} is called minimal if none of its members subsumes another one.

First-order syntactical anti-unification

The framework of first-order syntactical anti-unification is based on T {\displaystyle T} being the set of first-order terms (over some given set V {\displaystyle V} of variables, C {\displaystyle C} of constants and F n {\displaystyle F_{n}} of n {\displaystyle n} -ary function symbols) and on ≡ {\displaystyle \equiv } being syntactic equality. In this framework, each anti-unification problem ⟨ t 1 , t 2 ⟩ {\displaystyle \langle t_{1},t_{2}\rangle } has a complete, and obviously minimal, singleton solution set { t } {\displaystyle \{t\}} . Its member t {\displaystyle t} is called the least general generalization (lgg) of the problem, it has an instance syntactically equal to t 1 {\displaystyle t_{1}} and another one syntactically equal to t 2 {\displaystyle t_{2}} . Any common generalization of t 1 {\displaystyle t_{1}} and t 2 {\displaystyle t_{2}} subsumes t {\displaystyle t} . The lgg is unique up to variants: if S 1 {\displaystyle S_{1}} and S 2 {\displaystyle S_{2}} are both complete and minimal solution sets of the same syntactical anti-unification problem, then S 1 = { s 1 } {\displaystyle S_{1}=\{s_{1}\}} and S 2 = { s 2 } {\displaystyle S_{2}=\{s_{2}\}} for some terms s 1 {\displaystyle s_{1}} and s 2 {\displaystyle s_{2}} , that are renamings of each other.

Plotkin78 has given an algorithm to compute the lgg of two given terms. It presupposes an injective mapping ϕ : T × T ⟶ V {\displaystyle \phi :T\times T\longrightarrow V} , that is, a mapping assigning each pair s , t {\displaystyle s,t} of terms an own variable ϕ ( s , t ) {\displaystyle \phi (s,t)} , such that no two pairs share the same variable. 9 The algorithm consists of two rules:

f ( s 1 , … , s n ) ⊔ f ( t 1 , … , t n ) {\displaystyle f(s_{1},\dots ,s_{n})\sqcup f(t_{1},\ldots ,t_{n})} ⇝ {\displaystyle \rightsquigarrow } f ( s 1 ⊔ t 1 , … , s n ⊔ t n ) {\displaystyle f(s_{1}\sqcup t_{1},\ldots ,s_{n}\sqcup t_{n})}
s ⊔ t {\displaystyle s\sqcup t} ⇝ {\displaystyle \rightsquigarrow } ϕ ( s , t ) {\displaystyle \phi (s,t)} if previous rule not applicable

For example, ( 0 ∗ 0 ) ⊔ ( 4 ∗ 4 ) ⇝ ( 0 ⊔ 4 ) ∗ ( 0 ⊔ 4 ) ⇝ ϕ ( 0 , 4 ) ∗ ϕ ( 0 , 4 ) ⇝ x ∗ x {\displaystyle (0*0)\sqcup (4*4)\rightsquigarrow (0\sqcup 4)*(0\sqcup 4)\rightsquigarrow \phi (0,4)*\phi (0,4)\rightsquigarrow x*x} ; this least general generalization reflects the common property of both inputs of being square numbers.

Plotkin used his algorithm to compute the "relative least general generalization (rlgg)" of two clause sets in first-order logic, which was the basis of the Golem approach to inductive logic programming.

First-order anti-unification modulo theory

Equational theories

First-order sorted anti-unification

Nominal anti-unification

  • Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (Jun 2013). Nominal Anti-Unification. Proc. RTA 2015. Vol. 36 of LIPIcs. Schloss Dagstuhl, 57-73. Software.

Applications

Higher-order anti-unification

Notes

References

  1. Complete generalization sets always exist, but it may be the case that every complete generalization set is non-minimal. ↩

  2. Plotkin, Gordon D. (1970). Meltzer, B.; Michie, D. (eds.). "A Note on Inductive Generalization". Machine Intelligence. 5: 153–163. ↩

  3. Plotkin, Gordon D. (1971). Meltzer, B.; Michie, D. (eds.). "A Further Note on Inductive Generalization". Machine Intelligence. 6: 101–124. ↩

  4. Comon referred in 1986 to inequation-solving as "anti-unification", which nowadays has become quite unusual. Comon, Hubert (1986). "Sufficient Completeness, Term Rewriting Systems and 'Anti-Unification'". Proc. 8th International Conference on Automated Deduction. LNCS. Vol. 230. Springer. pp. 128–140. ↩

  5. E.g. a ⊕ ( b ⊕ f ( x ) ) ≡ a ⊕ ( f ( x ) ⊕ b ) ≡ ( b ⊕ f ( x ) ) ⊕ a ≡ ( f ( x ) ⊕ b ) ⊕ a {\displaystyle a\oplus (b\oplus f(x))\equiv a\oplus (f(x)\oplus b)\equiv (b\oplus f(x))\oplus a\equiv (f(x)\oplus b)\oplus a} ↩

  6. C.C. Chang; H. Jerome Keisler (1977). A. Heyting; H.J. Keisler; A. Mostowski; A. Robinson; P. Suppes (eds.). Model Theory. Studies in Logic and the Foundation of Mathematics. Vol. 73. North Holland.; here: Sect.1.3 ↩

  7. Plotkin, Gordon D. (1970). Meltzer, B.; Michie, D. (eds.). "A Note on Inductive Generalization". Machine Intelligence. 5: 153–163. ↩

  8. Plotkin, Gordon D. (1971). Meltzer, B.; Michie, D. (eds.). "A Further Note on Inductive Generalization". Machine Intelligence. 6: 101–124. ↩

  9. From a theoretical viewpoint, such a mapping exists, since both V {\displaystyle V} and T × T {\displaystyle T\times T} are countably infinite sets; for practical purposes, ϕ {\displaystyle \phi } can be built up as needed, remembering assigned mappings ⟨ s , t , ϕ ( s , t ) ⟩ {\displaystyle \langle s,t,\phi (s,t)\rangle } in a hash table. /wiki/Countably_infinite ↩