Editing Unification (computer science) (section)

===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 τ.