Editing Unification (computer science) (section)

==E-unification==
'''E-unification''' is the problem of finding solutions to a given set of [[equations]],
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]] (a.k.a. ''E-unification algorithms'') have been devised;
for others it has been proven that no such algorithms can exist.

For example, if {{mvar|a}} and {{mvar|b}} are distinct constants,
the [[equation]] {{tmath|x * a \doteq y * b}} has no solution
with respect to purely [[syntactic unification]],
where nothing is known about the operator {{tmath|*}}.
However, if the {{tmath|*}} is known to be [[commutative]],
then the substitution {{math|{{mset|''x'' ↦ ''b'', ''y'' ↦ ''a''}}}} solves the above equation,
since
:{|
|
| {{tmath|x * a}}
| {{math|{{mset|''x'' ↦ ''b'', ''y'' ↦ ''a''}}}}
|-
| {{=}}
| {{tmath|b * a}}
|
| by [[#Substitution|substitution application]]
|-
| {{=}}
| {{tmath|a * b}}
|
| by commutativity of {{tmath|*}}
|-
| {{=}}
| {{tmath|y * b}}
| {{math|{{mset|''x'' ↦ ''b'', ''y'' ↦ ''a''}}}}
| by (converse) substitution application
|}
The background knowledge ''E'' could state the commutativity of {{tmath|*}} by the universal equality
"{{tmath|1=u * v = v * u}} for all {{math|''u'', ''v''}}".

===Particular background knowledge sets E===
{|
|+ '''Used naming conventions'''
| {{math|∀ ''u'',''v'',''w'':}}
| align="right" | {{tmath|u*(v*w)}}
| {{=}}
| {{tmath|(u*v)*w}}
| align="center" | '''{{mvar|A}}'''
| Associativity of {{tmath|*}}
|-
| {{math|∀ ''u'',''v'':}}
| align="right" | {{tmath|u*v}}
| =
| {{tmath|v*u}}
| align="center" | '''{{mvar|C}}'''
| Commutativity of {{tmath|*}}
|-
| {{math|∀ ''u'',''v'',''w'':}}
| align="right" | {{tmath|u*(v+w)}}
| {{=}}
| {{tmath|u*v+u*w}}
| align="center" | '''{{mvar|D<sub>l</sub>}}'''
| Left distributivity of {{tmath|*}} over {{tmath|+}}
|-
| {{math|∀ ''u'',''v'',''w'':}}
| align="right" | {{tmath|(v+w)*u}}
| {{=}}
| {{tmath|v*u+w*u}}
| align="center" | '''{{mvar|D<sub>r</sub>}}'''
| Right distributivity of {{tmath|*}} over {{tmath|+}}
|-
| {{math|∀ ''u'':}}
| align="right" | {{tmath|u*u}}
| {{=}}
| {{mvar|u}}
| align="center" | '''{{mvar|I}}'''
| Idempotence of {{tmath|*}}
|-
| {{math|∀ ''u'':}}
| align="right" | {{tmath|n*u}}
| {{=}}
| {{mvar|u}}
| align="center" | '''{{mvar|N<sub>l</sub>}}'''
| Left neutral element {{mvar|n}} with respect to {{tmath|*}}
|-
| {{math|∀ ''u'':}}
| align="right" | {{tmath|u*n}}
| {{=}}
| {{mvar|u}}
| align="center" | &nbsp; &nbsp; '''{{mvar|N<sub>r</sub>}}''' &nbsp; &nbsp;
| Right neutral element {{mvar|n}} with respect to {{tmath|*}}
|}

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:
* '''{{mvar|A}}'''<ref>[[Gordon D. Plotkin]], ''Lattice Theoretic Properties of Subsumption'', Memorandum MIP-R-77, Univ. Edinburgh, Jun 1970</ref>
* '''{{mvar|A}}''','''{{mvar|C}}'''<ref>[[Mark E. Stickel]], ''A Unification Algorithm for Associative-Commutative Functions'', Journal of the Association for Computing Machinery, vol.28, no.3, pp. 423–434, 1981</ref>
* '''{{mvar|A}}''','''{{mvar|C}}''','''{{mvar|I}}'''<ref name="Fages.1987">F. Fages, ''Associative-Commutative Unification'', J. Symbolic Comput., vol.3, no.3, pp. 257–275, 1987</ref>
* '''{{mvar|A}}''','''{{mvar|C}}''','''{{mvar|N<sub>l</sub>}}'''<ref group=note name="LRequivC">in the presence of equality '''{{mvar|C}}''', equalities '''{{mvar|N<sub>l</sub>}}''' and '''{{mvar|N<sub>r</sub>}}''' are equivalent, similar for '''{{mvar|D<sub>l</sub>}}''' and '''{{mvar|D<sub>r</sub>}}'''</ref><ref name="Fages.1987"/>
* '''{{mvar|A}}''','''{{mvar|I}}'''<ref>Franz Baader, ''Unification in Idempotent Semigroups is of Type Zero'', J. Automat. Reasoning, vol.2, no.3, 1986</ref>
* '''{{mvar|A}}''','''{{mvar|N<sub>l</sub>}}'''{{mvar|,}}'''{{mvar|N<sub>r</sub>}}''' (monoid)<ref>J. Makanin, ''The Problem of Solvability of Equations in a Free Semi-Group'', Akad. Nauk SSSR, vol.233, no.2, 1977</ref>
* '''{{mvar|C}}'''<ref>{{cite journal| author=F. Fages| title=Associative-Commutative Unification| journal=J. Symbolic Comput.| year=1987| volume=3| number=3| pages=257–275| doi=10.1016/s0747-7171(87)80004-4| s2cid=40499266| url=https://hal.inria.fr/inria-00076271/file/RR-0287.pdf}}</ref>
* [[Boolean ring]]s<ref>{{cite book| author=Martin, U., Nipkow, T.| chapter=Unification in Boolean Rings| title=Proc. 8th CADE| year=1986| volume=230| pages=506–513| publisher=Springer| editor=Jörg H. Siekmann| series=LNCS}}</ref><ref>{{cite journal|author1=A. Boudet |author2=J.P. Jouannaud |author3=M. Schmidt-Schauß | title=Unification of Boolean Rings and Abelian Groups| journal=Journal of Symbolic Computation| year=1989| volume=8|issue=5 | pages=449–477 | doi=10.1016/s0747-7171(89)80054-9| doi-access=free}}</ref>
* [[Abelian group]]s, even if the signature is expanded by arbitrary additional symbols (but not axioms)<ref name="Baader and Snyder 2001, p. 486">Baader and Snyder (2001), p. 486.</ref>
* [[Kripke semantics#Correspondence and completeness|K4]] [[modal algebra]]s<ref>F. Baader and S. Ghilardi, ''[https://web.archive.org/web/20171223215706/https://pdfs.semanticscholar.org/492e/9f03ab7abd043ed0167dc7309552d21a88ef.pdf Unification in modal and description logics]'', Logic Journal of the IGPL 19 (2011), no.&nbsp;6, pp.&nbsp;705–730.</ref>

''Unification is semi-decidable'' for the following theories:
* '''{{mvar|A}}''','''{{mvar|D<sub>l</sub>}}'''{{mvar|,}}'''{{mvar|D<sub>r</sub>}}'''<ref>P. Szabo, ''Unifikationstheorie erster Ordnung'' (''First Order Unification Theory''), Thesis, Univ. Karlsruhe, West Germany, 1982</ref>
* '''{{mvar|A}}''','''{{mvar|C}}''','''{{mvar|D<sub>l</sub>}}'''<ref group=note name="LRequivC"/><ref>Jörg H. Siekmann, ''Universal Unification'', Proc. 7th Int. Conf. on Automated Deduction, Springer LNCS vol.170, pp. 1–42, 1984</ref>
* [[Commutative ring]]s<ref name="Baader and Snyder 2001, p. 486"/>

===One-sided paramodulation===
If there is a [[convergent term rewriting system]] ''R'' available for ''E'',
the ''one-sided paramodulation'' algorithm<ref>N. Dershowitz and G. Sivakumar, ''Solving Goals in Equational Languages'', Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, Springer LNCS vol.308, pp. 45–55, 1988</ref>
can be used to enumerate all solutions of given equations.

{| style="border: 1px solid darkgray;"
|+ One-sided paramodulation rules
|- border="0"
| align="right" | ''G'' ∪ { ''f''(''s''<sub>1</sub>,...,''s''<sub>''n''</sub>) ≐ ''f''(''t''<sub>1</sub>,...,''t''<sub>''n''</sub>) }
| ; ''S''
| ⇒
| align="right" | ''G'' ∪ { ''s''<sub>1</sub> ≐ ''t''<sub>1</sub>, ..., ''s''<sub>''n''</sub> ≐ ''t''<sub>''n''</sub> }
| ''; ''S''
|
| &nbsp; &nbsp; ''decompose''
|-
| align="right" | ''G'' ∪ { ''x'' ≐ ''t'' }
| ; ''S''
| ⇒
| align="right" | ''G'' { ''x'' ↦ ''t'' }
|; ''S''{''x''↦''t''} ∪ {''x''↦''t''}
| align="right" | if the variable ''x'' doesn't occur in ''t''
| &nbsp; &nbsp; ''eliminate''
|-
| align="right" | ''G'' ∪ { ''f''(''s''<sub>1</sub>,...,''s''<sub>''n''</sub>) ≐ ''t'' }
| ; ''S''
| ⇒
| align="right" | ''G'' ∪ { ''s''<sub>1</sub> ≐ u<sub>1</sub>, ..., ''s''<sub>''n''</sub> ≐ u<sub>''n''</sub>, ''r'' ≐ ''t'' }
| ; ''S''
| align="right" | &nbsp; &nbsp; if ''f''(''u''<sub>1</sub>,...,''u''<sub>''n''</sub>) → ''r'' is a rule from ''R''
| &nbsp; &nbsp; ''mutate''
|-
| align="right" | ''G'' ∪ { ''f''(''s''<sub>1</sub>,...,''s''<sub>''n''</sub>) ≐ ''y'' }
| ; ''S''
|⇒
| align="right" | ''G'' ∪ { ''s''<sub>1</sub> ≐ ''y''<sub>1</sub>, ..., ''s''<sub>''n''</sub> ≐ ''y''<sub>''n''</sub>, ''y'' ≐ ''f''(''y''<sub>1</sub>,...,''y''<sub>''n''</sub>) }
| ; ''S''
| align="right" | if ''y''<sub>1</sub>,...,''y''<sub>''n''</sub> are new variables
| &nbsp; &nbsp; ''imitate''
|}

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'' = { ''f''(...) ≐ ''g''(...) }).

{| style="border: 1px solid darkgray;"
|+ Example term rewrite system ''R''
|- border="0"
| '''1'''
| ''app''(''nil'',''z'')
| → ''z''
|-
|'''2''' &nbsp; &nbsp;
| ''app''(''x''.''y'',''z'')
| → ''x''.''app''(''y'',''z'')
|}

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]] 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 { ''app''(''x'',''app''(''y'',''x'')) ≐ ''a''.''a''.''nil'' } is shown below. To avoid variable name clashes, rewrite rules are consistently renamed each time before their use by rule ''mutate''; ''v''<sub>2</sub>, ''v''<sub>3</sub>, ... 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'' = { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' } can be obtained. In fact,
''app''(''x'',''app''(''y'',''x'')) {''y''↦''nil'', ''x''↦ ''a''.''nil'' } = ''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'' = { ''y'' ↦ ''a''.''a''.''nil'', ''x'' ↦ ''nil'' }; it is not shown here. No other path leads to a success.

{| class="wikitable"
|+ Example unifier computation
|-
! Used rule !!  !! ''G'' !! ''S''
|-
| ||
| { {{color|red|''app''(''x'',''app''(''y'',''x'')) ≐ ''a''.''a''.''nil''}} }
| {}
|-
| mutate(2) || ⇒
| { ''x'' ≐ ''v''<sub>2</sub>.''v''<sub>3</sub>, ''app''(''y'',''x'') ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>2</sub>.''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''a''.''nil''}} }
| {}
|-
| decompose || ⇒
| { {{color|red|''x'' ≐ ''v''<sub>2</sub>.''v''<sub>3</sub>}}, ''app''(''y'',''x'') ≐ ''v''<sub>4</sub>, ''v''<sub>2</sub> ≐ ''a'', ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
| {}
|-
| eliminate || ⇒
| { ''app''(''y'',''v''<sub>2</sub>.''v''<sub>3</sub>) ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>2</sub> ≐ ''a''}}, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
| { ''x'' ↦  ''v''<sub>2</sub>.''v''<sub>3</sub> }
|-
| eliminate || ⇒
| { {{color|red|''app''(''y'',''a''.''v''<sub>3</sub>) ≐ ''v''<sub>4</sub>}}, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
| { ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| mutate(1) || ⇒
| { ''y'' ≐ ''nil'', ''a''.''v''<sub>3</sub> ≐ ''v''<sub>5</sub>, {{color|red|''v''<sub>5</sub> ≐ ''v''<sub>4</sub>}}, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
| { ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| eliminate || ⇒
| { {{color|red|''y'' ≐ ''nil''}}, ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
| { ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| eliminate || ⇒
| { ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, {{color|red|''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil''}} }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| mutate(1) || ⇒
| { ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, ''v''<sub>3</sub> ≐ ''nil'', {{color|red|''v''<sub>4</sub> ≐ ''v''<sub>6</sub>}}, ''v''<sub>6</sub> ≐ ''a''.''nil'' }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| eliminate || ⇒
| { ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>3</sub> ≐ ''nil''}}, ''v''<sub>4</sub> ≐ ''a''.''nil'' }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| eliminate || ⇒
| { ''a''.''nil'' ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>4</sub> ≐ ''a''.''nil''}} }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
|-
| eliminate || ⇒
| { {{color|red|''a''.''nil'' ≐ ''a''.''nil''}} }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
|-
| decompose || ⇒
| { {{color|red|''a'' ≐ ''a''}}, ''nil'' ≐ ''nil'' }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
|-
| decompose || ⇒
| { {{color|red|''nil'' ≐ ''nil''}} }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
|-
| decompose &nbsp; &nbsp; || ⇒ &nbsp; &nbsp;
| {}
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
|}

===Narrowing===
[[File:Triangle diagram of narrowing step svg.svg|thumb|Triangle diagram of narrowing step ''s'' ↝ ''t'' at position ''p'' in term ''s'', with unifying substitution σ (bottom row), using a rewrite rule {{math|1=''l'' → ''r''}} (top row)]]
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 {{math|''l'' → ''r''}} is a [[renamed copy]] of a rewrite rule from ''R'', having no variables in common with a term ''s'', and the [[subterm]] {{math|''s''{{!}}<sub>''p''</sub>}} is not a variable and is unifiable with {{mvar|l}} via the [[#Syntactic unification of first-order terms|mgu]] {{mvar|σ}}, then {{mvar|s}} can be ''narrowed'' to the term {{math|1=''t'' = ''sσ''[''rσ'']<sub>''p''</sub>}}, i.e. to the term {{mvar|sσ}}, with the subterm at ''p'' [[Term (logic)#Operations with terms|replaced]] by {{mvar|rσ}}. The situation that ''s'' can be narrowed to ''t'' is commonly denoted as ''s'' ↝ ''t''.
Intuitively, a sequence of narrowing steps ''t''<sub>1</sub> ↝ ''t''<sub>2</sub> ↝ ... ↝ ''t''<sub>''n''</sub> can be thought of as a sequence of rewrite steps ''t''<sub>1</sub> → ''t''<sub>2</sub> → ... → ''t''<sub>''n''</sub>, but with the initial term ''t''<sub>1</sub> being further and further instantiated, as necessary to make each of the used rules applicable.

The [[#One-sided paramodulation|above]] example paramodulation computation corresponds to the following narrowing sequence ("↓" indicating instantiation here):

{|
|-
| ''app''( || ''x'' || ,''app''(''y'', || ''x'' || ))
|-
|     ||  ↓  ||  ||  ↓  ||   ||  ||  ||  ||  ||  ||  ||  ||  ||  ||  ||  ||  ||  ''x'' ↦ ''v''<sub>2</sub>.''v''<sub>3</sub>
|-
| ''app''( || ''v''<sub>2</sub>.''v''<sub>3</sub> || ,''app''(''y'', || ''v''<sub>2</sub>.''v''<sub>3</sub> || ))  ||  →  ||  ''v''<sub>2</sub>.''app''(''v''<sub>3</sub>,''app''( || ''y'' || ,''v''<sub>2</sub>.''v''<sub>3</sub>))
|-
|     ||         ||         ||         ||     ||                   ||                   ||  ↓  ||  ||  ||  ||  ||  ||  ||  ||    ||  ||  ''y'' ↦ ''nil''
|-
|     ||         ||         ||         ||     ||                   ||  ''v''<sub>2</sub>.''app''(''v''<sub>3</sub>,''app''( || ''nil'' || ,''v''<sub>2</sub>.''v''<sub>3</sub>))  ||  →  ||  ''v''<sub>2</sub>.''app''( || ''v''<sub>3</sub> || ,''v''<sub>2</sub>. || ''v''<sub>3</sub> || )
|-
|     ||         ||         ||         ||     ||                   ||                   ||     ||             ||                   ||           ||  ↓  ||   ||  ↓  ||  ||  ||  ||  ''v''<sub>3</sub> ↦ ''nil''
|-
|     ||         ||         ||         ||     ||                   ||                   ||     ||             ||                   ||  ''v''<sub>2</sub>.''app''( || ''nil'' || ,''v''<sub>2</sub>. || ''nil'' || )  ||  →  ||  ''v''<sub>2</sub>.''v''<sub>2</sub>.''nil''
|}

The last term, ''v''<sub>2</sub>.''v''<sub>2</sub>.''nil'' can be syntactically unified with the original right hand side term ''a''.''a''.''nil''.

The ''narrowing lemma''<ref>{{cite book| author=Fay| chapter=First-Order Unification in an Equational Theory| title=Proc. 4th Workshop on Automated Deduction| year=1979| pages=161–167}}</ref> 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 {{math|1=''s{{prime}}''}} and {{math|1=''t{{prime}}''}}, respectively, such that {{math|1=''t{{prime}}''}} is an instance of {{math|1=''s{{prime}}''}}.

Formally: whenever {{math|1=''sσ'' {{underset|&lowast;|→}} ''t''}} holds for some substitution σ, then there exist terms {{math|''s{{prime}}'', ''t{{prime}}''}} such that {{math|''s'' {{underset|&lowast;|↝}} ''s{{prime}}''}} and {{math|''t'' {{underset|&lowast;|→}} ''t{{prime}}''}} and {{math|1=''s{{prime}}'' ''τ'' = ''t{{prime}}''}} for some substitution τ.