1 <html> 2 <head> 3 <title>CL Unification: Standard Generic Function UNIFY</title> 4 <link rel="stylesheet" href="main.css"> 5 </head> 6 7 <body marginheight="0" marginwidth="0" leftmargin="0" topmargin="0" bgcolor="#ffffff"> 8 9 <table border="0" cellpadding="0" cellspacing="0" width="100%" height="100%" vspace="0" hspace="0"> 10 <tr> 11 <td colspan="3"> 12 <div class="header" 13 style="font-family:=Verdana,Arial,Helvetica; font-size: 18px; color: #41286f;"> 14 <strong><i>CL Unification: Standard Generic Function UNIFY</title></i></strong> 15 <div class="navigation"> 16 <a href="index.html" class="navigation-link">Home</a> 17 | <a href="unification-package.html" class="navigation-link">Previous</a> 18 | <a href="index.html" class="navigation-link">Next</a> 19 | <a href="downloads.html" class="navigation-link">Downloads</a> 20 | <a href="links.html" class="navigation-link">Links</a> 21 </div> 22 </div> 23 <div class="black-line"><img src="images/shim.gif" height="1" width="1"></div> 24 <div class="middle-bar"><img src="images/shim.gif" height="5" width="1"></div> 25 <div class="black-line"><img src="images/shim.gif" height="1" width="1"></div> 26 </td> 27 </tr> 28 29 <tr height="100%"> 30 <td height="100%"> </td> 31 <td valign="top" width="80%" height="100%"> 32 33 <div class="content"> 34 <div class="text" style="padding-top: 10px;"> 35 36 <h1><i>Generic function</i> <strong>UNIFY</strong></h1> 37 38 <h2>Package:</h2> 39 40 <p><code>COMMON-LISP.EXTENSIONS.DATA-AND-CONTROL-FLOW.UNIFICATION</code></p> 41 42 43 <h2>Syntax:</h2> 44 45 <p> 46 <pre> 47 <b>unify</b> <i>object1</i> <i>object2</i> &optional <i>substitution</i> 48 => <i>substitution</i> 49 </pre> 50 </p> 51 52 <h3>Arguments and Values:</h3> 53 54 <p><i><code>object1</code></i>---an <i>object</i> 55 <p><i><code>object2</code></i>---an <i>object</i> 56 <p><i><code>substitution</code></i>---a <i>substitution</i> 57 58 59 60 61 <h2>Description:</h2> 62 63 <p>The generic function UNIFY is the entry point in the unification 64 machinery. It takes two <strong>CL</strong> objects, <i>object1</i> 65 and <i>object2</i> and checks whether they can be <em>unified</em> 66 by constructing a (possibly empty) consistent substitution assigning 67 appropriate values to the <em>unification variables</em> appearing 68 each object. The rules by which the unification process is carried 69 on are dependent on the types of the two objects. The known rules 70 are described in the <a href="#known_methods">"known methods"</a> 71 section.</p> 72 73 <p>UNIFY takes a <em>substitution</em> as an optional argument. The 74 default value is a <em>fresh</em> empty substitution obtained by 75 calling MAKE-EMPTY-ENVIRONMENT.</p> 76 77 <h3><a name="known_methods">Known Methods</a>:</h3> 78 79 <p>Note that UNIFY is commutative in its two required arguments. Each 80 method listed exists also with <i>object1</i> and <i>object2</i> 81 reversed.</p> 82 83 <p>First, the methods defined on standard <strong>CL</strong> types 84 are described, and then all the methods involving <em>unification 85 templates</em> are described.</p> 86 87 88 <p> 89 <ul> 90 <li> 91 <p> 92 <pre> 93 <b>unify</b> (<i>s1</i> symbol) (<i>s2</i> symbol) &optional <i>substitution</i> 94 => <i>substitution</i> 95 </pre> 96 </p> 97 98 <p>The unification of two symbols depends on whether one (or both) 99 of them is a unification variable (i.e. either the symbol with name 100 <code>"_"</code>, or a symbol with name starting with the character 101 <code>#\?</code>.)</p> 102 103 <p>If neither object is an unification variable, then UNIFY succeds 104 if and only if the two symbols <i>s1</i> and <i>s2</i> are EQ.</p> 105 106 <p>If <i>s1</i> is an unification variable, and either <i>s1</i> is not 107 bound in <i>substitution</i>, or <i>s1</i> is bound to <i>s2</i> 108 then UNIFY succeds. If <i>s1</i> was not bound in the 109 <i>substitution</i>, then a new binding for <i>s1</i> to <i>s2</i> 110 is created.</p> 111 112 <p>The symmetric case holds if <i>s1</i> is not an unification 113 variable but <i>s2</i> is.</p> 114 115 <p>Otherwise an error of type UNIFICATION-FAILURE is signaled.</p> 116 </li> 117 118 <li> 119 <p> 120 <pre> 121 <b>unify</b> (<i>v</i> symbol) (<i>object</i> t) &optional <i>substitution</i> 122 => <i>substitution</i> 123 </pre> 124 </p> 125 126 <p>The symbol <i>v</i> must be an unification variable. If not, an 127 error of type UNIFICATION-FAILURE will be signaled. 128 Otherwise, the a new binding for the variable <i>v</i> with value 129 <i>object</i> will be created in the <i>substitution</i>.<p> 130 131 <p>The creation of the new binding for <i>v</i> in the 132 <i>substitution</i> is dependent on the <em>occur check</em> 133 implemented by the generic function OCCURS-IN-P. OCCURS-IN-P is 134 called by the unification machinery if the variable 135 *OCCURRENCE-CHECK-P* is non-NIL (the default.) If 136 *OCCURENCE-CHECK-P* is non-NIL, and if the variable 137 <i>v</i> <em>occurs</em> in the <i>object</i> (i.e. OCCURS-IN-P 138 returns a non-NIL value,) then an error of type UNIFICATION-FAILURE 139 is signaled.</p> 140 </li> 141 142 143 <li> 144 <p> 145 <pre> 146 <b>unify</b> (<i>n1</i> number) (<i>n2</i> number) &optional <i>substitution</i> 147 => <i>substitution</i> 148 </pre> 149 </p> 150 151 <p>Two numbers unify if and only if they are =, in which case 152 <i>substitution</i> is returned unmodified. Otherwise, an error of 153 type UNIFICATION-FAILURE is signaled.</p> 154 </li> 155 156 157 <li> 158 <p> 159 <pre> 160 <b>unify</b> (<i>s1</i> string) (<i>s2</i> string) &optional <i>substitution</i> 161 => <i>substitution</i> 162 </pre> 163 </p> 164 165 <p>Two strings unify only is they are "equal", under the following 166 condition. If the variable *UNIFY-STRING-CASE-SENSITIVE-P* is T 167 (the default) then the two strings <i>s1</i> and <i>s2</i> are 168 compared using STRING=, otherwise they are compared using STRING-EQUAL. 169 </p> 170 171 <p>If the two strings <i>s1</i> and <i>s2</i> are equal then 172 <i>substitution</i> is returned unchanged, otherwise an error of type 173 UNIFICATION-FAILURE is signaled.</p> 174 </li> 175 176 <li> 177 <p> 178 <pre> 179 <b>unify</b> (<i>v1</i> vector) (<i>v2</i> vector) &optional <i>substitution</i> 180 => <i>substitution</i> 181 </pre> 182 </p> 183 184 <p> 185 <pre> 186 <b>unify</b> (<i>l1</i> list) (<i>l2</i> list) &optional <i>substitution</i> 187 => <i>substitution</i> 188 </pre> 189 </p> 190 191 <p> 192 <pre> 193 <b>unify</b> (<i>s1</i> sequence) (<i>s2</i> sequence) &optional <i>substitution</i> 194 => <i>substitution</i> 195 </pre> 196 </p> 197 198 <p>The "sequence" methods (and the specialized ones, mostly for 199 efficiency) extend the <i>substitution</i> by calling UNIFY 200 recursively on each element of the two sequences, <i>s1</i> and 201 <i>s2</i> (respectively, <i>l1</i> and <i>l2</i>, <i>v1</i> and 202 <i>v2</i>.) 203 </p> 204 205 <p>An error of type UNIFICATION-FAILURE is signaled if the two 206 sequences are of different LENGTH or if any call to 207 UNIFY fails.</p> 208 </li> 209 210 211 <li> 212 <p> 213 <pre> 214 <b>unify</b> (<i>a1</i> array) (<i>a2</i> array) &optional <i>substitution</i> 215 => <i>substitution</i> 216 </pre> 217 </p> 218 219 <p>Two arrays <i>a1</i> and <i>a2</i> UNIFY if and only if each of 220 the respective elements does. The two arrays are traversed using 221 ROW-MAJOR-AREF. Otherwise an error of type UNIFICATION-FAILURE is 222 signaled.</p> 223 224 <p>An error of type UNIFICATION-FAILURE is also signaled if the two 225 arrays have different total size (as returned by ARRAY-TOTAL-SIZE.)</p> 226 </li> 227 228 229 <li> 230 <p> 231 <pre> 232 <b>unify</b> (<i>object1</i> t) (<i>object2</i> t) &optional <i>substitution</i> 233 => <i>substitution</i> 234 </pre> 235 </p> 236 237 <p>This is the catch all method that is called as a last resort. 238 No recursive call to UNIFY is attempted, and the call succeeds if and 239 only if <i>object1</i> and <i>object2</i> are EQUALP. Otherwise, an 240 error of type UNIFICATION-FAILURE is signaled.</p> 241 </li> 242 243 </ul> 244 </p> 245 246 <p>The next methods all involve a <em>unification template</em>. 247 Again all these methods are commutative in their required 248 arguments.</p> 249 250 <p> 251 <ul> 252 <li> 253 <p> 254 <pre> 255 <b>unify</b> (<i>s</i> structure-object) (<i>st</i> structure-object-template) &optional <i>substitution</i> 256 => <i>substitution</i> 257 </pre> 258 </p> 259 260 <p>This method UNIFYs a <i>s</i> against a STRUCTURE-OBJECT-TEMPLATE 261 <i>st</i>. <i>st</i> has the following (general) structure.</p> 262 <pre> 263 (<i><structure-class specifier></i> [ (<i><reader></i> <i><value></i>) ]* ) 264 </pre></p> 265 266 <p>The <i>structure-class specifier</i> is a symbol naming a 267 structure class, <i>reader</i> is one of the DEFSTRUCT-generated 268 accessors, and <i>value</i> is a regular <strong>CL</strong> object, 269 a unification variable, or a <em>unification template</em>.</p> 270 271 <p>The class of <i>s</i> must be a subclass of <i>structure-class 272 specifier</i>. Otherwise, an 273 error of type UNIFICATION-FAILURE is signaled.</p> 274 275 <p>UNIFY 276 is called recursively on each <i>value</i> and the result of 277 applying <i>reader</i> to <i>s</i>.</p> 278 279 <p>If all the (recursive) calls to UNIFY succeed, then a possibly 280 augmented <i>substitution</i> is returned. Otherwise, an 281 error of type UNIFICATION-FAILURE is signaled.</p> 282 </li> 283 284 285 <li> 286 <p> 287 <pre> 288 <b>unify</b> (<i>s</i> standard-object) (<i>st</i> standard-object-template) &optional <i>substitution</i> 289 => <i>substitution</i> 290 </pre> 291 </p> 292 293 <p>This method UNIFYs a <i>s</i> against a STANDARD-OBJECT-TEMPLATE 294 <i>st</i>. <i>st</i> has the following (general) structure.</p> 295 <pre> 296 (<i><standard-class specifier></i> [ ([slot-value | slot-accessor] <i><slot-spec></i> <i><value></i>) ]* ) 297 </pre></p> 298 299 <p>The <i>standard-class specifier</i> is a symbol naming a 300 class, <i>slot-spec</i> is a valid slot accessor when 301 <code>slot-value</code> is specified, or a valid slot name for the 302 class, when <code>slot-value</code> is specified, and <i>value</i> 303 is a regular <strong>CL</strong> object, 304 a unification variable, or a <em>unification template</em>.</p> 305 306 <p>The class of <i>s</i> must be a subclass of <i>standard-class 307 specifier</i>. Otherwise, an 308 error of type UNIFICATION-FAILURE is signaled.</p> 309 310 <p>UNIFY 311 is called recursively on each <i>value</i> and the result of 312 extracting the slot value from <i>s</i> using either the accessor 313 supplied, or SLOT-VALUE.</p> 314 315 <p>If all the (recursive) calls to UNIFY succeed, then a possibly 316 augmented <i>substitution</i> is returned. Otherwise, an 317 error of type UNIFICATION-FAILURE is signaled.</p> 318 </li> 319 320 </ul> 321 </p> 322 323 324 <h2>Affected By:</h2> 325 326 <p>None.</p> 327 328 329 <h2>Exceptional Situations:</h2> 330 331 <p>If <i>object1</i> and <i>object2</i> cannot be unified, then an 332 error of type UNIFICATION-FAILURE is signaled.</p> 333 334 335 <h2>See Also:</h2> 336 337 <p>MAKE-EMPTY-ENVIRONMENT, UNIFICATION-FAILURE, 338 *UNIFY-STRING-CASE-SENSITIVE-P*, OCCURS-IN-P, 339 *OCCURENCE-CHECK-P*.</p> 340 341 <h2>Notes:</h2> 342 343 <p>The unification algorithm implemented is very flexible and 344 provides many hooks for customization. However, it is not 345 necessarily asymptotically efficient (it has a worst case 346 exponential time complexity.)</p> 347 348 <p>It would be interesting to reimplement the kernel of the system 349 using a linear unification algorithm like the one described in<p> 350 351 <p>[MM82] A. Martelli and U. Montanari, <i>An Efficient Unification 352 Algorithm</i>, ACM Transactions on Programming Languages and 353 Systems, Vol. 4, No. 2, April 1982, Pages 258--282.</p> 354 355 </td> 356 357 <!-- <td height="100%"> </td> --> 358 </tr> 359 360 <tr height="100%"> 361 <td height="100%"> </td> 362 <td valign="top" width="80%" height="100%"> 363 364 <div class="content"> 365 <div class="text" style="padding-top: 10px;"> 366 367 <h1>News</h1> 368 369 <p>News in chronological order, most recent on top. 370 </p> 371 372 <ul> 373 <li><strong>2004-04-12</strong><br> 374 Completed description. 375 </li> 376 377 </ul> 378 379 </div> 380 </div> 381 382 </td> 383 384 <td height="100%"> </td> 385 </tr> 386 387 388 389 390 <tr> 391 <td colspan="3" valign="bottom" align="right"> 392 <div class="copyright"> 393 © 2003-2004, Marco Antoniotti, all rights reserved. 394 </div> 395 </td> 396 </tr> 397 398 </table> 399 </body> 400 </html>