/usr/share/doc/racket/racklog/unification.html is in racket-doc 6.1-4.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"/><title>5 Unification</title><link rel="stylesheet" type="text/css" href="../scribble.css" title="default"/><link rel="stylesheet" type="text/css" href="../racket.css" title="default"/><link rel="stylesheet" type="text/css" href="../manual-style.css" title="default"/><link rel="stylesheet" type="text/css" href="../manual-racket.css" title="default"/><link rel="stylesheet" type="text/css" href="../manual-racket.css" title="default"/><link rel="stylesheet" type="text/css" href="../doc-site.css" title="default"/><script type="text/javascript" src="../scribble-common.js"></script><script type="text/javascript" src="../manual-racket.js"></script><script type="text/javascript" src="../manual-racket.js"></script><script type="text/javascript" src="../doc-site.js"></script><script type="text/javascript" src="../local-redirect/local-redirect.js"></script><script type="text/javascript" src="../local-redirect/local-user-redirect.js"></script><!--[if IE 6]><style type="text/css">.SIEHidden { overflow: hidden; }</style><![endif]--></head><body id="doc-racket-lang-org"><div class="tocset"><div class="tocview"><div class="tocviewlist tocviewlisttopspace"><div class="tocviewtitle"><table cellspacing="0" cellpadding="0"><tr><td style="width: 1em;"><a href="javascript:void(0);" title="Expand/Collapse" class="tocviewtoggle" onclick="TocviewToggle(this,"tocview_0");">▼</a></td><td></td><td><a href="index.html" class="tocviewlink" data-pltdoc="x">Racklog:<span class="mywbr"> </span> Prolog-<wbr></wbr>Style Logic Programming</a></td></tr></table></div><div class="tocviewsublisttop" style="display: block;" id="tocview_0"><table cellspacing="0" cellpadding="0"><tr><td align="right">1 </td><td><a href="simple.html" class="tocviewlink" data-pltdoc="x">Simple Goals and Queries</a></td></tr><tr><td align="right">2 </td><td><a href="predicates.html" class="tocviewlink" data-pltdoc="x">Predicates</a></td></tr><tr><td align="right">3 </td><td><a href="racket-w-logic.html" class="tocviewlink" data-pltdoc="x">Using Conventional Racket Expressions in Racklog</a></td></tr><tr><td align="right">4 </td><td><a href="backtracking.html" class="tocviewlink" data-pltdoc="x">Backtracking</a></td></tr><tr><td align="right">5 </td><td><a href="" class="tocviewselflink" data-pltdoc="x">Unification</a></td></tr><tr><td align="right">6 </td><td><a href="and-or.html" class="tocviewlink" data-pltdoc="x">Conjuctions and Disjunctions</a></td></tr><tr><td align="right">7 </td><td><a href="lv-manip.html" class="tocviewlink" data-pltdoc="x">Manipulating Racklog Variables</a></td></tr><tr><td align="right">8 </td><td><a href="cut.html" class="tocviewlink" data-pltdoc="x">The Cut (<span class="RktSym"><span class="RktStxLink">!</span></span>)</a></td></tr><tr><td align="right">9 </td><td><a href="set-of.html" class="tocviewlink" data-pltdoc="x">Set Predicates</a></td></tr><tr><td align="right">10 </td><td><a href="Racklog_Module_Language.html" class="tocviewlink" data-pltdoc="x">Racklog Module Language</a></td></tr><tr><td align="right">11 </td><td><a href="glossary.html" class="tocviewlink" data-pltdoc="x">Glossary of Racklog Primitives</a></td></tr><tr><td align="right"></td><td><a href="doc-bibliography.html" class="tocviewlink" data-pltdoc="x">Bibliography</a></td></tr></table></div></div><div class="tocviewlist"><table cellspacing="0" cellpadding="0"><tr><td style="width: 1em;"><a href="javascript:void(0);" title="Expand/Collapse" class="tocviewtoggle" onclick="TocviewToggle(this,"tocview_1");">►</a></td><td>5 </td><td><a href="" class="tocviewselflink" data-pltdoc="x">Unification</a></td></tr></table><div class="tocviewsublistbottom" style="display: none;" id="tocview_1"><table cellspacing="0" cellpadding="0"><tr><td align="right">5.1 </td><td><a href="#%28part._.The_.Occurs_.Check%29" class="tocviewlink" data-pltdoc="x">The Occurs Check</a></td></tr></table></div></div></div><div class="tocsub"><div class="tocsubtitle">On this page:</div><table class="tocsublist" cellspacing="0"><tr><td><span class="tocsublinknumber">5.1<tt> </tt></span><a href="#%28part._.The_.Occurs_.Check%29" class="tocsubseclink" data-pltdoc="x">The Occurs Check</a></td></tr></table></div></div><div class="maincolumn"><div class="main"><div class="navsettop"><span class="navleft"><form class="searchform"><input class="searchbox" style="color: #888;" type="text" value="...search manuals..." title="Enter a search string to search the manuals" onkeypress="return DoSearchKey(event, this, "6.1", "../");" onfocus="this.style.color="black"; this.style.textAlign="left"; if (this.value == "...search manuals...") this.value="";" onblur="if (this.value.match(/^ *$/)) { this.style.color="#888"; this.style.textAlign="center"; this.value="...search manuals..."; }"/></form> <a href="../index.html" title="up to the documentation top" data-pltdoc="x" onclick="return GotoPLTRoot("6.1");">top</a></span><span class="navright"> <a href="backtracking.html" title="backward to "4 Backtracking"" data-pltdoc="x">← prev</a> <a href="index.html" title="up to "Racklog: Prolog-Style Logic Programming"" data-pltdoc="x">up</a> <a href="and-or.html" title="forward to "6 Conjuctions and Disjunctions"" data-pltdoc="x">next →</a></span> </div><h3 x-source-module="(lib "racklog/racklog.scrbl")" x-part-tag=""unification"">5<tt> </tt><a name="(part._unification)"></a>Unification</h3><p>When we say that a goal matches with a clause-head, we mean
that the predicate and argument positions line up. Before
making this comparison, Racklog dereferences all already
bound logic variables. The resulting structures are then
compared to see if they are recursively identical. Thus,
<span class="RktVal">1</span> unifies with <span class="RktVal">1</span>, and <span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="stt"> </span><span class="RktVal">1</span><span class="stt"> </span><span class="RktVal">2</span><span class="RktPn">)</span> with <span class="RktVal">'</span><span class="RktVal">(</span><span class="RktVal">1</span><span class="stt"> </span><span class="RktVal">2</span><span class="RktVal">)</span>; but <span class="RktVal">1</span> and
<span class="RktVal">2</span> do not unify, and neither do <span class="RktVal">'</span><span class="RktVal">(</span><span class="RktVal">1</span><span class="stt"> </span><span class="RktVal">2</span><span class="RktVal">)</span> and <span class="RktVal">'</span><span class="RktVal">(</span><span class="RktVal">1</span><span class="stt"> </span><span class="RktVal">3</span><span class="RktVal">)</span>.</p><p>In general, there could be quite a few uninstantiated logic
variables in the compared objects. Unification will then
endeavor to find the most natural way of binding these
variables so that we arrive at structurally identical
objects. Thus, <span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="stt"> </span><span class="RktVar">x</span><span class="stt"> </span><span class="RktVal">1</span><span class="RktPn">)</span>, where <span class="RktVar">x</span> is an unbound logic
variable, unifies with <span class="RktVal">'</span><span class="RktVal">(</span><span class="RktVal">0</span><span class="stt"> </span><span class="RktVal">1</span><span class="RktVal">)</span>, producing the
binding
<span class="RktPn">[</span><span class="RktVar">x</span><span class="stt"> </span><span class="RktVal">0</span><span class="RktPn">]</span>.</p><p>Unification is thus a goal, and Racklog makes the unification predicate
available to the user as <span class="RktSym"><a href="glossary.html#%28def._%28%28lib._racklog%2Fmain..rkt%29._~25~3d%29%29" class="RktValLink" data-pltdoc="x">%=</a></span>. Eg,</p><blockquote class="SCodeFlow"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="stt">> </span><span class="RktPn">(</span><span class="RktSym"><a href="glossary.html#%28form._%28%28lib._racklog%2Fmain..rkt%29._~25which%29%29" class="RktStxLink" data-pltdoc="x">%which</a></span><span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym">x</span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace"> </span><span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym"><a href="glossary.html#%28def._%28%28lib._racklog%2Fmain..rkt%29._~25~3d%29%29" class="RktValLink" data-pltdoc="x">%=</a></span><span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace"> </span><span class="RktSym">x</span><span class="hspace"> </span><span class="RktVal">1</span><span class="RktPn">)</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">(</span><span class="RktVal">0</span><span class="hspace"> </span><span class="RktVal">1</span><span class="RktVal">)</span><span class="RktPn">)</span><span class="RktPn">)</span></td></tr></table></td></tr><tr><td><p><span class="RktRes">'((x . 0))</span></p></td></tr></table></blockquote><p>Racklog also provides the predicate <span class="RktSym"><a href="glossary.html#%28def._%28%28lib._racklog%2Fmain..rkt%29._~25%2F~3d%29%29" class="RktValLink" data-pltdoc="x">%/=</a></span>, the <span style="font-style: italic">negation</span> of
<span class="RktSym"><a href="glossary.html#%28def._%28%28lib._racklog%2Fmain..rkt%29._~25~3d%29%29" class="RktValLink" data-pltdoc="x">%=</a></span>. <span class="RktPn">(</span><span class="RktSym"><a href="glossary.html#%28def._%28%28lib._racklog%2Fmain..rkt%29._~25%2F~3d%29%29" class="RktValLink" data-pltdoc="x">%/=</a></span><span class="stt"> </span><span class="RktVar">X</span><span class="stt"> </span><span class="RktVar">Y</span><span class="RktPn">)</span> succeeds if and only if <span class="RktVar">X</span> does
<span style="font-style: italic">not</span> unify with <span class="RktVar">Y</span>.</p><p>Unification goals constitute the basic subgoals that all
Racklog goals devolve to. A goal succeeds because all the
eventual unification subgoals that it decomposes to in at
least one of its subgoal-branching succeeded. It fails
because every possible subgoal-branching was thwarted by the
failure of a crucial unification subgoal.</p><p>Going back to the example in <a href="backtracking.html" data-pltdoc="x">Backtracking</a>, the goal
<span class="RktPn">(</span><span class="RktSym">%computer-literate</span><span class="stt"> </span><span class="RktVal">'</span><span class="RktVal">Penelope</span><span class="RktPn">)</span> succeeds because
(a) it unified with
<span class="RktPn">(</span><span class="RktSym">%computer-literate</span><span class="stt"> </span><span class="RktSym">person</span><span class="RktPn">)</span>; and then (b) with the binding
<span class="RktPn">[</span><span class="RktSym">person</span><span class="stt"> </span><span class="RktPn">. </span><span class="RktSym">Penelope</span><span class="RktPn">]</span> in place, <span class="RktPn">(</span><span class="RktSym">%knows</span><span class="stt"> </span><span class="RktSym">person</span><span class="stt"> </span><span class="RktVal">'</span><span class="RktVal">TeX</span><span class="RktPn">)</span>
unified with <span class="RktPn">(</span><span class="RktSym">%knows</span><span class="stt"> </span><span class="RktVal">'</span><span class="RktVal">Penelope</span><span class="stt"> </span><span class="RktVal">'</span><span class="RktVal">TeX</span><span class="RktPn">)</span> and
<span class="RktPn">(</span><span class="RktSym">%knows</span><span class="stt"> </span><span class="RktSym">person</span><span class="stt"> </span><span class="RktVal">'</span><span class="RktVal">Prolog</span><span class="RktPn">)</span> unified with <span class="RktPn">(</span><span class="RktSym">%knows</span><span class="stt"> </span><span class="RktVal">'</span><span class="RktVal">Penelope</span><span class="stt"> </span><span class="RktVal">'</span><span class="RktVal">Prolog</span><span class="RktPn">)</span>.</p><p>In contrast, the goal <span class="RktPn">(</span><span class="RktSym">%computer-literate</span><span class="stt"> </span><span class="RktVal">'</span><span class="RktVal">Telemachus</span><span class="RktPn">)</span>
fails because, with <span class="RktPn">[</span><span class="RktSym">person</span><span class="stt"> </span><span class="RktPn">. </span><span class="RktSym">Telemachus</span><span class="RktPn">]</span>,
the subgoals <span class="RktPn">(</span><span class="RktSym">%knows</span><span class="stt"> </span><span class="RktSym">person</span><span class="stt"> </span><span class="RktVal">'</span><span class="RktVal">Racket</span><span class="RktPn">)</span> and
<span class="RktPn">(</span><span class="RktSym">%knows</span><span class="stt"> </span><span class="RktSym">person</span><span class="stt"> </span><span class="RktVal">'</span><span class="RktVal">Prolog</span><span class="RktPn">)</span> have no facts they can
unify with.</p><h4 x-source-module="(lib "racklog/racklog.scrbl")" x-part-tag=""The_Occurs_Check"">5.1<tt> </tt><a name="(part._.The_.Occurs_.Check)"></a>The Occurs Check</h4><p>A robust unification algorithm uses the <a name="(tech._occurs._check)"></a><span style="font-style: italic">occurs check</span>, which ensures that a logic variable
isn’t bound to a structure that contains itself.
Not performing the check can cause the unification
to go into an infinite loop in some cases. On the
other hand, performing the occurs check greatly
increases the time taken by unification, even in cases
that wouldn’t require the check.</p><p>Racklog uses the global parameter
<span class="RktSym"><a href="glossary.html#%28def._%28%28lib._racklog%2Fmain..rkt%29._use-occurs-check~3f%29%29" class="RktValLink" data-pltdoc="x">use-occurs-check?</a></span> to decide whether to
use the occurs check. By default, this variable is
<span class="RktVal">#f</span>, ie, Racklog disables the occurs check. To
enable the check,</p><blockquote class="SCodeFlow"><p><span class="RktPn">(</span><span class="RktSym"><a href="glossary.html#%28def._%28%28lib._racklog%2Fmain..rkt%29._use-occurs-check~3f%29%29" class="RktValLink" data-pltdoc="x">use-occurs-check?</a></span><span class="hspace"> </span><span class="RktVal">#t</span><span class="RktPn">)</span></p></blockquote><div class="navsetbottom"><span class="navleft"><form class="searchform"><input class="searchbox" style="color: #888;" type="text" value="...search manuals..." title="Enter a search string to search the manuals" onkeypress="return DoSearchKey(event, this, "6.1", "../");" onfocus="this.style.color="black"; this.style.textAlign="left"; if (this.value == "...search manuals...") this.value="";" onblur="if (this.value.match(/^ *$/)) { this.style.color="#888"; this.style.textAlign="center"; this.value="...search manuals..."; }"/></form> <a href="../index.html" title="up to the documentation top" data-pltdoc="x" onclick="return GotoPLTRoot("6.1");">top</a></span><span class="navright"> <a href="backtracking.html" title="backward to "4 Backtracking"" data-pltdoc="x">← prev</a> <a href="index.html" title="up to "Racklog: Prolog-Style Logic Programming"" data-pltdoc="x">up</a> <a href="and-or.html" title="forward to "6 Conjuctions and Disjunctions"" data-pltdoc="x">next →</a></span> </div></div></div><div id="contextindicator"> </div></body></html>
|