From 092176848cbfd27b96c323cc30c54dff4c4a6872 Mon Sep 17 00:00:00 2001 From: Camm Maguire Date: Mon, 8 May 2017 12:58:52 -0400 Subject: Import acl2_7.4dfsg.orig.tar.gz [dgit import orig acl2_7.4dfsg.orig.tar.gz] --- .../multiset/examples/newman/local-confluence.lisp | 471 +++++++++++++++++++++ 1 file changed, 471 insertions(+) create mode 100644 books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp (limited to 'books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp') diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp b/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp new file mode 100644 index 0000000..9ca2fd1 --- /dev/null +++ b/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp @@ -0,0 +1,471 @@ +;;; local-confluence.lisp +;;; Convergent reduction relations have a decidable equivalence closure +;;; Created: 1-11-99 Last modified: 11-10-00 +;;; ============================================================================= + + +;;; To certify this book: +#| +(in-package "ACL2") + +(defconst *abstract-proofs-exports* + '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step + first-of-proof last-of-proof steps-up steps-down steps-valley + proof-before-valley proof-after-valley inverse-r-step inverse-proof + local-peak-p proof-measure proof-before-peak proof-after-peak + local-peak peak-element)) + +(defconst *cnf-package-exports* + (union-eq *acl2-exports* + (union-eq + *common-lisp-symbols-from-main-lisp-package* + *abstract-proofs-exports*))) + +(defpkg "CNF" *cnf-package-exports*) + +(defpkg "NWM" (cons 'multiset-diff *cnf-package-exports*)) + +(defpkg "LCNF" (cons 'multiset-diff *cnf-package-exports*)) + +(certify-book "local-confluence" 5) +|# + +;;; +(in-package "LCNF") + +(local (include-book "confluence")) + +(include-book "newman") + + +;;; **************************************************************************** +;;; LOCALLY CONFLUENT AND TERMINATING REDUCTION RELATIONS HAVE A +;;; DECIDABLE EQUIVALENCE CLOSURE +;;; **************************************************************************** + + +;;; We prove that every noetherian, locally confluent reduction relation +;;; has decidable equivalence closure. This is a good example of how +;;; functional instantiation can be useful. This result can be easily +;;; proved by functional instantiation of the results in the books +;;; previously developed. Using confluence.lisp, we need to show that +;;; the reduction relation is normalizing and has the Church-Rosser +;;; property. And the Church-Rosser property can be proved by using +;;; Newman's lemma, proved in newman.lisp. The normalizing property is +;;; an easy consequence of noetherianity. + +;;; ============================================================================ +;;; 1. A Tool for functional instantation +;;; ============================================================================ + +;;; In this file we have to extensively use functional +;;; instantiation of results previously proved. The functional +;;; instantiations we have to carry out are always of the same kind: +;;; the functional substitution relates functions with the same symbol +;;; name but in different package and the same happen with individual +;;; variables. We define the following functions in :program +;;; mode to provide a tool to make this kind of functional-instance +;;; hints convenient. + +(local + (defun pkg-functional-instance-pairs (lemma-name symbols) + (declare (xargs :mode :program)) + (if (endp symbols) + nil + (cons (list (acl2::intern-in-package-of-symbol + (string (car symbols)) lemma-name) + (car symbols)) + (pkg-functional-instance-pairs lemma-name (cdr symbols)))))) + +(local + (defun pkg-functional-instance + (id lemma-name variable-symbols function-symbols) + (declare (xargs :mode :program)) + (if (equal id (acl2::parse-clause-id "Goal")) + (list :use (list* :functional-instance + (list* :instance + lemma-name + (pkg-functional-instance-pairs + lemma-name variable-symbols)) + (pkg-functional-instance-pairs + lemma-name function-symbols))) + nil))) + + +;;; The function pkg-functional-instance computes a hint (see +;;; computed-hints in the ACL2 manual) and is called +;;; in the following way: + +;;; (pkg-functional-instance id lemma-name variable-symbols +;;; function-symbols) + +;;; where: + +;;; id: is always the variable acl2::id +;;; lemma-name: the name of the lemma to be instantiated +;;; (including the package). +;;; variable-symbols: the list of symbol names of variables to be +;;; instantiated. +;;; function-symbols: the list of symbol names of functions to be +;;; instantiated. + +;;; The computed hint is the functional instantiation of the lemma-name, +;;; relating each variable name and function name (of the package where +;;; the lemma has been proved) to the same symbol name in the current +;;; package. + + +;;; ============================================================================ +;;; 2. Formalizing the hypothesis of the theorem +;;; ============================================================================ + +;;; REMARK: This section is exactly the same as in newman.lisp: +;;; formalization of noetherianity and local confluence. Nevertheless, +;;; since we have to compute normal forms and the function +;;; proof-irreducible, we have to assume the existence of a reducibility +;;; test given by a function reducible with the following properties for +;;; every element x: +;;; 1) When reducible returns non-nil, it returns a legal operator for x. +;;; 2) When reducible returns nil, there are no legal operators for x. +;;; See newman.lisp and confluence-v0.lisp for more details. + + +;;; A noetherian partial order rel (used to justify noetherianity of the +;;; reduction relation defined later) +;;; ..................................................................... + +(encapsulate + ((rel (x y) booleanp) + (fn (x) e0-ordinalp)) + + + (local (defun rel (x y) (declare (ignore x y)) nil)) + (local (defun fn (x) (declare (ignore x)) 1)) + + (defthm rel-well-founded-relation-on-mp + ;; modified for v2-8 ordinals changes + (and + (o-p (fn x)) + (implies (rel x y) + (o< (fn x) (fn y)))) + :rule-classes (:well-founded-relation + :rewrite)) + + (defthm rel-transitive + (implies (and (rel x y) (rel y z)) + (rel x z)))) + +(in-theory (disable rel-transitive)) + + +;;; A noetherian and locally confluent reduction relation +;;; ····················································· + + +(encapsulate + ((legal (x u) boolean) + (reduce-one-step (x u) element) + (reducible (x) boolean) + (transform-local-peak (x) proof)) + + (local (defun legal (x u) (declare (ignore x u)) nil)) + (local (defun reduce-one-step (x u) (+ x u))) + (local (defun reducible (x) (declare (ignore x)) nil)) + (local (defun transform-local-peak (x) (declare (ignore x)) nil)) + + + (defthm legal-reducible-1 + (implies (reducible x) (legal x (reducible x)))) + + (defthm legal-reducible-2 + (implies (not (reducible x)) (not (legal x u)))) + + (defun proof-step-p (s) + (let ((elt1 (elt1 s)) (elt2 (elt2 s)) + (operator (operator s)) (direct (direct s))) + (and (r-step-p s) + (implies direct (and (legal elt1 operator) + (equal (reduce-one-step elt1 operator) + elt2))) + (implies (not direct) (and (legal elt2 operator) + (equal (reduce-one-step elt2 operator) + elt1)))))) + + (defun equiv-p (x y p) + (if (endp p) + (equal x y) + (and (proof-step-p (car p)) + (equal x (elt1 (car p))) + (equiv-p (elt2 (car p)) y (cdr p))))) + +; The following was added by Matt Kaufmann after ACL2 Version 3.4 because of +; a soundness bug fix; see ``subversive'' in :doc note-3-5. + (defthm equiv-p-type + (booleanp (equiv-p x y p)) + :rule-classes :type-prescription) + + (defthm local-confluence + (let ((valley (transform-local-peak p))) + (implies (and (equiv-p x y p) (local-peak-p p)) + (and (steps-valley valley) + (equiv-p x y valley))))) + + (defthm noetherian + (implies (legal x u) (rel (reduce-one-step x u) x)))) + + +;;; ============================================================================ +;;; 2. Theorem: The reduction relation has the Church-Rosser property +;;; ============================================================================ + + + +;;; REMARK: We show that it is possible to define a function +;;; transform-to-valley with the propertiy of transforming every proof +;;; ina an equivalent valley proof. This is done in newman.lisp, so +;;; now we can functionally instantiate the main results proved there. +;;; See newman.lisp for details. + +;;; Well-founded multiset extension of rel +;;; ······································ + +;(acl2::defmul-components rel) +;The list of components is: +; (REL REL-WELL-FOUNDED-RELATION-ON-MP T FN X Y) +(local + (acl2::defmul (REL REL-WELL-FOUNDED-RELATION-ON-MP T FN X Y))) + + +;;; Auxiliary functions in the definition of transform-to-valley +;;; ··························································· + +(local + (defun exists-local-peak (p) + (cond ((or (atom p) (atom (cdr p))) nil) + ((and + (not (direct (car p))) + (direct (cadr p))) + (and (proof-step-p (car p)) + (proof-step-p (cadr p)) + (equal (elt2 (car p)) (elt1 (cadr p))))) + (t (exists-local-peak (cdr p)))))) + +(local + (defun replace-local-peak (p) + (cond ((or (atom p) (atom (cdr p))) nil) + ((and (not (direct (car p))) (direct (cadr p))) + (append (transform-local-peak (list (car p) (cadr p))) + (cddr p))) + (t (cons (car p) (replace-local-peak (cdr p))))))) + + +;;; transform-to-valley terminates +;;; ······························ + +;;; By functional instantiation of the same result in newman.lisp + +(local + (defthm transform-to-valley-admission + (implies (exists-local-peak p) + (mul-rel (proof-measure (replace-local-peak p)) + (proof-measure p))) + + :rule-classes nil + :hints ((pkg-functional-instance + acl2::id + 'nwm::transform-to-valley-admission + '(p) '(fn legal forall-exists-rel-bigger reduce-one-step + proof-step-p equiv-p rel mul-rel + exists-local-peak replace-local-peak + transform-local-peak exists-rel-bigger)) + ("Subgoal 10" :in-theory (enable rel-transitive))))) + + + +;;; Definition of transform-to-valley +;;; ································· + +(local + (defun transform-to-valley (p) + (declare (xargs :measure (proof-measure p) + :well-founded-relation mul-rel + :hints (("Goal" :use + (:instance transform-to-valley-admission))))) + + (if (not (exists-local-peak p)) + p + (transform-to-valley (replace-local-peak p))))) + + +;;; Properties of transform-to-valley: the Church-Rosser property +;;; ····························································· + +;;; By functional instantiation of the same results in newman.lisp + + +(local + (defthm equiv-p-x-y-transform-to-valley + (implies (equiv-p x y p) + (equiv-p x y (transform-to-valley p))) + :hints ((pkg-functional-instance + acl2::id + 'nwm::equiv-p-x-y-transform-to-valley + '(p x y) + '(fn transform-to-valley reduce-one-step legal + proof-step-p equiv-p rel exists-local-peak + replace-local-peak transform-local-peak))))) + +(local + (defthm valley-transform-to-valley + (implies (equiv-p x y p) + (steps-valley (transform-to-valley p))) + :hints ((pkg-functional-instance + acl2::id + 'nwm::valley-transform-to-valley + '(p x y) + '(fn transform-to-valley reduce-one-step legal + proof-step-p equiv-p rel exists-local-peak + replace-local-peak transform-local-peak))))) + + + +;;; ============================================================================ +;;; 3. Theorem: The reduction relation is normalizing +;;; ============================================================================ + +;;; To instantiate the results in confluence.lisp, we have to define a +;;; function proof-irreducible and prove the properties assumed there as +;;; axioms. + +;;; Definition of proof-irreducible +;;; ······························· + +;;; REMARK: Iteratively apply reduction steps until an irreducible +;;; element is found. This function termination can be justified by the +;;; well-founded relation rel. That is, the normal-form computation +;;; terminates because the reduction relation is assumed to be +;;; noetherian. + +(defun proof-irreducible (x) (declare (xargs :measure x + :well-founded-relation rel)) + (let ((red (reducible x))) + (if (not red) + nil + (cons (make-r-step + :direct t :elt1 x :elt2 (reduce-one-step x red) + :operator red) + (proof-irreducible (reduce-one-step x red)))))) + + +;;; Properties of proof-irreducible (normalizing property) +;;; ······················································ + +;;; REMARK: These are the assumed proerties of proof-irreducible in +;;; confluence.lisp, in rewriting rule form: + +(local + (defthm normalizing-1 + (let ((y (elt2 (last-elt (proof-irreducible x))))) + (implies (consp (proof-irreducible x)) + (and (equiv-p x y (proof-irreducible x)) + (not (legal y op))))))) +(local + (defthm normalizing-2 + (implies + (not (consp (proof-irreducible x))) + (not (legal x op))))) + +;;; ============================================================================ +;;; 4. Theorem: The equivalence closure is decidable +;;; ============================================================================ + + +;;; ---------------------------------------------------------------------------- +;;; 4.1 Definition of a decison procedure for <--*--reduce-one-step--*--> +;;; ---------------------------------------------------------------------------- + +(defun normal-form (x) + (declare (xargs :measure x + :well-founded-relation rel)) + (let ((red (reducible x))) + (if (not red) + x + (normal-form (reduce-one-step x red))))) + +(defun r-equivalent (x y) + (equal (normal-form x) (normal-form y))) + + +;;; REMARK: Note that this is not exactly the same definition of the +;;; decision procedure given in confluence.lisp. The point is that in +;;; confluence.lisp the normal-form computation is through the proof +;;; given by proof-irreducible. In order to functionally instantiate the +;;; result of confluence.lisp, we show that it is the same function. + + +;;; This is the same function as r-equiv in confluence.lisp +;;; ······················································· + +;;; REMARK: normal-form-aux is analogue NWM::normal-form, but +;;; normal-form is more eficcient. The same for r-equiv. + +(local + (defun normal-form-aux (x) (last-of-proof x (proof-irreducible x)))) + +(local + (defthm normal-form-aux-normal-form + (equal (normal-form x) + (normal-form-aux x)))) + +(local + (defun r-equiv (x y) + (equal (normal-form-aux x) (normal-form-aux y)))) + + + +;;; ---------------------------------------------------------------------------- +;;; 4.2 Soundness and completeness +;;; ---------------------------------------------------------------------------- + +;;; Completeness +;;; ············ + +;;; By functional instantiation of the same results in confluence.lisp + +(defthm r-equivalent-complete + (implies (equiv-p x y p) + (r-equivalent x y)) + + :rule-classes nil + :hints ((pkg-functional-instance + acl2::id + 'cnf::r-equiv-complete + '(p x y) + '(legal proof-step-p r-equiv + equiv-p reduce-one-step proof-irreducible + transform-to-valley normal-form)))) + + + +;;; Soundness +;;; ········· + +;;; By functional instantiation of the same results in confluence.lisp + +;;; Skolem function +(defun make-proof-common-n-f (x y) + (append (proof-irreducible x) (inverse-proof (proof-irreducible y)))) + + +(defthm r-equivalent-sound + (implies (r-equivalent x y) + (equiv-p x y (make-proof-common-n-f x y))) + + :hints ((pkg-functional-instance + acl2::id + 'cnf::r-equiv-sound + '(x y) + '(legal make-proof-common-n-f proof-step-p + r-equiv equiv-p + reduce-one-step proof-irreducible transform-to-valley + normal-form)))) -- cgit v1.2.3