;;; 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
(and
(e0-ordinalp (fn x))
(implies (rel x y)
(e0-ord-< (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)))))
(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 12" :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))))