1 <html> 2 <head> 3 <title>CL Unification</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 Extensions: UNIFICATION</i><string> 15 <div class="navigation"> 16 <a href="index.html" class="navigation-link-selected">Home</a> 17 | <a href="downloads.html" class="navigation-link">Downloads</a> 18 | <a href="mailing-lists.html" class="navigation-link">Mailing Lists</a> 19 | <a href="links.html" class="navigation-link">Links</a> 20 </div> 21 </div> 22 <div class="black-line"><img src="images/shim.gif" height="1" width="1"></div> 23 <div class="middle-bar"><img src="images/shim.gif" height="5" width="1"></div> 24 <div class="black-line"><img src="images/shim.gif" height="1" width="1"></div> 25 </td> 26 </tr> 27 28 <tr height="100%"> 29 <td height="100%"> <div class="sidebar"></div></td> 30 <td valign="top" width="80%" height="100%"> 31 32 <div class="content"> 33 <div class="text" style="padding-top: 10px;"> 34 35 <h1>Common Lisp Extensions: UNIFICATION</h1> 36 37 <p>The notion of <em>unification</em> originated in the field of 38 formal logic (e.g. <a href="#R65">[R65]</a>,) and has been used 39 extensively in Computer Science and Programming Languages. Most 40 notably, <strong>Prolog</strong> uses the full power of 41 unification.</p> 42 43 <p> 44 Unification is also at the core of <em>type checking</em> algorithms 45 in the tradition of Milner's, and a limited form - <em>pattern 46 matching</em> - is available to the user in languages of the ML and 47 Haskell family.</p> 48 49 <p>The library presented in these pages provides a full blown 50 <em>unification framework</em> for <strong>Common Lisp</strong>.</p> 51 52 <p>Writing a pattern matcher or a an unifier in <strong>Common 53 Lisp</strong> is easy, as long as we limit ourselves to manipulate 54 only ATOMs and CONSes.</p> 55 56 <p>Alas, it would be much nicer if we could manipulate arbitrary 57 <strong>Common Lisp</strong> objects as the ML programmer can with 58 arbitrary ML objects.<p> 59 60 <p>The library presented here is the first one (to the best of the 61 author's knowledge) that is capable of manipulating arbitrary 62 <strong>Common Lisp</strong> objects.</p> 63 64 <p>The hope is that this library could be incorporated directly in 65 an implementation in order to provide better type checking.</p> 66 67 <p>This should not come as a surprise, as a compiler like CMUCL does 68 include a type inference engine, which does very similar things.</p> 69 70 <h2>Unification Basics</h2> 71 72 <p>The unification process makes sure that two <em>object 73 descriptions</em> containing some <em>holes</em> 74 - i.e. <em>variables</em> - can be made equal (almost in the EQUALP 75 sense) by assigning <em>consistent</em> values to the variables 76 involved.</p> 77 78 <p>Suppose we had a function U performing unification and returning 79 a set of <em>variable assignments</em>, often called a 80 <em>substitution</em>. A very simple 81 example involving the unification of two numbers could be 82 <pre> 83 <b>U</b>(42, 42) ==> {} 84 </pre> 85 The two numbers are EQL, so no variable is involved and the empty 86 substitution is returned. 87 <pre> 88 <b>U</b>(42, 123) ==> <unification failure> 89 </pre> 90 The two numbers are not EQL, so the unification fails. 91 <pre> 92 <b>U</b>(42, x) ==> {x -> 42} 93 </pre> 94 The only way to make the unification process to succeed is to bind 95 the value 42 to the variable <code>x</code>.</p> 96 97 <p>The UNIFICATION library defines all the necessary functions and a 98 <em>unification sub-language</em> to handle most of <strong>Common 99 Lisp</strong>.</p> 100 101 <h2>UNIFICATION Library</h2> 102 103 <p>The UNIFICATION library has one main entry point, the generic function 104 UNIFY, and a sub-language definition that allows us to talk about 105 <strong>Common Lisp</strong> objects.</p> 106 107 <p>The UNIFY generic function has the following signature: 108 <pre> 109 <b>unify</b> <i>x</i> <i>y</i> &optional <i>substitution</i> 110 </pre> 111 Where <code><i>x</i></code> and <code><i>y</i></code> are either 112 arbitrary <strong>Common Lisp</strong> objects, <em>variables</em>, 113 or <em>object templates</em>. These items constitute the so-called 114 <em>extended terms</em> manipulated by the unification 115 machinery.</p> 116 117 <p><em>Variables</em> are symbols with a <code>#\?</code> as the 118 first character of the name. This is a rather traditional choice, 119 although a different one based on quoted symbols is possible. 120 Therefore, the following are examples of variables. 121 <pre> 122 ?A ?s ?qwe ?42z ?a-variable-with-a-very-long-name ?_ 123 </pre> 124 There are two special variables, <code>?_</code> and <code>_</code>, 125 which are used as anonymous place holders, they match anything, but 126 never appear in a substitution.</p> 127 128 <p>Hence, the above examples result in the following 129 <pre> 130 cl-prompt> (<b>unify</b> 42 42) 131 <i>#<EMPTY ENVIRONMENT xxxxxx></i> 132 </pre> 133 134 <pre> 135 cl-prompt> (<b>unify</b> 42 123) 136 ==> error: unification failure 137 </pre> 138 139 <pre> 140 cl-prompt> (<b>unify</b> 42 ?x) 141 <i>#<ENVIRONMENT xxxxxx></i> 142 143 cl-prompt> (<b>find-variable-value</b> '?x *) 144 <i>42</i> 145 </pre> 146 </p> 147 Where FIND-VARIABLE-VALUE is the accessor used to find the value of 148 a variable in a substitution.</p> 149 150 <p>As a more complicated example, consider the usual CONS based 151 unification 152 <pre> 153 cl-prompt> (<b>unify</b> '(foo (bar frobboz) ?baz) '(foo ?gnao 42)) 154 <i>#<ENVIRONMENT xxxxxx></i> 155 156 cl-prompt> (<b>find-variable-value</b> '?gnao *) 157 <i>(BAR FROBBOZ)</i> 158 159 cl-prompt> (<b>find-variable-value</b> '?baz **) 160 <i>42</i> 161 </pre> 162 163 <p>Of course note the following behavior 164 <pre> 165 cl-prompt> (<b>unify</b> '(foo ?x 42) '(foo 42 ?x)) 166 <i>#<ENVIRONMENT xxxxxx></i> 167 168 cl-prompt> (<b>unify</b> '(foo ?x 42) '(foo baz ?x)) 169 ==> error: unification failure 170 </pre> 171 </p> 172 173 174 <p>UNIFY works also on arrays and vectors. Strings are treated as 175 atomic objects 176 <pre> 177 cl-prompt> (<b>unify</b> #(1 2 3) #(1 ?x ?y)) 178 <i>#<ENVIRONMENT xxxxxx></i> 179 180 cl-prompt> (<b>find-variable-value</b> '?x *) 181 <i>2</i> 182 </pre> 183 184 <pre> 185 cl-prompt> (<b>unify</b> #2A((1 2 3) (a s ?z)) #2A((1 ?x ?y) (a s d))) 186 <i>#<ENVIRONMENT xxxxxx></i> 187 188 cl-prompt> (<b>find-variable-value</b> '?z *) 189 <i>D</i> 190 </pre> 191 </p> 192 193 <p>So far so good, but how can you unify two structures? First of 194 all there is no portable way (yet) to list all the slots of a given 195 structure. Secondly, by allowing the unification of arbitrary 196 CONSes, we have created a short-circuit in the unification 197 machinery.</p> 198 199 <p>Dealing with object instances raises similar problems.</p> 200 201 <p>Suppose we have the following definition 202 <pre> 203 (defstruct foo a s d) 204 </pre> 205 The straightforward 206 <pre> 207 (<b>unify</b> #S(FOO A 42 S NIL D NIL) (make-foo :a 42)) 208 </pre> 209 cannot be built portably, besides, we do not even have the equivalent of the 210 <code>#S(...)</code> notation for regular CLOS objects. Moreover we want 211 to do other things with other data types.</p> 212 213 <p>A simple solution is to define a <em>template sub-language</em> 214 to express unifications between structure objects or standard 215 objects (and other data types as well.) Nevertheless, the 216 definition of such sub-language cannot be CONS based, because in 217 such case, we would conflate arbitrary CONSes and the expressions of 218 the sub-language.</p> 219 220 <p>To circumvent this problem we resort to the usual trick a ML 221 programmer uses to placate the type-checker: we introduce an 222 "intermediate" data type. Essentially the following 223 <pre> 224 (defclass <b>template</b> () 225 ((spec :accessor template-spec :type (or cons symbol number) ...))) 226 </pre> 227 </p> 228 229 <p>The TEMPLATE class is accompanied by a reader macro 230 (<code>#T</code> for <em>template</em>, or <em>type</em>, with an 231 abuse of language) and an 232 appropriate PRINT-OBJECT method. The <code>#T</code> reader macro 233 expands as 234 <pre> 235 <b>#T</b><i>something</i> ==> (make-instance 'template :spec <i>something</i>) 236 </pre> 237 With this infrastructure we can 238 express the unification of the FOO instance as 239 <pre> 240 (<b>unify</b> #S(FOO A 42 S NIL D NIL) <b>#T(foo foo-a 42)</b>) 241 </pre> 242 I.e. we use the actual structure accessor FOO-A to get to the the 243 value of the slot A in a FOO. This is an example of the template 244 language.</p> 245 246 <p>A more interesting example, which involves vectors is the 247 following 248 <pre> 249 cl-prompt> (<b>unify</b> #(1 2 3 4 5) <b>#T(vector 1 ?x &rest ?rest)</b>) ; You get the idea... 250 <i>#<ENVIRONMENT xxxxxxx></i> 251 252 cl-prompt> (<b>find-variable-value</b> '?rest *) 253 <i>#(3 4 5)</i> 254 </pre> 255 I.e. we have a DESTRUCTURING-BIND on steroids.<p> 256 257 <p>Note that separating the templates is necessary if we want to do 258 something like 259 <pre> 260 cl-prompt> (<b>unify</b> '(1 2 3 4 5) <b>#T(list 1 ?x &rest ?rest)</b>) 261 <i>#<ENVIRONMENT xxxxxxx></i> 262 263 cl-prompt> (<b>find-variable-value</b> '?rest *) 264 <i>(3 4 5)</i> 265 </pre> 266 Without the template denoted by <code>#T(list ...)</code> the 267 unifier would have been utterly confused.</p> 268 269 <p>In the following the full extent of the UNIFICATION facility is 270 described in its main components. 271 </p> 272 273 274 <h2><a href="unifying-substitutions.html">Unifying Substitutions</a></h2> 275 276 <h2><a href="templates.html">The Template Sub-language</a></h2> 277 278 <h2><a href="control-flow.html">Control Flow</a></h2> 279 280 <h2><a href="unification-dictionary.html">The UNIFICATION 281 Dictionary</a></h2> 282 283 <h2>References</h2> 284 285 <p> 286 <a name="R65">[R56]</a> J. A. Robinson, <i>A machine-oriented logic based on the 287 resolution principle</i>, Journal of the ACM, Vol. 12, No. 1, 288 January 1965, Pages 23--49.</p> 289 290 291 <h1></h1> 292 <hr> 293 <em> 294 <p> 295 <b>DISCLAIMER:</b> The code associated to these documents is not 296 completely tested and it is bound to contain errors and omissions. 297 This documentation may contain errors and omissions as well.</p> 298 299 <p>The file <tt>COPYING</tt> contains a Berkeley-style license. You 300 are advised to use the code at your own risk. No warranty 301 whatsoever is provided, the author will not be held responsible for 302 any effect generated by your use of the library, and you can put 303 here the scarier extra disclaimer you can think of. 304 </p> 305 </em> 306 <hr> 307 308 309 310 <!-- 311 ;;; Copyright (c) 2004-2011 Marco Antoniotti, All rigths reserved. 312 ;;; 313 ;;; Permission to use, modify, and redistribute this code is hereby 314 ;;; granted. 315 ;;; The code is provided AS IS with NO warranty whatsoever. The author 316 ;;; will not be held liable etc etc etc etc etc. 317 --> 318 319 <h2>Site Map</h2> 320 321 322 <p>Enjoy!</p> 323 324 325 326 <hr> 327 <p>Questions? Queries? Suggestions? Comments? Please direct them 328 at <a href="mailto:marcoxa_PROVA_A_SPAMMARME@alu.org">me</a>. 329 </p> 330 331 </div> 332 </div> 333 334 </td> 335 336 <!-- <td height="100%"> </td> --> 337 </tr> 338 339 <tr height="100%"> 340 <td height="100%"> </td> 341 <td valign="top" width="80%" height="100%"> 342 343 <div class="content"> 344 <div class="text" style="padding-top: 10px;"> 345 346 <h1>News</h1> 347 348 <p>News in chronological order, most recent on top. 349 </p> 350 351 <ul> 352 <li><strong>2011-02-20</strong><br> 353 CL-UNIFICATION is now in <a href="www.quicklisp.org">Quicklisp</a>. 354 <li><strong>2007-11-09</strong><br> 355 Updated. 356 <li><strong>2004-11-04</strong><br> 357 Updated. 358 <li><strong>2004-05-05</strong><br> 359 Started the site. 360 </li> 361 </ul> 362 363 </div> 364 </div> 365 366 </td> 367 368 <td height="100%"> </td> 369 </tr> 370 371 372 373 374 <tr> 375 <td colspan="3" valign="bottom" align="right"> 376 <div class="copyright"> 377 © 2004-2012, Marco Antoniotti, all rights reserved. 378 </div> 379 </td> 380 </tr> 381 382 </table> 383 </body> 384 </html>