diff options
Diffstat (limited to 'books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp')
| -rw-r--r-- | books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp | 567 |
1 files changed, 567 insertions, 0 deletions
diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp new file mode 100644 index 0000000..4a36b0f --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp @@ -0,0 +1,567 @@ +;;; subsumption.lisp Definition of a particular RULE-BASED matching +;;; algorithm between terms. We use functional instantion of the +;;; pattern given in matching.lisp Using this algorithm, we define the +;;; subsumption relation between terms and lists of terms in a +;;; constructive way, and we prove that subsumption is a preorder. +;;; Created: 11-10-99 Last revison: 07-12-2000 +;;; ============================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "subsumption") + +|# + +(in-package "ACL2") +(local (include-book "matching")) +(include-book "terms") +(include-book "../../../../ordinals/e0-ordinal") +(set-well-founded-relation e0-ord-<) + +;;; ************************************************* +;;; A PARTICULAR AND EXECUTABLE SUBSUMPTION ALGORITHM +;;; ************************************************* + +;;; Here we show how we can obtain a correct subsumption algorithm from +;;; the "pattern" verified in subsumption-definition.lisp: +;;; - We define a particular selection function. +;;; - We introduce multi-values to deal with the pair of systems +;;; S-match. +;;; - Some other minor improvements concerning efficency are done. +;;; - Guards are verified, allowing execution in raw Common Lisp. + +;;; ============================================================================ +;;; 1. The subsumption algorithm between terms +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 1.1 A particular version of transform-subs +;;; ---------------------------------------------------------------------------- + +;;; Selection function. If we detect an inmediate fail, we select it. + +(defun sel-match (S) + (declare (xargs :guard (and (consp S) (system-p S)))) + (if (endp (cdr S)) + (car S) + (let* ((equ (car S)) + (t1 (car equ)) + (t2 (cdr equ))) + (cond ((variable-p t1) + (sel-match (cdr S))) + ((variable-p t2) equ) + ((eql (car t1) (car t2)) + (sel-match (cdr S))) + (t equ))))) + +;;; Main property, needed to instantiate from +;;; subsumption-definition.lisp: +(local + (defthm sel-match-select-a-pair + (implies (consp S) + (member (sel-match S) S)))) + + +;;; The following lemmas help the guard verification of +;;; transform-subs (although they are not strictly needed) + +(local + (defthm sel-match-consp + (implies (and (consp S) + (alistp S)) + (consp (sel-match S))) + :rule-classes :type-prescription)) + + +(encapsulate + () + (local + (defthm transform-subs-guard-verification-stuff-1 + (implies (and (system-p S) + (member equ S)) + (and + (implies (variable-p (car equ)) (eqlablep (car equ))) + (implies (variable-p (cdr equ)) (eqlablep (cdr equ))))))) + + + (local + (defthm transform-subs-guard-verification-stuff-2 + (implies (and (system-p S) + (member equ S)) + (and + (eqlablep (cadr equ)) + (true-listp (cdar equ)) + (true-listp (cddr equ)) + (iff (variable-p (car equ)) (eqlablep (car equ))) + (iff (variable-p (cdr equ)) (eqlablep (cdr equ))))))) + +;;; The rules of transformation: + + (defun transform-subs (S match) + (declare (xargs :guard (and (consp S) (system-p S) + (alistp match)))) + (let* ((ecu (sel-match S)) + (t1 (car ecu)) (t2 (cdr ecu)) + (R (eliminate ecu S))) + (cond + ((variable-p t1) + (let ((bound (assoc t1 match))) + (if bound + (if (equal (cdr bound) t2) + (mv R match t) + (mv nil nil nil)) + (mv R (cons (cons t1 t2) match) t)))) + ((variable-p t2) (mv nil nil nil)) + ((eql (car t1) (car t2)) + (mv-let (empareja bool) + (pair-args (cdr t1) (cdr t2)) + (if bool + (mv (append empareja R) match t) + (mv nil nil nil)))) + (t (mv nil nil nil)))))) + + +;;; REMARK: transform-subs will not be the counterpart of +;;; transform-subs in our functional instantiation. Instead we have to +;;; define a function acting on pair of systems: + +(local + (defun transform-subs-bridge (S-match) + (mv-let (S1 match1 bool1) + (transform-subs (car S-match) (cdr S-match)) + (if bool1 (cons S1 match1) nil)))) + +;;; ---------------------------------------------------------------------------- +;;; 1.2 A particular version of a matching algorithm for systems of equations +;;; ---------------------------------------------------------------------------- + + +;;; Termination properties of transform-subs. + +(local + (defthm transform-subs-decreases-length-of-first-system + (implies (consp S) + (e0-ord-< (length-system (first (transform-subs S match))) + (length-system S))) + :hints (("Goal" :use ((:functional-instance + (:instance + transform-subs-sel-decreases-length-of-first-system + (S-match (cons S match))) + (transform-subs-sel transform-subs-bridge) + (a-pair sel-match))))))) + +;;; A particular version of subs-system + +(defun subs-system (S match bool) + (declare (xargs + :guard (and (system-p S) (alistp match)) + :measure (length-system S) + :hints (("Goal" :in-theory (disable transform-subs))))) + (if (or (not bool) (not (consp S))) + (mv S match bool) + (mv-let (S1 match1 bool1) + (transform-subs S match) + (subs-system S1 match1 bool1)))) + +;;; Matching algorithm for systems of equations: + +(defun match-mv (S) + (declare (xargs :guard (system-p S))) + (mv-let (S1 sol1 bool1) + (subs-system S nil t) + (declare (ignore S1)) + (mv sol1 bool1))) + +;;; REMARK: Again, subs-system and match-mv will not be the counterpart +;;; of subs-system-sel, match-sel in our functional instantiation, +;;; because of signature mismatch. Instead we have to +;;; define functions acting on pair of systems: + +(local + (defun subs-system-bridge (S-match) + (if (normal-form-syst S-match) + S-match + (mv-let (S1 match1 bool1) + (subs-system (car S-match) (cdr S-match) t) + (if bool1 (cons S1 match1) nil))))) + + + +(local + (defun match-mv-bridge (S) + (let ((subs-system-bridge (subs-system-bridge (cons S nil)))) + (if subs-system-bridge (list (cdr subs-system-bridge)) nil)))) + + + +;;; ---------------------------------------------------------------------------- +;;; 1.3 Main properties of the matching algorithm for systems of equations +;;; ---------------------------------------------------------------------------- + +;;; Some technical lemmas + +(local + (defthm booleanp-third-subs-system + (implies (booleanp bool) + (booleanp (third (subs-system S match bool)))) + :rule-classes :type-prescription)) + +(local + (defthm nil-third-implies-nil-second-subs-system + (implies (not (third (subs-system s match t))) + (not (second (subs-system s match t)))))) + +;;; And the main properties of match-mv + +(defthm match-mv-soundness + (implies (second (match-mv S)) + (matcher (first (match-mv S)) S)) + :hints (("Goal" :use ((:functional-instance + match-sel-soundness + (match-sel match-mv-bridge) + (subs-system-sel subs-system-bridge) + (transform-subs-sel transform-subs-bridge) + (a-pair sel-match)))))) + + +(defthm match-mv-completeness + (implies (matcher sigma S) + (second (match-mv S))) + :hints (("Goal" :use ((:functional-instance + match-sel-completeness + (match-sel match-mv-bridge) + (subs-system-sel subs-system-bridge) + (transform-subs-sel transform-subs-bridge) + (a-pair sel-match)))))) + + +(defthm match-mv-substitution-s-p + (implies (system-s-p S) + (substitution-s-p (first (match-mv S)))) + :hints (("Goal" :use ((:functional-instance + match-sel-substitution-s-p + (match-sel match-mv-bridge) + (subs-system-sel subs-system-bridge) + (transform-subs-sel transform-subs-bridge) + (a-pair sel-match)))))) + + +;;; ---------------------------------------------------------------------------- +;;; 1.4 A particular and executable version of subsumption of two terms. +;;; ---------------------------------------------------------------------------- + +;;; The subsumption algorithm + +(defun subs-mv (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (match-mv (list (cons t1 t2)))) + +;;; The subsumption relation + +(defun subs (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (mv-let (matching subs) + (subs-mv t1 t2) + (declare (ignore matching)) + subs)) + +;;; The witness substitution for matching (when (subs t1 t2)) + +(defun matching (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (mv-let (matching subs) + (subs-mv t1 t2) + (declare (ignore subs)) + matching)) + + +;;; REMARK: +;;; subs-mv will be used to compute the subsumption relation and +;;; matching substitutions at the same time. The functions subs and +;;; matching are defined to be used in the statements of theorems. + + +;;; ---------------------------------------------------------------------------- +;;; 1.5 Fundamental properties of subs, matching and subs-mv +;;; ---------------------------------------------------------------------------- +;;; Most of these properties are obtained by functional instantiation. + +;;; Soundness +;;; ········· + +(defthm subs-soundness + (implies (subs t1 t2) + (equal (instance t1 (matching t1 t2)) t2)) + :rule-classes (:rewrite :elim) + :hints (("Goal" :use + (:instance match-mv-soundness (S (list (cons t1 t2))))))) + + +;;; Completeness +;;; ············· + +(defthm subs-completeness + (implies (equal (instance t1 sigma) t2) + (subs t1 t2)) + :rule-classes nil + :hints (("Goal" :use + (:instance match-mv-completeness (S (list (cons t1 t2))))))) + +;;; Substitution-s-p (closure property) +;;; ··································· + + +(defthm matching-substitution-s-p + (implies (and (term-s-p t1) (term-s-p t2)) + (substitution-s-p (matching t1 t2))) + :hints (("Goal" :use + (:instance match-mv-substitution-s-p (S (list (cons t1 t2))))))) + +;;; Substitution-p (needed for guard verification) +;;; ·············································· + + +(defthm matching-substitution-p + (implies (and (term-p t1) (term-p t2)) + (substitution-p (matching t1 t2))) + :hints (("Goal" :use (:functional-instance + matching-substitution-s-p + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux) + (substitution-s-p substitution-p))))) + +;;; Later, We will disable match-mv, subs-mv, matching and subs and +;;; their executable counter-parts, to be sure that ONLY the above two +;;; properties are used in the sequel. But before doing this, we state +;;; the relations between subs-mv and subs and matching. Note that, from +;;; now on, we will not assume any relations between match-mv and +;;; subs-mv + +(defthm subs-mv-subs + (equal (second (subs-mv t1 t2)) (subs t1 t2))) + +(defthm subs-mv-matching + (equal (first (subs-mv t1 t2)) (matching t1 t2))) + + + +;;; ============================================================================ +;;; 2. The subsumption algorithm between lists of terms +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 2.1 Subsumption between lists of terms +;;; ---------------------------------------------------------------------------- + +;;; Sometimes it will be useful to talk abou subsumption between lists +;;; of terms (see, for example, kb/critical-pairs.lisp). We define here +;;; such concept and its main properties, in a similar way to subs. + +;;; The subsumption algorithm (between lists of terms) + +(defun subs-list-mv (l1 l2) + (declare (xargs :guard (and (term-p-aux nil l1) + (term-p-aux nil l2)))) + (mv-let (pair-lists bool) + (pair-args l1 l2) + (if bool (match-mv pair-lists) (mv nil nil)))) + + + +;;; The subsumption relation between lists of terms + +(defun subs-list (l1 l2) + (declare (xargs :guard (and (term-p-aux nil l1) + (term-p-aux nil l2)))) + (mv-let (matching subs-list) + (subs-list-mv l1 l2) + (declare (ignore matching)) + subs-list)) + +;;; The witness substitution for matching lists of terms (when +;;; (subs-list l1 l2)) + +(defun matching-list (l1 l2) + (declare (xargs :guard + (and (term-p-aux nil l1) + (term-p-aux nil l2)))) + (mv-let (matching subs-list) + (subs-list-mv l1 l2) + (declare (ignore subs-list)) + matching)) + + +;;; ---------------------------------------------------------------------------- +;;; 2.2 Main properties of subsumption between lists of terms +;;; ---------------------------------------------------------------------------- + +;;; Two previous lemmas relating matcher with instances: + +(local + (defthm matcher-apply-subst-nil + (implies (second (pair-args l1 l2)) + (iff (matcher sigma (first (pair-args l1 l2))) + (equal (apply-subst nil sigma l1) l2))))) + + +(local + (defthm apply-subst-nil-pair-args + (second (pair-args l1 (apply-subst nil sigma l1))))) + +;;; Soundness +;;; ········· + + +(defthm subs-list-soundness + (implies (subs-list l1 l2) + (equal (apply-subst nil (matching-list l1 l2) l1) l2)) + :rule-classes (:rewrite :elim) + :hints (("Goal" :use + (:instance match-mv-soundness (S (first (pair-args l1 l2))))))) + + +;;; Completeness +;;; ············· + +(defthm subs-list-completeness + (implies (equal (apply-subst nil sigma l1) l2) + (subs-list l1 l2)) + :rule-classes nil + :hints (("Goal" :use + (:instance match-mv-completeness (S (first (pair-args l1 l2))))))) + +;;; Substitution-s-p (closure property) +;;; ··································· + + +(defthm matching-list-substitution-s-p + (implies (and (term-s-p-aux nil l1) (term-s-p-aux nil l2)) + (substitution-s-p (matching-list l1 l2))) + :hints (("Goal" :use + (:instance match-mv-substitution-s-p + (S (first (pair-args l1 l2))))))) + + + +;;; Substitution-p (needed for guard verification) +;;; ·············································· + + +(defthm matching-list-substitution-p + (implies (and (term-p-aux nil l1) + (term-p-aux nil l2)) + (substitution-p (matching-list l1 l2))) + :hints (("Goal" :use (:functional-instance + matching-list-substitution-s-p + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux) + (substitution-s-p substitution-p))))) + + +;;; As with subs, we will disable the definitions related to subs-list to be +;;; sure that ONLY the above two properties are used in the sequel. But +;;; before doing this, we state the relations between subs-list-mv and subs-list +;;; and matching-list. + +(defthm subs-list-mv-subs-list + (equal (second (subs-list-mv t1 t2)) (subs-list t1 t2))) + +(defthm subs-list-mv-matching-list + (equal (first (subs-list-mv t1 t2)) (matching-list t1 t2))) + + +(in-theory + (disable + subs-list-mv (subs-list-mv) subs-list (subs-list) matching-list + (matching-list))) + + + +;;; ============================================================================ +;;; 3. Properties of the subsumption relation +;;; ============================================================================ + + +(in-theory + (disable + match-mv (match-mv) subs-mv (subs-mv) subs (subs) matching (matching))) + + +;;; REMARK: Note that the properties described below only use the +;;; soundness and completeness properties of the subsumption +;;; algorithm (the definition and executable-counterpart of subs +;;; are disabled) + + +;;; ---------------------------------------------------------------------------- +;;; 3.1 Subsumption is a quasi-order +;;; ---------------------------------------------------------------------------- + +;;;; Subsumption reflexive +;;;; ····················· + +(defthm subsumption-reflexive + (subs t1 t1) + :hints (("Goal" :use (:instance + subs-completeness + (sigma nil) (t2 t1))))) + + +;;;; Subsumption transitive +;;;; ······················ + + +(defthm subsumption-transitive + (implies (and (subs t1 t2) (subs t2 t3)) + (subs t1 t3)) + :hints (("Goal" :use ((:instance + subs-completeness + (sigma (composition + (matching t2 t3) + (matching t1 t2))) + (t2 t3)))))) + +(in-theory (disable subsumption-transitive )) + +;;; ---------------------------------------------------------------------------- +;;; 3.2 Several properties of subsumption +;;; ---------------------------------------------------------------------------- + +;;; An useful rule: +;;; ··············· + +(defthm subsumption-apply-subst + (subs term (instance term sigma)) + :hints (("Goal" :use (:instance subs-completeness + (t1 term) (t2 (instance term sigma)))))) + +;;; Variables are minimum elements in this quasi-order +;;; ·················································· + +(defthm variable-minimum-subsumption + (implies (variable-p x) + (subs x term)) + :hints (("Goal" :use ((:instance subs-completeness + (sigma (list (cons x term))) + (t1 x) + (t2 term)))))) + +(in-theory (disable variable-minimum-subsumption)) + +(defthm minimum-subsumption-implies-variable + (implies (and (variable-p x) (subs term x)) + (variable-p term)) + :hints (("Goal" :use (:instance + apply-returns-variable-implies-variable + (flg t) (sigma (matching term x))))) + :rule-classes nil) + + + + + + + + |