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