← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/deduction/passmore/unification.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/deduction/passmore/unification.lisp
 
1
;; UTEP - Utrecht Texas Equational Prover
 
2
;; Written by Grant Olney Passmore {grant@math.utexas.edu}
 
3
;; 
 
4
;; Unification routines.
 
5
 
 
6
(in-package "ACL2")
 
7
(include-book "general")
 
8
 
 
9
;; UNIFICATION 
 
10
;;
 
11
;; Motivating example:
 
12
;; lit0 = (P x (f x y) (g (f (a) z)))    lit1 = (P u (f (g (a)) u) w)
 
13
;;
 
14
;; Searching for the MGU of lit0 and lit1 should yield:
 
15
;; pi = ( (u (g (a)))   (x (g (a)))   (y (g (a)))   (w (g (f (a) z))) ),
 
16
;; which when applied to lit0 and lit1 yields:
 
17
;;
 
18
;; lit0(pi) = (P (g (a)) (f (g (a)) (g (a))) (g (f (a) z))),
 
19
;; lit1(pi) = (P (g (a)) (f (g (a)) (g (a))) (g (f (a) z))).
 
20
;;
 
21
;; FIRST-UNMATCHED-SYMBOL-PAIR (lit0 lit1)
 
22
;; Given two literals, lit0 and lit1, return the first symbol upon
 
23
;; which they do not match.
 
24
;; G. Passmore : 12/22/05
 
25
 
 
26
(defun first-unmatched-symbol-pair (lit0 lit1)
 
27
  (if (or (and (equal lit0 nil) (equal lit1 nil))
 
28
          (equal lit0 lit1)) nil
 
29
    (if (or (varp lit0) (varp lit1))
 
30
        (if (varp lit0) (list lit0 lit1) (list lit1 lit0)) ;; Orient the pair so that a variable is in the first position.
 
31
      (if (equal (car lit0) (car lit1))
 
32
          (first-unmatched-symbol-pair (cdr lit0) (cdr lit1))
 
33
        (first-unmatched-symbol-pair (car lit0) (car lit1))))))
 
34
 
 
35
;; FUNCTION-SYMBOLS (lit)
 
36
;; Given a literal, lit, return a list of all function 
 
37
;; symbols appearing within, possibly containing duplicates 
 
38
;; (only a membership check will be done upon this list, 
 
39
;; so duplicates are fine).
 
40
;; G. Passmore :: 12/22/05
 
41
 
 
42
;; FUNCTION-SYMBOLS* (lit cur-list)
 
43
;; This auxiliary function locates function symbols by noting that
 
44
;; they appear with an immediate left parenthesis.  
 
45
;; Note that the literal here, lit*, is passed in as the cdr of the literal
 
46
;; given to the parent FUNCTION-SYMBOLS function, so that we omit the top-level 
 
47
;; predicate.
 
48
;; G. Passmore :: 12/22/05
 
49
 
 
50
(defun function-symbols* (lit* cur-list)
 
51
  (if (equal lit* nil) cur-list
 
52
    (if (consp lit*)
 
53
        (if (consp (car lit*)) 
 
54
            (function-symbols* 
 
55
             (cdr lit*) 
 
56
             (append (list (caar lit*)) (function-symbols* (cdar lit*) cur-list)))
 
57
          (function-symbols* (cdr lit*) cur-list))
 
58
      nil)))
 
59
 
 
60
(defun function-symbols (lit)
 
61
  (cond ((consp lit) (function-symbols* (cdr lit) nil))
 
62
         (t nil)))
 
63
 
 
64
;; PREDICATE-SYMBOL (lit)
 
65
;; Given a literal, lit, we return a list of the top-level predicate symbol,
 
66
;; which happens to just be the car.
 
67
;; G. Passmore :: 12/22/05
 
68
   
 
69
(defun predicate-symbol (lit)
 
70
  (cond ((consp lit) (list (car lit)))
 
71
        (t nil)))
 
72
 
 
73
;; VARIABLE-SYMBOLS (lit)
 
74
;; Given a literal, lit, we return a list of all variable symbols contained within.
 
75
;; G. Passmore :: 12/22/05
 
76
 
 
77
(defun variable-symbols (lit)
 
78
  (remove-elements (all-symbols* lit) (append (function-symbols lit) (predicate-symbol lit))))
 
79
 
 
80
;; DEEP-SUBST (sexpr old new)
 
81
;; Given a sexpr, return the result of replacing every occurrence of
 
82
;; old in sexpr with new.
 
83
;; G. Passmore :: 12/22/05
 
84
 
 
85
(defun deepsubst (sexpr old new) 
 
86
  (cond ((equal sexpr old) new)
 
87
        ((consp sexpr)
 
88
              (cons (deepsubst (car sexpr) old new)
 
89
                    (deepsubst (cdr sexpr) old new)))
 
90
        (t sexpr)))
 
91
 
 
92
;; DEEPMEMBER (sexpr element)
 
93
;; Given an element and a sexpr, return t if element is a member of sexpr,
 
94
;; totally traversing the sexpr tree.
 
95
;; Note: This is used for the OCCURS-CHECK.
 
96
;; G. Passmore :: 12/22/05
 
97
 
 
98
(defun deepmember (sexpr element)
 
99
  (cond ((equal sexpr element) t)
 
100
        ((consp sexpr)
 
101
         (or (deepmember (car sexpr) element)
 
102
             (deepmember (cdr sexpr) element)))
 
103
        (t nil)))
 
104
         
 
105
;; APPLY-UNIFIER (form unifier)
 
106
;; Given a unifier, return the result of applying the unifier to a
 
107
;; form (either a literal or an entire clause).
 
108
;; G. Passmore : 12/22/05
 
109
 
 
110
(defun apply-unifier (form unifier)
 
111
  (if (endp unifier) form
 
112
    (let ((cur-subst (car unifier)))
 
113
      (apply-unifier 
 
114
       (deepsubst form (car cur-subst) (cadr cur-subst))
 
115
       (cdr unifier)))))
 
116
        
 
117
;; NEGATIVE-LITERALP (lit)
 
118
;; Given a literal, return t if this literal is negative (i.e. 
 
119
;; of the form (not (P x y)).
 
120
;; G. Passmore :: 12/22/05
 
121
 
 
122
(defun negative-literalp (lit)
 
123
  (equal (car lit) 'NOT))
 
124
 
 
125
;; STRIP-NEGATION (lit)
 
126
;; Given a literal, possibly negated, return the result of stripping
 
127
;; it of its negation symbol (i.e. (not (P x y)) becomes (P x y)).
 
128
;; If literal is not negated, return it unharmed.
 
129
;; G. Passmore :: 12/22/05
 
130
 
 
131
(defun strip-negation (lit)
 
132
  (if (negative-literalp lit)
 
133
      (cadr lit) lit))
 
134
 
 
135
;; LST-INTERSECTION (lst0 lst1)
 
136
;; Given two lists, lst0 and list1, return the list of their
 
137
;; intersecting elements.  Duplicates are OK.
 
138
;; G. Passmore :: 12/22/05
 
139
 
 
140
(defun lst-intersection (lst0 lst1)
 
141
  (if (or (endp lst0) (endp lst1)) nil
 
142
    (if (member-equal (car lst0) lst1)
 
143
        (cons (car lst0) (lst-intersection (cdr lst0) lst1))
 
144
      (lst-intersection (cdr lst0) lst1))))
 
145
 
 
146
;; CLAUSE-VARIABLE-SYMBOLS (clause)
 
147
;; Given a clause, return a list of variables appearing in
 
148
;; the entire clause.  We simply recur upon each literal
 
149
;; contained in clause, collecting the VARIABLE-SYMBOLS
 
150
;; in each of them.  Duplicates are OK.
 
151
;; G. Passmore :: 12/22/05
 
152
 
 
153
(defun clause-variable-symbols (clause)
 
154
  (if (endp clause) nil
 
155
    (append (variable-symbols (car clause))
 
156
            (clause-variable-symbols (cdr clause)))))
 
157
 
 
158
;; CLAUSE-PREDICATE-SYMBOLS (clause)
 
159
;; Given a clause, return a list of all of its predicate symbols.
 
160
;; This is analogous to the above function, modulo the fact that
 
161
;; we must remove the negation from negative literals before passing
 
162
;; them to PREDICATE-SYMBOL.  Duplicates are OK.
 
163
;; G. Passmore :: 12/22/05
 
164
 
 
165
(defun clause-predicate-symbols (clause)
 
166
  (if (endp clause) nil
 
167
    (cons (predicate-symbol (strip-negation (car clause)))
 
168
          (clause-predicate-symbols (cdr clause)))))
 
169
 
 
170
;; STANDARDIZE-CLAUSE (clause frozen-vars available-std-vars)
 
171
;; Given a clause, a list of frozen variables that must be renamed,
 
172
;; and a list of available unused standard variables to use,
 
173
;; return the result of performing substitutions upon clause
 
174
;; until its variables have been standardized.
 
175
;; G. Passmore :: 12/22/05
 
176
 
 
177
(defun standardize-clause (clause frozen-vars available-std-vars)
 
178
  (if (endp frozen-vars) clause
 
179
    (standardize-clause 
 
180
     (deepsubst clause (car frozen-vars) (car available-std-vars))
 
181
     (cdr frozen-vars)
 
182
     (cdr available-std-vars))))
 
183
 
 
184
;; STANDARDIZE-APART (clause0 clause1)
 
185
;; Given two clauses, clause0 and clause1, we assign a new variable
 
186
;; name to every variable in clause1 that also appears in clause0.
 
187
;; We use *STANDARDIZE-APART-VARS-LST* to find unused variable names.
 
188
;; We return the adjusted clause1.
 
189
;; G. Passmore :: 12/22/05
 
190
 
 
191
(defun standardize-apart (clause0 clause1)
 
192
  (let ((clause0-vars (clause-variable-symbols clause0))
 
193
        (clause1-vars (clause-variable-symbols clause1)))
 
194
    (let ((c0-vars-intersect-c1-vars 
 
195
           (lst-intersection clause0-vars clause1-vars))
 
196
          (usable-SAVL-vars
 
197
           (remove-elements *standardize-apart-vars-lst* (append clause0-vars clause1-vars))))
 
198
      (standardize-clause clause1 (remove-duplicates c0-vars-intersect-c1-vars) usable-SAVL-vars))))
 
199
 
 
200
;; UNIFY (lit0 lit1) => (MV unified-instance mgu) | 'DNU | 'OUT-OF-TIME
 
201
;; Given two literals, lit0 and lit1, find and apply the most general unifier, 
 
202
;; returning (mv lit0 NIL) if the terms are unified by the empty substitution, 
 
203
;; returning (mv 'DNU nil) of the terms do not unify, and returning (mv unified-instance mgu)
 
204
;; if unification is successful.
 
205
;; Note: We may run out of time, in which case we return (mv 'OUT-OF-TIME nil). 
 
206
;; We *do* utilize an occurs-check.
 
207
;; G. Passmore :: 12/22/05
 
208
 
 
209
(defun unify* (lit0 lit1 function-symbols predicate-symbols cur-mgu time-count)
 
210
  (declare (xargs :measure (acl2-count time-count)))
 
211
  (cond ((not (posp time-count)) (mv 'OUT-OF-TIME nil)) 
 
212
        ((equal lit0 lit1) (mv lit0 cur-mgu))
 
213
        (t (let ((cur-unifier (first-unmatched-symbol-pair lit0 lit1)))
 
214
;; If the two literals disagree on a function symbol, they do not unify.             
 
215
             (cond ((and (member (car cur-unifier) function-symbols)
 
216
                         (member (cadr cur-unifier) function-symbols))
 
217
                    (mv 'DNU nil))
 
218
;; If the two literals disagree on a predicate symbol, they do not unify.
 
219
                   ((or (member (car cur-unifier) predicate-symbols)
 
220
                        (member (cadr cur-unifier) predicate-symbols))
 
221
                    (mv 'DNU nil))
 
222
;; If the current unifier does not pass an OCCURS-CHECK, they do not unify. 
 
223
                   ((and (consp (cadr cur-unifier))
 
224
                         (deepmember (cadr cur-unifier) (car cur-unifier))) (mv 'DNU nil))
 
225
;; Otherwise, we now perform the substitution and recur!
 
226
                   (t (unify* (deepsubst lit0 (car cur-unifier) (cadr cur-unifier))
 
227
                              (deepsubst lit1 (car cur-unifier) (cadr cur-unifier))
 
228
                              function-symbols predicate-symbols (list* cur-unifier cur-mgu) (1- time-count))))))))
 
229
 
 
230
;; Parent unification function: Given two literals, we return
 
231
;; a form of the species (mv unified-instance mgu) if lit0 and lit1
 
232
;; unify.  See above comments preceding UNIFY* for details on what
 
233
;; we return when unification fails.
 
234
;; G. Passmore :: 12/22/05
 
235
 
 
236
(defun unify (lit0 lit1)
 
237
  (unify* lit0 lit1 
 
238
          (append (function-symbols lit0) (function-symbols lit1))
 
239
          (append (predicate-symbol lit0) (predicate-symbol lit1))
 
240
  nil 100))