repos
/
cl-unification
/ annotate_shade
summary
|
shortlog
|
log
|
tree
|
commit
|
commitdiff
|
headdiff
|
annotate
|
headblob
|
headfilediff
|
filehistory
normal
|
plain
|
shade
|
zebra
Copyright updated.
Annotate for file /docs/html/index.html
2004-11-17 mantoniotti
1
<html>
22:19:54 '
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>
2005-05-20 mantoniotti
18
| <a href="mailing-lists.html" class="navigation-link">Mailing Lists</a>
15:47:44 '
19
| <a href="links.html" class="navigation-link">Links</a>
2004-11-17 mantoniotti
20
</div>
22:19:54 '
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>
2007-11-09 mantoniotti
289
13:56:40 '
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
2004-11-17 mantoniotti
308
22:19:54 '
309
'
310
<!--
2011-04-02 mantoniotti
311
;;; Copyright (c) 2004-2011 Marco Antoniotti, All rigths reserved.
2004-11-17 mantoniotti
312
;;;
22:19:54 '
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>
2011-04-02 mantoniotti
352
<li><strong>2011-02-20</strong><br>
04:11:54 '
353
CL-UNIFICATION is now in <a href="www.quicklisp.org">Quicklisp</a>.
2007-11-09 mantoniotti
354
<li><strong>2007-11-09</strong><br>
13:56:40 '
355
Updated.
2004-11-17 mantoniotti
356
<li><strong>2004-11-04</strong><br>
22:19:54 '
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">
2012-03-13 mantoniotti
377
© 2004-2012, Marco Antoniotti, all rights reserved.
2004-11-17 mantoniotti
378
</div>
22:19:54 '
379
</td>
'
380
</tr>
'
381
'
382
</table>
'
383
</body>
'
384
</html>