← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp
 
1
;;; unification.lisp 
 
2
;;; Definition of a particular rule-based unification algorithm.
 
3
;;; This is an executable instance of the general pattern verified in
 
4
;;; unification-pattern.lisp 
 
5
;;; Created 17-10-99. Last revision: 10-12-2000
 
6
;;; =================================================================
 
7
 
 
8
#| To certify this book:
 
9
 
 
10
(in-package "ACL2")
 
11
 
 
12
(certify-book "unification")
 
13
 
 
14
|#
 
15
 
 
16
 
 
17
 
 
18
 
 
19
 
 
20
(in-package "ACL2")
 
21
(include-book "subsumption-subst")
 
22
(local (include-book "unification-pattern"))
 
23
(set-well-founded-relation e0-ord-<)
 
24
 
 
25
 
 
26
;;; *************************************************
 
27
;;; A CONCRETE AND EXECUTABLE UNIFICATION ALGORITHM
 
28
;;; *************************************************
 
29
 
 
30
;;; Here we show how we can obtain a correct and executable unification
 
31
;;; algorithm from the "pattern"  verified in unification-definition.lisp:
 
32
;;; - We define a particular selection function. 
 
33
;;; - We introduce multi-values to deal with the pair of systems
 
34
;;;   S-sol and with the returned values, to improve efficiency.
 
35
;;; - Some other improvements concerning efficency are done.
 
36
;;; - Guards are verified, allowing execution in Common Lisp.
 
37
 
 
38
;;; ============================================================================
 
39
;;; 1. The unification algorithm
 
40
;;; ============================================================================
 
41
 
 
42
;;; ----------------------------------------------------------------------------
 
43
;;; 1.1 A particular version of transform-mm-sel
 
44
;;; ----------------------------------------------------------------------------
 
45
 
 
46
;;; ����������������������������������������������������������������������������
 
47
;;; 1.1.1 A particular "selection" function. If we detect an inmediate fail,
 
48
;;; we select it.
 
49
;;; ����������������������������������������������������������������������������
 
50
 
 
51
(defun sel-unif (S)
 
52
  (declare (xargs :guard (and (consp S) (system-p S))))
 
53
  (if (endp (cdr S))
 
54
      (car S)
 
55
    (let* ((equ (car S))
 
56
           (t1 (car equ))
 
57
           (t2 (cdr equ)))
 
58
        (cond ((or (variable-p t1) (variable-p t2)) 
 
59
               (sel-unif (cdr S)))
 
60
              ((eql (car t1) (car t2))
 
61
               (sel-unif (cdr S)))
 
62
              (t equ)))))
 
63
 
 
64
;;; Main property, needed to instantiate from unification-definition.lisp: 
 
65
(local
 
66
 (defthm sel-unif-select-a-pair
 
67
   (implies (consp S)
 
68
            (member (sel-unif S) S))))
 
69
 
 
70
 
 
71
 
 
72
;;; ����������������������������������������������������������������������������
 
73
;;; 1.1.2 Some lemmas needed for guard verification:
 
74
;;; ����������������������������������������������������������������������������
 
75
 
 
76
(encapsulate
 
77
 ()
 
78
 
 
79
 (local
 
80
  (defthm sel-unif-consp
 
81
    (implies (and (alistp S)
 
82
                  (consp S)
 
83
                  (system-p S))
 
84
             (consp (sel-unif S)))
 
85
    :rule-classes :type-prescription))
 
86
 
 
87
 (defthm termp-p-sel-unif-system-p
 
88
   (implies (and (consp S)
 
89
                 (system-p S))
 
90
            (and
 
91
             (term-p (car (sel-unif S)))
 
92
             (term-p (cdr (sel-unif S))))))
 
93
 
 
94
 (local
 
95
  (defthm term-p-true-listp-arguments
 
96
    (implies (and (term-p term) (not (variable-p term)))
 
97
             (true-listp (cdr term)))))
 
98
 
 
99
 (local
 
100
  (defthm system-p-eqlable-function-symbols
 
101
    (implies (and (system-p S)
 
102
                  (member equ S))
 
103
             (eqlablep (cadr equ)))))
 
104
 
 
105
 (defthm system-p-eqlablep-car
 
106
   (implies (and (system-p S)
 
107
                 (consp S)
 
108
                 (variable-p (car (sel-unif S))))
 
109
            (eqlablep (car (sel-unif S)))))
 
110
 
 
111
;;; ����������������������������������������������������������������������������
 
112
;;; 1.1.3 The function transform-mm
 
113
;;; ����������������������������������������������������������������������������
 
114
 
 
115
 
 
116
 (defun transform-mm (S sol)
 
117
   (declare (xargs :guard (and (system-p S)
 
118
                               (system-p sol)
 
119
                               (consp S))))
 
120
   (let* ((ecu (sel-unif S))
 
121
          (t1 (car ecu)) (t2 (cdr ecu))
 
122
          (R (eliminate ecu S)))
 
123
     (cond ((equal t1 t2) (mv R sol t))                  ;;; *DELETE*
 
124
           ((variable-p t1)
 
125
            (if (member t1 (variables t t2))
 
126
                (mv nil nil nil)                         ;;; *CHECK*
 
127
              (mv                                        ;;; *ELIMINATE*
 
128
               (substitute-syst t1 t2 R)
 
129
               (cons ecu
 
130
                     (substitute-range t1 t2 sol))
 
131
               t)))
 
132
           ((variable-p t2)
 
133
            (mv (cons (cons t2 t1) R) sol t))            ;;; *ORIENT*
 
134
           ((not (eql (car t1) (car t2)))
 
135
            (mv nil nil nil))                            ;;; *CONFLICT*
 
136
           (t (mv-let (pairs bool) 
 
137
                      (pair-args (cdr t1) (cdr t2))
 
138
                      (if bool
 
139
                          (mv (append pairs R) sol t)    ;;; *DESCOMPOSE*
 
140
                        (mv nil nil nil))))))))           ;;; *NOT-PAIR*
 
141
 
 
142
 
 
143
 
 
144
;;; ----------------------------------------------------------------------------
 
145
;;; 1.2 Some lemmas needed for functional instantiation (first part)
 
146
;;; ----------------------------------------------------------------------------
 
147
 
 
148
;;; Here we define some lemmas to show that the efficiency improvements
 
149
;;; done in transform-mm does not affect the logic:
 
150
 
 
151
(local
 
152
 (defthm substitute-var-apply-subst
 
153
   (equal (apply-subst flg (list equ) term)
 
154
          (substitute-var (car equ) (cdr equ) flg term))))
 
155
 
 
156
 
 
157
(local
 
158
 (defthm substitute-syst-apply-syst
 
159
   (equal (apply-syst (list equ) S)
 
160
          (substitute-syst (car equ) (cdr equ) S)))) 
 
161
 
 
162
(local
 
163
 (defthm substitute-range-apply-range
 
164
   (equal (apply-range (list equ) S)
 
165
          (substitute-range (car equ) (cdr equ) S)))) 
 
166
 
 
167
 
 
168
;;; transform-mm-sel of unification-definition.lisp cannot be
 
169
;;; instantiated by transform-mm, since they different signatures, due
 
170
;;; to the use of multi values in transform-mm. Instead, we will
 
171
;;; instantiate transform-mm-sel for the following function: 
 
172
 
 
173
(local
 
174
 (defun transform-mm-bridge (S-sol)
 
175
   (mv-let (S1 sol1 bool1)
 
176
           (transform-mm (car S-sol) (cdr S-sol))
 
177
           (if bool1 (cons S1 sol1) nil))))
 
178
 
 
179
 
 
180
;;; ----------------------------------------------------------------------------
 
181
;;; 1.3 Termination properties of transform-mm
 
182
;;; ----------------------------------------------------------------------------
 
183
   
 
184
;;; The theorem to justify the definition. This lemma is easily obtained
 
185
;;; by functional instantiation:
 
186
 
 
187
(local
 
188
 (encapsulate
 
189
  ()
 
190
;;; A technical lemma, to make the proof shorter:
 
191
  (local
 
192
   (defthm um-technical
 
193
     (equal (unification-measure '(nil))
 
194
            (unification-measure nil))))
 
195
  
 
196
  (defthm unification-measure-decreases-instance
 
197
    (let ((transform-mm (transform-mm S sol)))
 
198
      (implies (consp S)
 
199
               (e0-ord-<
 
200
                (unification-measure (cons (first transform-mm)
 
201
                                           (second transform-mm)))
 
202
                (unification-measure (cons S sol)))))
 
203
    :hints (("Goal" :use (:functional-instance
 
204
                          (:instance unification-measure-decreases
 
205
                                     (S-sol (cons S sol)))
 
206
                          (transform-mm-sel transform-mm-bridge)
 
207
                          (sel sel-unif)))
 
208
            ("Subgoal 3" :in-theory (disable unification-measure
 
209
                                             (unification-measure)))))))
 
210
 
 
211
 
 
212
 
 
213
(local (in-theory (disable unification-measure)))
 
214
 
 
215
            
 
216
 
 
217
;;; ----------------------------------------------------------------------------
 
218
;;; 1.4 Guard verification 
 
219
;;; ----------------------------------------------------------------------------
 
220
 
 
221
;;; Some lemmas needed for guard verification of mgu-mv
 
222
 
 
223
(local
 
224
 (defthm system-p-substitute-var
 
225
   (implies (and (term-p t1)
 
226
                 (term-p-aux flg term))
 
227
            (term-p-aux flg (substitute-var x t1 flg term)))))
 
228
 
 
229
(local
 
230
 (defthm system-p-substitute-syst
 
231
   (implies (and (system-p S)
 
232
                 (term-p term))
 
233
            (system-p (substitute-syst x term S)))))
 
234
 
 
235
(local
 
236
 (defthm system-p-substitute-range
 
237
   (implies (and (system-p S)
 
238
                 (term-p term))
 
239
            (system-p (substitute-range x term S)))))
 
240
 
 
241
 
 
242
;;; ----------------------------------------------------------------------------
 
243
;;; 1.5 The unification algorithm
 
244
;;; ----------------------------------------------------------------------------
 
245
 
 
246
;;; Appling transform-mm until a normal form is found:
 
247
 
 
248
(defun solve-system (S sol bool)
 
249
  (declare
 
250
   (xargs
 
251
    :guard (and (system-p S)
 
252
                (system-p sol))
 
253
    :measure (unification-measure (cons S sol))
 
254
    :hints
 
255
    (("Goal" :in-theory (disable transform-mm)))))
 
256
  (if (or (not bool) (not (consp S)))
 
257
      (mv S sol bool)
 
258
    (mv-let (S1 sol1 bool1)
 
259
            (transform-mm S sol)
 
260
            (solve-system S1 sol1 bool1))))
 
261
 
 
262
 
 
263
 
 
264
;;; Most general solutions of systems of equations
 
265
 
 
266
(defun mgs-mv (S)
 
267
  (declare (xargs :guard (system-p S)))
 
268
  (mv-let (S1 sol1 bool1)
 
269
          (solve-system S nil t)
 
270
          (declare (ignore S1))
 
271
          (mv sol1 bool1)))
 
272
 
 
273
;;; The unification algorithm
 
274
 
 
275
(defun mgu-mv (t1 t2)
 
276
  (declare (xargs :guard (and (term-p t1) (term-p t2))))
 
277
  (mgs-mv (list (cons t1 t2))))
 
278
  
 
279
 
 
280
 
 
281
;;; We also define as functions the property of being unifiable and the
 
282
;;; umg substitution: 
 
283
(defun unifiable (t1 t2)
 
284
  (declare (xargs :guard (and (term-p t1) (term-p t2))))
 
285
  (mv-let (mgu unifiable)
 
286
          (mgu-mv t1 t2)
 
287
          (declare (ignore mgu))
 
288
          unifiable))
 
289
 
 
290
(defun mgu (t1 t2)
 
291
  (declare (xargs :guard (and (term-p t1) (term-p t2))))
 
292
  (mv-let (mgu unifiable)
 
293
          (mgu-mv t1 t2)
 
294
          (declare (ignore unifiable))
 
295
          mgu))
 
296
 
 
297
 
 
298
;;; REMARK: mgu-mv will be used to compute unifiability and most general
 
299
;;; unifier at the same time. The functions unifiable and mgu are
 
300
;;; defined to be used in the statements of theorems.
 
301
 
 
302
;;; ============================================================================
 
303
;;; 2. Fundamental properties of mgu-mv, unifiable and mgu
 
304
;;; ============================================================================
 
305
 
 
306
;;; ----------------------------------------------------------------------------
 
307
;;; 2.1 Some lemmas needed for the functional instantiation (second part)
 
308
;;; ----------------------------------------------------------------------------
 
309
 
 
310
(local
 
311
 (defthm booleanp-third-solve-system
 
312
   (implies (booleanp bool)
 
313
            (booleanp (third (solve-system S sol bool))))
 
314
   :rule-classes :type-prescription))
 
315
 
 
316
(local
 
317
 (defthm nil-third-implies-nil-second-solve-system
 
318
   (implies (not (third (solve-system S sol t)))
 
319
            (not (second (solve-system S sol t))))))
 
320
 
 
321
 
 
322
;;; solve-system-sel of unification-pattern.lisp cannot be
 
323
;;; instantiated by solve-system, since they different signatures, due
 
324
;;; to the use of multi values in transform-mm. Instead, we will
 
325
;;; instantiate solve-system-sel for the following function: 
 
326
 
 
327
(local
 
328
 (defun solve-system-bridge (S-sol)
 
329
   (if (not (consp S-sol))
 
330
       S-sol
 
331
     (mv-let (S1 sol1 bool1)
 
332
             (solve-system (car S-sol) (cdr S-sol) t)
 
333
             (if bool1 (cons S1 sol1) nil)))))
 
334
 
 
335
;;; The same happens with mgs-sel and mgu-sel
 
336
 
 
337
(local
 
338
 (defun mgs-mv-bridge (S)
 
339
   (let ((solve-system-bridge (solve-system-bridge (cons S nil))))
 
340
     (if solve-system-bridge (list (cdr solve-system-bridge)) nil))))
 
341
 
 
342
(local
 
343
 (defun unifiable-bridge (t1 t2)
 
344
   (mgs-mv-bridge (list (cons t1 t2)))))
 
345
 
 
346
(local
 
347
 (defun mgu-bridge (t1 t2)
 
348
   (first (unifiable-bridge t1 t2))))
 
349
 
 
350
 
 
351
;;; ----------------------------------------------------------------------------
 
352
;;; 2.2 The properties
 
353
;;; ----------------------------------------------------------------------------
 
354
;;; Most of these properties are obtained by functional instantiation.
 
355
 
 
356
;;; Completeness
 
357
;;; ������������
 
358
 
 
359
(defthm  mgu-completeness 
 
360
  (implies (equal (instance t1 sigma)
 
361
                  (instance t2 sigma))
 
362
           (unifiable t1 t2))
 
363
  :rule-classes nil
 
364
  :otf-flg t
 
365
  :hints
 
366
  (("Goal"
 
367
    :use
 
368
    ((:functional-instance
 
369
      unifiable-sel-completeness
 
370
      (sel sel-unif)
 
371
      (transform-mm-sel transform-mm-bridge)
 
372
      (solve-system-sel solve-system-bridge)
 
373
      (mgs-sel mgs-mv-bridge)
 
374
      (unifiable-sel unifiable-bridge))))))
 
375
 
 
376
;;; The hint is not necessary, but makes the proof shorter.
 
377
 
 
378
;;; Soundness
 
379
;;; ���������
 
380
 
 
381
 
 
382
(defthm mgu-soundness 
 
383
  (implies (unifiable t1 t2)
 
384
           (equal (instance t1 (mgu t1 t2))
 
385
                  (instance t2 (mgu t1 t2))))
 
386
  :hints
 
387
  (("Goal"
 
388
    :use
 
389
    ((:functional-instance
 
390
      unifiable-sel-soundness
 
391
      (sel sel-unif)
 
392
      (transform-mm-sel transform-mm-bridge)
 
393
      (solve-system-sel solve-system-bridge)
 
394
      (mgs-sel mgs-mv-bridge)
 
395
      (unifiable-sel unifiable-bridge)
 
396
      (mgu-sel mgu-bridge))))))
 
397
 
 
398
 
 
399
;;; Idempotence
 
400
;;; �����������
 
401
 
 
402
(defthm mgu-idempotent 
 
403
  (idempotent (mgu t1 t2))
 
404
  :hints
 
405
  (("Goal"
 
406
    :use
 
407
    ((:functional-instance
 
408
      mgu-sel-idempotent
 
409
      (sel sel-unif)
 
410
      (transform-mm-sel transform-mm-bridge)
 
411
      (solve-system-sel solve-system-bridge)
 
412
      (mgs-sel mgs-mv-bridge)
 
413
      (unifiable-sel unifiable-bridge)
 
414
      (mgu-sel mgu-bridge))))))
 
415
 
 
416
 
 
417
 
 
418
;;; Generality of the unifier
 
419
;;; �������������������������
 
420
 
 
421
(defthm mgu-most-general-unifier 
 
422
  (implies (equal (instance t1 sigma)
 
423
                  (instance t2 sigma))
 
424
           (subs-subst (mgu t1 t2) sigma))
 
425
   :hints
 
426
   (("Goal"
 
427
    :use
 
428
    ((:functional-instance
 
429
      mgu-sel-most-general-unifier 
 
430
      (sel sel-unif)
 
431
      (transform-mm-sel transform-mm-bridge)
 
432
      (solve-system-sel solve-system-bridge)
 
433
      (mgs-sel mgs-mv-bridge)
 
434
      (unifiable-sel unifiable-bridge)
 
435
      (mgu-sel mgu-bridge))))))
 
436
 
 
437
 
 
438
 
 
439
;;; Substitution-s-p (closure property of mgu)
 
440
;;; ����������������������������������������������
 
441
 
 
442
 
 
443
(defthm mgu-substitution-s-p
 
444
  (implies (and (term-s-p t1) (term-s-p t2))
 
445
           (substitution-s-p (mgu t1 t2)))
 
446
   :hints
 
447
   (("Goal"
 
448
    :use
 
449
    ((:functional-instance
 
450
      mgu-sel-substitution-s-p 
 
451
      (sel sel-unif)
 
452
      (transform-mm-sel transform-mm-bridge)
 
453
      (solve-system-sel solve-system-bridge)
 
454
      (mgs-sel mgs-mv-bridge)
 
455
      (unifiable-sel unifiable-bridge)
 
456
      (mgu-sel mgu-bridge))))))
 
457
 
 
458
 
 
459
 
 
460
;;; Substitution-p (needed for guard verification)
 
461
;;; ����������������������������������������������
 
462
 
 
463
 
 
464
(defthm mgu-substitution-p
 
465
  (implies (and (term-p t1) (term-p t2))
 
466
           (substitution-p (mgu t1 t2)))
 
467
  :hints (("Goal" :use (:functional-instance
 
468
                        mgu-substitution-s-p
 
469
                        (signat (lambda (x n) (eqlablep x)))
 
470
                        (term-s-p-aux term-p-aux)
 
471
                        (substitution-s-p substitution-p)))))
 
472
 
 
473
 
 
474
 
 
475
;;; We disable mgu-mv, unifiable and mgu and their executable
 
476
;;; counter-parts, to be sure that ONLY the above two properties are
 
477
;;; used in the sequel. But before doind this, we state the relations
 
478
;;; between mgu-mv and unifiable and mgu.
 
479
 
 
480
(defthm mgu-mv-unifiable
 
481
  (equal (second (mgu-mv t1 t2)) (unifiable t1 t2)))
 
482
 
 
483
(defthm mgu-mv-mgu
 
484
  (equal (first (mgu-mv t1 t2)) (mgu t1 t2)))
 
485
 
 
486
 
 
487
(in-theory (disable mgu-mv (mgu-mv) mgu (mgu) unifiable (unifiable)))
 
488
 
 
489
 
 
490
;;; ============================================================================
 
491
;;; 3. Some examples
 
492
;;; ============================================================================
 
493
 
 
494
;;; ACL2 !>(mgu '(h u) '(h (b)))
 
495
;;; ((U B))
 
496
;;; ACL2 !>(mgu  1 1)
 
497
;;; NIL
 
498
;;; ACL2 !>(mgu '(f (g x y) (g y x)) '(f u u))
 
499
;;; ((X . Y) (U G Y Y))
 
500
;;; ACL2 !>(unifiable '(f (g x y) (g y x)) '(f x x))
 
501
;;; NIL
 
502
;;; ACL2 !>(mgu '(f (h z) (h (h z))) '(f u (h (h (g v v)))))
 
503
;;; ((Z G V V) (U H (G V V)))
 
504
;;; ACL2 !>(mgu '(f x (g (a) y)) '(f x (g y x)))
 
505
;;; ((X A) (Y A))
 
506
;;; ACL2 !>(mgu '(f x (g a y)) '(f x (g y x)))
 
507
;;; ((A . X) (Y . X))
 
508
;;; ACL2 !>(mgu '(f x (g (a) y)) '(f x (g y x)))
 
509
;;; ((X A) (Y A))
 
510
;;; ACL2 !>(mgu '(f x (g a y)) '(f x (g y x)))
 
511
;;; ((A . X) (Y . X))
 
512
 
 
513
 
 
514
 
 
515