/usr/lib/swi-prolog/doc/Manual/compare.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">

<HTML>
<HEAD>
<TITLE>SWI-Prolog 5.11.18 Reference Manual: Section 4.6</TITLE><LINK REL=home HREF="index.html">
<LINK REL=contents HREF="Contents.html">
<LINK REL=index HREF="DocIndex.html">
<LINK REL=summary HREF="summary.html">
<LINK REL=previous HREF="typetest.html">
<LINK REL=next HREF="control.html">
<STYLE type="text/css">
/* Style sheet for SWI-Prolog latex2html
*/

dd.defbody
{ margin-bottom: 1em;
}

dt.pubdef
{ background-color: #c5e1ff;
}

dt.multidef
{ background-color: #c8ffc7;
}

.bib dd
{ margin-bottom: 1em;
}

.bib dt
{ float: left;
margin-right: 1.3ex;
}

pre.code
{ margin-left: 1.5em;
margin-right: 1.5em;
border: 1px dotted;
padding-top: 5px;
padding-left: 5px;
padding-bottom: 5px;
background-color: #f8f8f8;
}

div.navigate
{ text-align: center;
background-color: #f0f0f0;
border: 1px dotted;
padding: 5px;
}

div.title
{ text-align: center;
padding-bottom: 1em;
font-size: 200%;
font-weight: bold;
}

div.author
{ text-align: center;
font-style: italic;
}

div.abstract
{ margin-top: 2em;
background-color: #f0f0f0;
border: 1px dotted;
padding: 5px;
margin-left: 10%; margin-right:10%;
}

div.abstract-title
{ text-align: center;
padding: 5px;
font-size: 120%;
font-weight: bold;
}

div.toc-h1
{ font-size: 200%;
font-weight: bold;
}

div.toc-h2
{ font-size: 120%;
font-weight: bold;
margin-left: 2em;
}

div.toc-h3
{ font-size: 100%;
font-weight: bold;
margin-left: 4em;
}

div.toc-h4
{ font-size: 100%;
margin-left: 6em;
}

span.sec-nr
{
}

span.sec-title
{
}

span.pred-ext
{ font-weight: bold;
}

span.pred-tag
{ float: right;
padding-top: 0.2em;
font-size: 80%;
font-style: italic;
color: #202020;
}

/* Footnotes */

sup.fn { color: blue; text-decoration: underline; }
span.fn-text { display: none; }
sup.fn span {display: none;}
sup:hover span
{ display: block !important;
position: absolute; top: auto; left: auto; width: 80%;
color: #000; background: white;
border: 2px solid;
padding: 5px; margin: 10px; z-index: 100;
font-size: smaller;
}
</STYLE>
</HEAD>
<BODY BGCOLOR="white">
<DIV class="navigate"><A class="nav" href="index.html"><IMG SRC="home.gif" BORDER=0 ALT="Home"></A>
<A class="nav" href="Contents.html"><IMG SRC="index.gif" BORDER=0 ALT="Contents"></A>
<A class="nav" href="DocIndex.html"><IMG SRC="yellow_pages.gif" BORDER=0 ALT="Index"></A>
<A class="nav" href="summary.html"><IMG SRC="info.gif" BORDER=0 ALT="Summary"></A>
<A class="nav" href="typetest.html"><IMG SRC="prev.gif" BORDER=0 ALT="Previous"></A>
<A class="nav" href="control.html"><IMG SRC="next.gif" BORDER=0 ALT="Next"></A>
</DIV>

<H2><A NAME="sec:4.6"><SPAN class="sec-nr">4.6</SPAN> <SPAN class="sec-title">Comparison 
and Unification of Terms</SPAN></A></H2>

<A NAME="sec:compare"></A>

<P>Although unification is mostly done implicitly while matching the 
head of a predicate, it is also provided by the predicate =/2.

<DL class="latex">
<DT class="pubdef"><span class="pred-tag">[ISO]</span><A NAME="=/2"><VAR>+Term1</VAR> <STRONG>=</STRONG> <VAR>+Term2</VAR></A></DT>
<DD class="defbody">
Unify <VAR>Term1</VAR> with <VAR>Term2</VAR>. True if the unification 
succeeds. For behaviour on cyclic terms see the Prolog flag
<A class="flag" href="flags.html#flag:occurs_check">occurs_check</A>. It 
acts as if defined by the following fact.

<PRE class="code">
=(Term, Term).
</PRE>

</DD>
<DT class="pubdef"><span class="pred-tag">[ISO]</span><A NAME="\=/2"><VAR>+Term1</VAR> <STRONG>\=</STRONG> <VAR>+Term2</VAR></A></DT>
<DD class="defbody">
Equivalent to <CODE><CODE>\+</CODE>Term1 = Term2</CODE>. See also <A NAME="idx:dif2:505"></A><A class="pred" href="coroutining.html#dif/2">dif/2</A>.
</DD>
</DL>

<H3><A NAME="sec:4.6.1"><SPAN class="sec-nr">4.6.1</SPAN> <SPAN class="sec-title">Standard 
Order of Terms</SPAN></A></H3>

<A NAME="sec:standardorder"></A>

<P>Comparison and unification of arbitrary terms. Terms are ordered in 
the so called ``standard order''. This order is defined as follows:

<P>
<OL class="latex">
<LI><VAR><VAR>Variables</VAR> &lt; <VAR>Numbers</VAR> &lt; <VAR>Atoms</VAR> 
&lt; <VAR>Strings</VAR> &lt; <VAR>Compound Terms</VAR></VAR><SUP class="fn">26<SPAN class="fn-text">Strings 
might be considered atoms in future versions. See also <A class="sec" href="strings.html">section 
4.22</A></SPAN></SUP>
<LI>Variables are sorted by address. Attaching attributes (see <A class="sec" href="attvar.html">section 
6.1</A>) does not affect the ordering.
<LI><VAR>Atoms</VAR> are compared alphabetically.
<LI><VAR>Strings</VAR> are compared alphabetically.
<LI><VAR>Numbers</VAR> are compared by value. Mixed integer/float are 
compared as floats. If the comparison is equal, the float is considered 
the smaller value. If the Prolog flag <A class="flag" href="flags.html#flag:iso">iso</A> 
is defined, all floating point numbers precede all integers.
<LI><VAR>Compound</VAR> terms are first checked on their arity, then on 
their functor-name (alphabetically) and finally recursively on their 
arguments, leftmost argument first.
</OL>

<DL class="latex">
<DT class="pubdef"><span class="pred-tag">[ISO]</span><A NAME="==/2"><VAR>+Term1</VAR> <STRONG>==</STRONG> <VAR>+Term2</VAR></A></DT>
<DD class="defbody">
True if <VAR>Term1</VAR> is equivalent to <VAR>Term2</VAR>. A variable 
is only identical to a sharing variable.</DD>
<DT class="pubdef"><span class="pred-tag">[ISO]</span><A NAME="\==/2"><VAR>+Term1</VAR> <STRONG>\==</STRONG> <VAR>+Term2</VAR></A></DT>
<DD class="defbody">
Equivalent to <CODE><CODE>\+</CODE>Term1 == Term2</CODE>.</DD>
<DT class="pubdef"><span class="pred-tag">[ISO]</span><A NAME="@</2"><VAR>+Term1</VAR> <STRONG>@&lt;</STRONG> <VAR>+Term2</VAR></A></DT>
<DD class="defbody">
True if <VAR>Term1</VAR> is before <VAR>Term2</VAR> in the standard 
order of terms.</DD>
<DT class="pubdef"><span class="pred-tag">[ISO]</span><A NAME="@=</2"><VAR>+Term1</VAR> <STRONG>@=&lt;</STRONG> <VAR>+Term2</VAR></A></DT>
<DD class="defbody">
True if both terms are equal (<A class="pred" href="compare.html#==/2">==/2</A>) 
or <VAR>Term1</VAR> is before <VAR>Term2</VAR> in the standard order of 
terms.</DD>
<DT class="pubdef"><span class="pred-tag">[ISO]</span><A NAME="@>/2"><VAR>+Term1</VAR> <STRONG>@&gt;</STRONG> <VAR>+Term2</VAR></A></DT>
<DD class="defbody">
True if <VAR>Term1</VAR> is after <VAR>Term2</VAR> in the standard order 
of terms.</DD>
<DT class="pubdef"><span class="pred-tag">[ISO]</span><A NAME="@>=/2"><VAR>+Term1</VAR> <STRONG>@&gt;=</STRONG> <VAR>+Term2</VAR></A></DT>
<DD class="defbody">
True if both terms are equal (<A class="pred" href="compare.html#==/2">==/2</A>) 
or <VAR>Term1</VAR> is after <VAR>Term2</VAR> in the standard order of 
terms.</DD>
<DT class="pubdef"><A NAME="compare/3"><STRONG>compare</STRONG>(<VAR>?Order, 
+Term1, +Term2</VAR>)</A></DT>
<DD class="defbody">
Determine or test the <VAR>Order</VAR> between two terms in the standard 
order of terms. <VAR>Order</VAR> is one of <CODE><CODE>&lt;</CODE></CODE>, <CODE><CODE>&gt;</CODE></CODE> 
or <CODE><CODE>=</CODE></CODE>, with the obvious meaning.
</DD>
</DL>

<H3><A NAME="sec:4.6.2"><SPAN class="sec-nr">4.6.2</SPAN> <SPAN class="sec-title">Special 
unification and comparison predicates</SPAN></A></H3>

<A NAME="sec:unifyspecial"></A>

<P>This section describes special purpose variations on Prolog 
unification. The predicate <A NAME="idx:unifywithoccurscheck2:506"></A><A class="pred" href="compare.html#unify_with_occurs_check/2">unify_with_occurs_check/2</A> 
provides sound unification and is part of the ISO standard. The 
predicate <A NAME="idx:subsumesterm2:507"></A><A class="pred" href="compare.html#subsumes_term/2">subsumes_term/2</A> 
defines `one-sided-unification' and is part of the ISO proposal 
established in Edinburgh (2010). Finally, <A NAME="idx:unifiable3:508"></A><A class="pred" href="compare.html#unifiable/3">unifiable/3</A> 
is a `what-if' version of unification that is often used as a building 
block in constraint reasoners.

<DL class="latex">
<DT class="pubdef"><span class="pred-tag">[ISO]</span><A NAME="unify_with_occurs_check/2"><STRONG>unify_with_occurs_check</STRONG>(<VAR>+Term1, 
+Term2</VAR>)</A></DT>
<DD class="defbody">
As <A class="pred" href="compare.html#=/2">=/2</A>, but using <EM>sound-unification</EM>. 
That is, a variable only unifies to a term if this term does not contain 
the variable itself. To illustrate this, consider the two goals below:

<PRE class="code">
1 ?- A = f(A).

A = f(f(f(f(f(f(f(f(f(f(...))))))))))
2 ?- unify_with_occurs_check(A, f(A)).

No
</PRE>

<P><A NAME="idx:occurscheck:509"></A>I.e. the first creates a <EM>cyclic-term</EM>, 
which is printed as an infinitely nested <CODE>f/1</CODE> term (see the <CODE>max_depth</CODE> 
option of <A NAME="idx:writeterm2:510"></A><A class="pred" href="termrw.html#write_term/2">write_term/2</A>). 
The second executes logically sound unification and thus fails. Note 
that the behaviour of unification through
<A class="pred" href="compare.html#=/2">=/2</A> as well as implicit 
unification in the head can be changed using the Prolog flag <A class="flag" href="flags.html#flag:occurs_check">occurs_check</A>.</DD>
<DT class="pubdef"><A NAME="=@=/2"><VAR>+Term1</VAR> <STRONG>=@=</STRONG> <VAR>+Term2</VAR></A></DT>
<DD class="defbody">
<A NAME="idx:variant:511"></A>True if <VAR>Term1</VAR> is a <EM>variant</EM> 
of (or <EM>structurally equivalent</EM> to) <VAR>Term2</VAR>. Testing 
for a variant is weaker than equivalence (<A class="pred" href="compare.html#==/2">==/2</A>), 
but stronger than unification (<A class="pred" href="compare.html#=/2">=/2</A>). 
Two terms <VAR>A</VAR> and <VAR>B</VAR> are variants iff there exists a 
renaming of the variables in <VAR>A</VAR> that makes <VAR>A</VAR> 
equivalent (==) to <VAR>B</VAR> and visa-versa.<SUP class="fn">27<SPAN class="fn-text">Row&nbsp;7 
and 8 of this table may come as a surprise, but row&nbsp;8 is satisfied 
by (left-to-right) <VAR>A -&gt; C</VAR>, <VAR>B -&gt; A</VAR> and 
(right-to-left) <VAR>C -&gt; A</VAR>, <VAR>A -&gt; B</VAR>. If the same 
variable appears in different locations in the left and right term, the 
variant-relation can be broken by consistent binding of both terms. 
E.g., after binding the first argument in row&nbsp;8 to a value both 
terms are no longer variant.</SPAN></SUP> Examples:
<BLOCKQUOTE>
<TABLE BORDER=0 FRAME=void RULES=groups>
<TR VALIGN=top><TD ALIGN=right>1</TD><TD ALIGN=center><TT>a =@= A</TT></TD><TD ALIGN=center>false </TD></TR>
<TR VALIGN=top><TD ALIGN=right>2</TD><TD ALIGN=center><TT>A =@= B</TT></TD><TD ALIGN=center>true </TD></TR>
<TR VALIGN=top><TD ALIGN=right>3</TD><TD ALIGN=center><TT>x(A,A) =@= 
x(B,C)</TT></TD><TD ALIGN=center>false </TD></TR>
<TR VALIGN=top><TD ALIGN=right>4</TD><TD ALIGN=center><TT>x(A,A) =@= 
x(B,B)</TT></TD><TD ALIGN=center>true </TD></TR>
<TR VALIGN=top><TD ALIGN=right>5</TD><TD ALIGN=center><TT>x(A,A) =@= 
x(A,B)</TT></TD><TD ALIGN=center>false </TD></TR>
<TR VALIGN=top><TD ALIGN=right>6</TD><TD ALIGN=center><TT>x(A,B) =@= 
x(C,D)</TT></TD><TD ALIGN=center>true </TD></TR>
<TR VALIGN=top><TD ALIGN=right>7</TD><TD ALIGN=center><TT>x(A,B) =@= 
x(B,A)</TT></TD><TD ALIGN=center>true </TD></TR>
<TR VALIGN=top><TD ALIGN=right>8</TD><TD ALIGN=center><TT>x(A,B) =@= 
x(C,A)</TT></TD><TD ALIGN=center>true </TD></TR>
</TABLE>

</BLOCKQUOTE>

<P>A term is always a variant of a copy of itself. Term copying takes 
place in e.g., <A NAME="idx:copyterm2:512"></A><A class="pred" href="manipterm.html#copy_term/2">copy_term/2</A>, <A NAME="idx:findall3:513"></A><A class="pred" href="allsolutions.html#findall/3">findall/3</A> 
or proving a clause added with
<A NAME="idx:asserta1:514"></A><A class="pred" href="db.html#asserta/1">asserta/1</A>. 
In the pure Prolog world (i.e., without attributed variables), <A class="pred" href="compare.html#=@=/2">=@=/2</A> 
behaves as if defined below. With attributed variables, variant of the 
attributes is tested rather than trying to satisfy the constraints.

<PRE class="code">
A =@= B :-
        copy_term(A, Ac),
        copy_term(B, Bc),
        numbervars(Ac, 0, N),
        numbervars(Bc, 0, N),
        Ac == Bc.
</PRE>

<P>The SWI-Prolog implementation is cycle-safe and can deal with 
variables that are shared between the left and right argument.<SUP class="fn">bug<SPAN class="fn-text">The 
combination of sharing and cycles may produce false possitives.</SPAN></SUP> 
Its performance is comparable to <A class="pred" href="compare.html#==/2">==/2</A>, 
both on success and (early) failure. Unlike ==, the variant 
implementation does not benefit from sharing subterms.<SUP class="fn">28<SPAN class="fn-text">The 
current implementation is based on ideas from Kuniaki Mukai.</SPAN></SUP>

<P>This predicate is known by the name <SPAN class="pred-ext">variant/2</SPAN> 
in some other Prolog systems. Be aware of possible differences in 
semantics if the arguments contain attributed variables or share 
variables.<SUP class="fn">29<SPAN class="fn-text">In many systems 
variant is implemented using two calls to <A NAME="idx:subsumesterm2:515"></A><A class="pred" href="compare.html#subsumes_term/2">subsumes_term/2</A>.</SPAN></SUP></DD>
<DT class="pubdef"><A NAME="\=@=/2"><VAR>+Term1</VAR> <STRONG>\=@=</STRONG> <VAR>+Term2</VAR></A></DT>
<DD class="defbody">
Equivalent to <CODE>`<CODE>\+</CODE>Term1 =@= Term2'</CODE>. See <A class="pred" href="compare.html#=@=/2">=@=/2</A> 
for details.</DD>
<DT class="pubdef"><span class="pred-tag">[ISO]</span><A NAME="subsumes_term/2"><STRONG>subsumes_term</STRONG>(<VAR>@Generic, @Specific</VAR>)</A></DT>
<DD class="defbody">
True if <VAR>Generic</VAR> can be made equivalent to <VAR>Specific</VAR> 
by only binding variables in <VAR>Generic</VAR>. The current 
implementation performs the unification and ensures that the variable 
set of <VAR>Specific</VAR> is not changed by the unification. On 
success, the bindings are undone.<SUP class="fn">30<SPAN class="fn-text">This 
predicate is often named <A NAME="idx:subsumeschk2:516"></A><SPAN class="pred-ext">subsumes_chk/2</SPAN> 
in older Prolog dialects. The current name was established in the ISO 
WG17 meeting in Edinburgh (2010). The <TT>chk</TT> postfix was 
considered to refer to determinism as in e.g., <A NAME="idx:memberchk2:517"></A><A class="pred" href="builtinlist.html#memberchk/2">memberchk/2</A>.</SPAN></SUP></DD>
<DT class="pubdef"><A NAME="term_subsumer/3"><STRONG>term_subsumer</STRONG>(<VAR>+Special1, 
+Special2, -General</VAR>)</A></DT>
<DD class="defbody">
<VAR>General</VAR> is the most specific term that is a generalisation of
<VAR>Special1</VAR> and <VAR>Special2</VAR>. The implementation can 
handle cyclic terms.</DD>
<DT class="pubdef"><A NAME="unifiable/3"><STRONG>unifiable</STRONG>(<VAR>@X, @Y, 
-Unifier</VAR>)</A></DT>
<DD class="defbody">
If <VAR>X</VAR> and <VAR>Y</VAR> can unify, unify <VAR>Unifier</VAR> 
with a list of
<VAR>Var</VAR> = <VAR>Value</VAR>, representing the bindings required to 
make <VAR>X</VAR> and <VAR>Y</VAR> equivalent.<SUP class="fn">31<SPAN class="fn-text">This 
predicate was introduced for the implementation of <A NAME="idx:dif2:518"></A><A class="pred" href="coroutining.html#dif/2">dif/2</A> 
and <A NAME="idx:when2:519"></A><A class="pred" href="coroutining.html#when/2">when/2</A> 
after discussion with Tom Schrijvers and Bart Demoen. None of us is 
really happy with the name and therefore suggestions for a new name are 
welcome.</SPAN></SUP> This predicate can handle cyclic terms. Attributed 
variables are handles as normal variables. Associated hooks are <EM>not</EM> 
executed.</DD>
<DT class="pubdef"><A NAME="?=/2"><STRONG>?=</STRONG>(<VAR>@Term1, @Term2</VAR>)</A></DT>
<DD class="defbody">
Succeeds, if the syntactic equality of <VAR>Term1</VAR> and <VAR>Term2</VAR> 
can be decided safely, i.e. if the result of <CODE>Term1 == Term2</CODE> 
will not change due to further instantiation of either term. It behaves 
as if defined by <CODE>?=(X,Y) :- \+ unifiable(X,Y,[_|_]).</CODE>
</DD>
</DL>

<P></BODY></HTML>
swi-prolog-nox 5.10.4-3ubuntu1 / usr / lib / swi-prolog / doc / Manual / compare.html
