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/dictionary.html
2004-11-17 mantoniotti
1
<html>
22:19:54 '
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
<!--
2011-04-02 mantoniotti
282
;;; Copyright (c) 2004-2011 Marco Antoniotti, All rigths reserved.
2004-11-17 mantoniotti
283
;;;
22:19:54 '
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
2011-04-02 mantoniotti
317
<!-- <h1>News</h1>
2004-11-17 mantoniotti
318
22:19:54 '
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>
2011-04-02 mantoniotti
327
-->
2004-11-17 mantoniotti
328
</div>
22:19:54 '
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">
2011-04-02 mantoniotti
342
© 2003-2011, Marco Antoniotti, all rights reserved.
2004-11-17 mantoniotti
343
</div>
22:19:54 '
344
</td>
'
345
</tr>
'
346
'
347
</table>
'
348
</body>
'
349
</html>