repos
/
cl-unification
/ annotate_shade
summary
|
shortlog
|
log
|
tree
|
commit
|
commitdiff
|
headdiff
|
annotate
|
headblob
|
headfilediff
|
filehistory
normal
|
plain
|
shade
|
zebra
Use *unify-string-case-sensitive-p* consistently.
Annotate for file docs/html/unify-function.html
2004-11-17 mantoniotti
1
<html>
22:19:54 '
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
2011-04-02 rbrown
166
condition. If the variable *UNIFY-STRING-CASE-SENSITIVE-P* is T
2004-11-17 mantoniotti
167
(the default) then the two strings <i>s1</i> and <i>s2</i> are
22:19:54 '
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,
2011-04-02 rbrown
338
*UNIFY-STRING-CASE-SENSITIVE-P*, OCCURS-IN-P,
2004-11-17 mantoniotti
339
*OCCURENCE-CHECK-P*.</p>
22:19:54 '
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>