Skip to content

Instantly share code, notes, and snippets.

@fogus
Created September 21, 2011 01:40
Show Gist options
  • Save fogus/1230975 to your computer and use it in GitHub Desktop.
Save fogus/1230975 to your computer and use it in GitHub Desktop.
;;; rewriting.lisp
;;; Directed equations as reductions: rewrite rules and normal forms.
;;; Created: 13-11-99 Last revision: 10-04-2001
;;; ====================================================================
#| To certify this book:
(in-package "ACL2")
(certify-book "rewriting")
|#
(in-package "ACL2")
(include-book "../terminos/subsumption")
(include-book "equational-theories")
;;; *******************************************************************
;;; REDUCIBILITY, REWRITE RULES, NORMAL FORMS, REDUCTION ORDERINGS
;;; *******************************************************************
;;; In this book:
;;; - Definition and verification of a reducibility test for the
;;; equational reduction defined in equational-theories.lisp.
;;; - Definition of term rewriting systems.
;;; - Verification of a function to perform one step of reduction
;;; w.r.t. term rewriting systems.
;;; - Definition and properties of reduction orderings.
;;; - Definition of a function to compute normal form with respect to
;;; terminating term rewriting systems.
;;; ============================================================================
;;; 1. A reducibility test: definition and verification.
;;; ============================================================================
;;; Recall from the book convergent.lisp that we need to define an applicability
;;; test (or reducibility test) in order to export the main result of
;;; that book from the abstract case to the equational case. By
;;; definition, a reducibility test is a function receiving an element
;;; (a term in this case) and returning a legal operator (equational
;;; operator) whenever it exists.
;;; In this section we define a reducibility test for the equational
;;; reduction defined in equational-theories.lisp.
;;; ----------------------------------------------------------------------------
;;; 1.1 Definition of a reducibility test
;;; ----------------------------------------------------------------------------
;;; REDUCIBLE-TOP
;;; ·············
;;; To be reducible at top position by a rule of E (we return a
;;; multivalue with the first rule that reduces term + the matching
;;; substitution + t if such a rule exists, or (mv nil nil nil)
;;; otherwise.
(defun eq-reducible-top (term E)
(declare (xargs :guard (and (term-p term) (system-p E))))
(if (endp E)
(mv nil nil nil)
(let ((equ (car E)))
(mv-let (matching subsumption)
(subs-mv (lhs equ) term)
(if subsumption
(mv equ matching t)
(eq-reducible-top term (cdr E)))))))
;;; Closure property
(local
(defthm eq-reducible-top-substitution-s-p
(implies (and (term-s-p term)
(system-s-p E)
(third (eq-reducible-top term E)))
(substitution-s-p (second (eq-reducible-top term E))))))
;;; The following results are needed for guard verification
(local
(defthm eq-reducible-top-term-p
(implies (and (term-p-aux flg term) flg
(system-p E)
(third (eq-reducible-top term E)))
(and
(term-p (lhs (first (eq-reducible-top term E))))
(term-p (rhs (first (eq-reducible-top term E))))))))
(local
(encapsulate
()
(local
(defthm eq-reducible-top-substitution-p-lemma
(implies (and (term-p term)
(system-p E)
(third (eq-reducible-top term E)))
(substitution-p (second (eq-reducible-top term E))))
:rule-classes nil))
(defthm eq-reducible-top-substitution-p
(implies (and (term-p-aux flg term) flg
(system-p E)
(third (eq-reducible-top term E)))
(substitution-p (second (eq-reducible-top term E))))
:otf-flg t
:hints (("Goal" :use eq-reducible-top-substitution-p-lemma)))))
;;; EQ-REDUCIBLE (and EQ-REDUCIBLE-AUX)
;;; ···································
;;; Recall from equational-theories.lisp that an equational operator
;;; consists of a rule, a position and a matching substitution. This
;;; function has to return a legal eq-operator for a given term if such
;;; exists, nil otherwise. We use an auxiliary function
;;; eq-reducible-aux with three extra parameters (flg, posr and arg) in
;;; addition to term and E.
;;; Intuitively, we search a legal equational operator for a given term
;;; t1 in a depth-first way. The function eq-reducible-aux implements
;;; this recursive search. Initially, the function is called
;;; (eq-reducible-aux t t1 nil 0 E). During the proccess,
;;; (eq-reducible-aux flg term posr arg E) intuitively means the
;;; following : (reverse posr) is the position where term is included in
;;; the original term t1. So term is the subterm of the original term to
;;; be explored and posr is the reverse of the position of that subterm
;;; in the original term t1. If flg=nil, term is considered as a list of
;;; terms (the arguments of the subterm being explored) and arg is the
;;; number of argument. More precisely, the interpretation of
;;; eq-reducidible-aux is as follows:
;;; - If flg=t, term is a term and the function returns nil or the
;;; eq-operator with three components:
;;; * position: (append (reverse posr) q)
;;; * rule: l -> r
;;; * matching: sigma where q is the first
;;; position (searching in a depth-first way) such that term/q =
;;; sigma(l), for some rule l -> r in E.
;;; - If flg=nil, term is a list of terms and returns nil or the
;;; eq-operator with three components:
;;; * position: (append (reverse posr) (cons n q))
;;; * rule: l -> r
;;; * matching: sigma where n >= arg and t1 = (nth (- n arg 1) term)
;;; is the first element of term such that a subterm of it is
;;; reducible by the rule, and such that q is the first position of t1
;;; (searching in a depth-first way) such that t1/q is equal to
;;; sigma(l), for some rule l -> r in E.
;;; Note that we are interested in the case posr=nil, flg=t, arg=0.
(defun eq-reducible-aux (flg term posr arg E)
(if flg
(mv-let (equ match top-reducible)
(eq-reducible-top term E)
(if top-reducible
(make-eq-operator :pos (revlist posr)
:rule equ
:match match)
(if (variable-p term)
nil
(eq-reducible-aux nil (cdr term) posr 0 E))))
(if (endp term)
nil
(let ((first-arg-red
(eq-reducible-aux t (car term) (cons (1+ arg) posr) 0 E)))
(if first-arg-red
first-arg-red
(eq-reducible-aux nil (cdr term) posr (1+ arg) E))))))
;;; Closure property
(local
(defthm eq-reducible-aux-substitution-s-p
(implies (and (term-s-p-aux flg term)
(system-s-p E)
(eq-reducible-aux flg term posr arg E))
(substitution-s-p
(op-match (eq-reducible-aux flg term posr arg E))))))
(defun eq-reducible (term E)
(eq-reducible-aux t term nil 0 E))
;;; ----------------------------------------------------------------------------
;;; 1.2 Verification of the reducibility test
;;; ----------------------------------------------------------------------------
;;; Remember form convergent.lisp that the function that tests
;;; reducibility in a given abstact relation has to verify this two
;;; properties:
;;; 1) eq-reducible, when not nil, returns a legal eq-operator for the
;;; term in a given signature.
;;; I.e. the following theorem:
;;; (defthm eq-reducible-implies-legal
;;; (implies (and (term-s-p term)
;;; (eq-reducible term E)
;;; (system-s-p E))
;;; (eq-legal term (eq-reducible term E) E)))
;;; 2) When eq-reducible returns nil, there are not eq-legal operators
;;; for the term in a given signature.
;;; I.e., the following theorem:
;;; (defthm not-eq-reducible-nothing-legal
;;; (implies (not (eq-reducible term E))
;;; (not (eq-legal term op E))))
;;; Our goal in the following is to prove the two above theorems
;;; ····················
;;; 1.2.1 Preliminaries
;;; ····················
;;; A boolean version of eq-reducible-aux
;;; ·····································
;;; It will be useful to define a function that takes the same boolean
;;; values than eq-reducible-aux.
(local
(defun eq-reducible-p-aux (flg term E)
(if flg
(cond ((mv-let (equ match top-reducible)
(eq-reducible-top term E)
(declare (ignore equ match))
top-reducible) t)
((variable-p term) nil)
(t (eq-reducible-p-aux nil (cdr term) E)))
(cond ((endp term) nil)
((eq-reducible-p-aux t (car term) E) t)
(t (eq-reducible-p-aux nil (cdr term) E))))))
;;; The following is the main property of eq-reducible-p-aux. Note that
;;; when only truth values of eq-reducible-p are important, the posr and
;;; arg arguments of eq-reducible-aux are irrelevant, and this rule
;;; allows us to forget about them.
(local
(defthm eq-reducible-p-iff-eq-reducible
(iff (eq-reducible-aux flg term posr arg E)
(eq-reducible-p-aux flg term E))))
(local
(in-theory (disable eq-reducible-p-iff-eq-reducible)))
;;; The main property of eq-reducible-top
;;; ·····································
;;; When eq-reducible-top-succeeds, it returns a rule and matching
;;; substitution for that rule and the term:
(local
(defthm eq-reducible-top-subs-lhs
(let ((eq-reducible-top
(eq-reducible-top term E)))
(implies (third eq-reducible-top)
(equal (instance (lhs (first eq-reducible-top))
(second eq-reducible-top))
term)))))
;;; The position of term computed by eq-reducible-aux
;;; ·················································
;;; By definition, (eq-reducible-aux flg term posr arg E) when non nil,
;;; computes a position appending (reverse posr) with the position of
;;; the subterm of term where reducibility is detected. This macro
;;; reducible-pos allows us to talk about the position computed without
;;; the prefix (reverse posr):
(local
(defmacro reducible-pos (flg term posr arg E)
`(difference-pos (revlist ,posr)
(op-pos (eq-reducible-aux ,flg ,term ,posr ,arg ,E)))))
;;; ·····························································
;;; 1.2.1 eq-reducible returns a legal eq-operator (when non-nil)
;;; ·····························································
;;; Our goal is the following lemma, stablishing the main property of
;;; eq-reducible-aux:
; ; (local
; ; (defthm eq-reducible-aux-main-lemma
; ; (let* ((red (eq-reducible-aux flg term posr arg E))
; ; (pos (op-pos red))
; ; (rule (op-rule red))
; ; (matching (op-match red))
; ; (q (difference-pos (revlist posr) pos)))
; ; (implies (and red (integerp arg) (>= arg 0))
; ; (if flg
; ; (and (position-p-rec flg q term)
; ; (equal (instance (lhs rule) matching)
; ; (occurrence-rec flg term q)))
; ; (and (position-p-rec flg (cons (- (car q) arg) (cdr q))
; ; term)
; ; (equal (instance (lhs rule) matching)
; ; (occurrence-rec flg term (cons (- (car q) arg)
; ; (cdr q)))))))))
;;;
;;; Note how this lemma formalizes the desription of the function
;;; eq-reducible-aux given when we defined it. Note also that we are
;;; using the alternative recursive versions of position-p and
;;; occurrence. The intended result is a obtained instantiating this
;;; lemma for flg=t, posr=nil and arg=0
;;; Some previous lemmas needed
;;; ···························
;;; The following encapsulate proves that the argument posr is always a
;;; preffix of the returned position:
(local
(encapsulate
()
;;; We need a specific induction scheme:
(local
(defun eq-reducible-append-induction (flg term l m arg E)
(if flg
(if (mv-let (equ match top-reducible)
(eq-reducible-top term E)
(declare (ignore equ match))
top-reducible)
arg ;; we make this formal relevant
(if (variable-p term)
t
(eq-reducible-append-induction nil (cdr term) l m 0 E)))
(if (endp term)
t
(let ((first-arg-red
(eq-reducible-aux t (car term)
(cons (1+ arg) (append l m)) 0 E)))
(if first-arg-red
(eq-reducible-append-induction t (car term)
(cons (1+ arg) l) m 0 E)
(eq-reducible-append-induction nil (cdr term) l m (1+ arg) E)))))))
;;; From the truth point of view the third argument (the position) is
;;; irrelevant:
(local
(defthm eq-reducible-aux-pos1-iff-pos2
(implies (eq-reducible-aux flg term pos1 arg E)
(eq-reducible-aux flg term pos2 arg E))
:hints (("Goal"
:in-theory (enable eq-reducible-p-iff-eq-reducible)))))
(local
(defthm eq-reducible-aux-pos1-iff-pos2-bis
(implies (not (eq-reducible-aux flg term pos1 arg E))
(not (eq-reducible-aux flg term pos2 arg E)))))
;;; This is the main lemma. It generalizes the result we are looking
;;; form: every prefix of the reverse of the third argument is a prefix
;;; of the position finally computed:
(local
(defthm eq-reducible-preffix-append
(implies (eq-reducible-aux flg term (append l m) arg E)
(equal (op-pos (eq-reducible-aux flg term (append l m) arg E))
(append (revlist m)
(op-pos (eq-reducible-aux flg term l arg E)))))
:rule-classes nil
:hints (("Goal"
:induct (eq-reducible-append-induction flg term l m arg E)))))
;;; A particular case:
(defthm eq-reducible-preffix-append-instance
(implies (eq-reducible-aux flg term (cons x l) arg E)
(equal
(op-pos (eq-reducible-aux flg term (cons x l) arg E))
(append (revlist (cons x l))
(op-pos (eq-reducible-aux flg term nil arg E)))))
:hints (("Goal" :use (:instance eq-reducible-preffix-append
(l nil) (m (cons x l))))))))
;;; Some arithmetic results
(local
(defthm arg-cancelation
(equal (+ (- arg) 1 arg) 1)))
(local
(defthm integer-difference
(implies (and (integerp x) (integerp y))
(integerp (+ (- x) y)))))
(local
(defthm distributivity-of-minus
(equal (- (+ a b)) (+ (- a) (- b)))))
;;; The argument arg always increases when running on a list of terms:
(local
(defthm arg-increases
(implies (eq-reducible-aux nil term posr arg E)
(> (car (reducible-pos nil term posr arg E))
arg))
:rule-classes :linear))
;;; A particular case:
(local
(defthm arg-increases-instance
(implies (and (integerp arg) (eq-reducible-aux nil term posr
(1+ arg) E))
(<= 2 (+ (- arg) (car (reducible-pos nil term posr
(+ 1 arg) E)))))))
;;; The argument arg is always integer if it is initially an integer.
(local
(defthm arg-integer
(implies (and (integerp arg) (eq-reducible-aux nil term posr arg E))
(integerp (car (reducible-pos nil term posr arg E))))))
;;; Before beginning the rest of the proofs, we enable the alternatives
;;; recursive versions of position-p, occurrence and replace-term.
(in-theory
(union-theories (current-theory :here) *position-rec-versions*))
;;; This is the main lemma:
;;; ·······················
(local
(defthm eq-reducible-aux-main-lemma
(let* ((red (eq-reducible-aux flg term posr arg E))
(pos (op-pos red))
(rule (op-rule red))
(matching (op-match red))
(q (difference-pos (revlist posr) pos)))
(implies (and red (integerp arg) (>= arg 0))
(if flg
(and (position-p-rec flg q term)
(equal (instance (lhs rule) matching)
(occurrence-rec flg term q)))
(and (position-p-rec flg (cons (- (car q) arg) (cdr q))
term)
(equal (instance (lhs rule) matching)
(occurrence-rec flg term (cons (- (car q) arg)
(cdr q))))))))
:rule-classes nil))
;;; Some additional results needed
;;; ······························
;;; eq-reducible-aux returns nil or an eq-operator.
(local
(defthm eq-reducible-aux-eq-operator-op
(let ((reducible (eq-reducible-aux flg term posr arg E)))
(implies reducible
(eq-operator-p reducible)))))
;;; eq-reducible-aux, when non nil, returns a rule of E (in the rule
;;; field).
(local
(defthm eq-reducible-top-member-E
(implies (third (eq-reducible-top term E))
(member (first (eq-reducible-top term E))
E))))
(local
(defthm eq-reducible-aux-rule-member-E
(let ((reducible (eq-reducible-aux flg term posr arg E)))
(implies reducible
(member (op-rule reducible) E)))))
;;; AT LAST, THE INTENDED RELATION, FIRST PART
;;; ··········································
(defthm eq-reducible-implies-eq-legal
(implies (and (system-s-p E)
(term-s-p term)
(eq-reducible term E))
(eq-legal term (eq-reducible term E) E))
:hints (("Goal" :use
(:instance
eq-reducible-aux-main-lemma (flg t) (posr nil) (arg 0)))))
;;; REMARK: Note that, exactly as we intended, we state the theorem in
;;; terms of position-p and occurrence, and NOT in terms of their
;;; recursive counterparts, position-p-rec and occurrence-rec, used till
;;; now for the above proofs.
;;; ····························································
;;; 1.2.2 If not eq-reducible, there are not eq-legal operators.
;;; ····························································
;;; Previous lemmas
;;; ···············
;;; The property for eq-reducible-top
(local
(defthm not-eq-reducible-top-member
(implies (and (not (third (eq-reducible-top term e)))
(member rule e))
(not (subs (car rule) term)))))
;;; The main lemma:
(local
(defthm not-eq-reducible-aux-not-subs-positions-lemma
(implies (and (not (eq-reducible-p-aux flg term E))
(position-p-rec flg pos2 term)
(member rule E))
(not (subs (lhs rule)
(occurrence-rec flg term pos2))))
:rule-classes nil))
;;; The same lemma as above stablished in terms of instance, using
;;; subs-completeness:
(local
(defthm not-eq-reducible-aux-not-subs-positions
(implies (and (not (eq-reducible-p-aux flg term E))
(position-p-rec flg pos2 term)
(member rule E))
(not (equal (instance (lhs rule) sigma)
(occurrence-rec flg term pos2))))
:hints (("Goal" :use
((:instance not-eq-reducible-aux-not-subs-positions-lemma)
(:instance subs-completeness
(t1 (lhs rule))
(t2 (occurrence-rec flg term pos2))))))))
;;; THE INTENDED RELATION, SECOND PART
;;; ··································
(defthm not-eq-reducible-nothing-eq-legal
(implies (not (eq-reducible term E))
(not (eq-legal term op E)))
:hints (("Goal" :in-theory (enable eq-reducible-p-iff-eq-reducible))))
;;; ============================================================================
;;; 2. Rewrite systems. Definition
;;; ============================================================================
;;; ---------------
;;; REWRITE SYSTEMS
;;; ---------------
;;; Definition: a rewrite system is a true list of equations s.t. the
;;; lhs is not a variable and the variables in the right hand side are in
;;; the left hand side. The function rewrite-rules checks these
;;; conditions. The function rewrite-system-s-p checks additionally that we
;;; have a system of equations in the given signature.
(defun rewrite-rules (R)
(if (atom R)
(equal R nil)
(and
(not (variable-p (lhs (car R))))
(subsetp (variables t (rhs (car R)))
(variables t (lhs (car R))))
(rewrite-rules (cdr R)))))
(defmacro rewrite-system-s-p (R)
`(and (system-s-p ,R)
(rewrite-rules ,R)))
;;; ============================================================================
;;; 3. One step of reduction: definition and verification
;;; ============================================================================
;;; Note that functions eq-reducible and eq-reduce-one-step are given a
;;; "theoretical" implementation of applying one step of reduction:
;;; eq-reducible searches for an appliable equational operator and (if
;;; any) and eq-reduce-one-step applies the operator. But from a more
;;; practical point of view, we don't need to deal with equational
;;; operators.
;;; We will see now an executable function for testing reducibility of
;;; a term w.r.t a rewrite system and, at the same time, applying one
;;; step of reduction in case of reducibility. We will define it and we
;;; will prove that computes the same as a combination
;;; eq-reducible and eq-reduce-one-step, in case of rewrite system.
;;; Guard verification
(local
(defthm system-p-alistp
(implies (substitution-p S) (alistp S))))
;;; ----------------------------------------------------------------------------
;;; 3.1 Definition of one step of reduction
;;; ----------------------------------------------------------------------------
;;; -------------------------
;;; R-REDUCE-AUX and R-REDUCE
;;; -------------------------
;;; This function r-reduce-aux receives as input a term (or list of
;;; terms, depending on flg) and and a term rewriting system R, and
;;; returns a multivalue of two: the second one is nil if the term is
;;; irreducible w.r.t. R and t if it can be reduced. In this case, the
;;; first value is the result of applying one-step of reduction. As with
;;; eq-reducible-aux, the search of an subterm instance of the lhs of a
;;; rule in R is done in a depth-first way.
(defun r-reduce-aux (flg term R)
(declare (xargs :guard (and (term-p-aux flg term)
(system-p R))))
(if flg
(if (variable-p term)
(mv nil nil)
(mv-let
(equ match top-red)
(eq-reducible-top term R)
(if top-red
(mv (instance (rhs equ) match) t)
(mv-let
(reduced-args reducible-args)
(r-reduce-aux nil (cdr term) R)
(if reducible-args
(mv (cons (car term) reduced-args) t)
(mv nil nil))))))
(if (endp term)
(mv nil nil)
(mv-let
(reduced-first reducible-first)
(r-reduce-aux t (car term) R)
(if reducible-first
(mv (cons reduced-first (cdr term)) t)
(mv-let
(reduced-rest reducible-rest)
(r-reduce-aux nil (cdr term) R)
(if reducible-rest
(mv (cons (car term) reduced-rest) t)
(mv nil nil))))))))
;;; r-reduce is r-reduce-aux acting on terms:
(defun r-reduce (term R)
(declare (xargs :guard (and (term-p term) (system-p R))))
(r-reduce-aux t term R))
;;; ----------------------------------------------------------------------------
;;; 3.2 Closure property
;;; ----------------------------------------------------------------------------
(local
(defthm r-reduce-aux-term-p-aux
(implies (and (term-p-aux flg term) (system-p TRS))
(term-p-aux flg (first (r-reduce-aux flg term TRS))))
:hints (("Subgoal *1/2"
:in-theory (disable apply-subst-term-p-aux)
:use (:instance apply-subst-term-p-aux
(flg t)
(term (rhs (first (eq-reducible-top term
TRS))))
(sigma (second (eq-reducible-top term TRS))))))))
(defthm r-reduce-term-p
(implies (and (term-p term) (system-p TRS))
(term-p (first (r-reduce term TRS)))))
;;; ----------------------------------------------------------------------------
;;; 3.3 Main properties
;;; ----------------------------------------------------------------------------
;;; We have to prove:
;;; 1) the second value of r-reduce-aux is not nil if and only if
;;; eq-reducible-aux is not nil (the truth values are the same),
;;; whenever R is a rewrite system.
;;; 2) When the second value of r-reduce-aux is not nil, applying with
;;; eq-reduce-one-step the operator obtained, returns the first value
;;; returned by r-reduce-aux.
;;; ·····································································
;;; 3.2.1 r-reduce and eq-reducible returns the same truth values
;;; ·····································································
;;; Note that the only difference between r-reduce-aux and
;;; eq-reducible-aux (w.r.t. its truth values) is that we do not a to
;;; test reducibility of variables, since lhs of rules of rewrite
;;; systems are not variables:
(local
(encapsulate
()
(local
(defthm If-apply-subst-returns-variable-then-variable
(implies (and (not (variable-p t1)) (variable-p t2))
(not (equal (apply-subst flg sigma t1) t2)))))
(defthm subs-variable-minimum
(implies (and (variable-p t2) (not (variable-p t1)))
(not (subs t1 t2)))
:hints (("Goal" :use subs-soundness
:in-theory (disable subs-soundness))))
(defthm eq-reducible-p-aux-iff-r-reduce-aux
(implies (rewrite-rules R)
(iff (eq-reducible-aux flg term pos arg R)
(second (r-reduce-aux flg term R)))))))
;;; As a particular case (flg=t), the first main property of r-reduce
;;; (non-local theorem):
(defthm eq-reducible-p-iff-r-reduce
(implies (rewrite-rules R)
(iff (second (r-reduce term R))
(eq-reducible term R))))
;;; ·····································································
;;; 3.2.2 r-reduce performs the same reduction step as
;;; eq-reduce-one-step when applied withe the operator given by
;;; eq-reducible
;;; ·····································································
;;; Two technical lemmas:
(local
(defthm variables-not-reducible-by-rewrite-systems
(implies (and (variable-p term)
(rewrite-rules R))
(not (third (eq-reducible-top term R))))))
(local
(defthm consp-eq-reducible-aux-of-lists
(implies (eq-reducible-aux nil term posr arg R)
(consp (difference-pos (revlist posr)
(op-pos (eq-reducible-aux nil term
posr arg r)))))))
;;; The main lemma, stablishing the relation between eq-reducible-aux and
;;; r-reduce-aux
(local
(defthm eq-reducible-aux-r-reduce-aux-relation
(let* ((red (eq-reducible-aux flg term posr arg R))
(pos (op-pos red))
(rule (op-rule red))
(matching (op-match red))
(sigma-rhs (instance (rhs rule) matching))
(q (difference-pos (revlist posr) pos))
(reduced (first (r-reduce-aux flg term R))))
(implies (and red (integerp arg) (>= arg 0) (rewrite-rules R))
(if flg
(equal
(replace-term-rec flg term q sigma-rhs)
reduced)
(equal
(replace-term-rec flg term
(cons (- (car q) arg) (cdr q))
sigma-rhs)
reduced))))
:rule-classes nil))
;;; Too much cases, fix it!!
(local
(defthm eq-reducible-implies-legal-corollary
(implies (eq-reducible term E)
(position-p-rec t (op-pos (eq-reducible-aux t term nil 0 E)) term))
:hints (("Goal" :use (:instance
eq-reducible-aux-main-lemma
(flg t) (posr nil) (arg 0))))))
;;; As a particular case (flg=t), the second main property of r-reduce
;;; (non-local theorem):
(defthm r-reduce-equal-eq-reduce-one-step-when-non-nil
(implies (and (rewrite-rules R)
(second (r-reduce term R)))
(equal (first (r-reduce term R))
(eq-reduce-one-step
term
(eq-reducible term R))))
:hints (("Goal" :use (:instance
eq-reducible-aux-r-reduce-aux-relation
(flg t) (posr nil) (arg 0)))))
;;; We now disable the recursive versions of position-p, replace-term
;;; and occurrence
(in-theory
(set-difference-theories (current-theory :here) *position-rec-versions*))
;;; ============================================================================
;;; 4. Termination of term rewriting systems. Reduction orderings.
;;; ============================================================================
;;; Reduction orderings are stable, compatible and well-founded
;;; orderings. They give a necessary and sufficient condition for
;;; noetherianity of rewriting systems in a given signature.
;;; Remember from newman.lisp or convergent.lisp that we defined
;;; noetherianity of an abstract reduction relation as inclusion in a
;;; well-founded ordering. Now we give a general definition of a
;;; reduction ordering and we prove that every term rewriting system
;;; contained in a reduction ordering describes a noetherian reduction
;;; relation. Note the benefits: once a suitable reduction ordering is
;;; found, noetherianity of a finite TRS can be proved simply checking
;;; that all its elements (a finite amount of rules) are in the
;;; reduction ordering
;;; ---------------------------------------------------------------------
;;; 4.1 Definition of a general reduction ordering red0<
;;; ---------------------------------------------------------------------
;;; The reduction ordering will be defined in the set of terms in a
;;; given signature:
(defun term-s-p-f (x) (term-s-p x))
(encapsulate
((red0< (t1 t2) booleanp)
(fn0 (term) e0-ordinalp))
(local (defun red0< (t1 t2) (declare (ignore t1 t2)) nil))
(local (defun fn0 (term) (declare (ignore term)) 1))
(defthm red0<-well-founded-relation-on-term-s-p
(and
(implies (term-s-p-f t1) (e0-ordinalp (fn0 t1)))
(implies (and (term-s-p-f t1) (term-s-p-f t2) (red0< t1 t2))
(e0-ord-< (fn0 t1) (fn0 t2))))
:rule-classes (:well-founded-relation
:rewrite))
(defthm red0<-stable
(implies (and (term-s-p t1) (term-s-p t2)
(substitution-s-p sigma)
(red0< t1 t2))
(red0< (instance t1 sigma)
(instance t2 sigma))))
(defthm red0<-compatible
(implies (and (term-s-p t1) (term-s-p t2) (term-s-p term)
(position-p pos term)
(red0< t1 t2))
(red0< (replace-term term pos t1)
(replace-term term pos t2))))
(defthm red0<-transitive
(implies (and (term-s-p t1) (term-s-p t2) (term-s-p t3)
(red0< t1 t2) (red0< t2 t3))
(red0< t1 t3))))
(in-theory (disable red0<-transitive))
;;; TECHNICAL REMARK: Note that we needed to define the function
;;; term-s-p-f exactly as the macro term-s-p. From the logical point of
;;; view it is the same. But the checks done for the syntax of a
;;; well-founded relation rule requires that the domain of definition
;;; has to be defined as a function.
;;; IMPORTANT REMARK: The way we have defined reduction orderings can be
;;; an obstacle to show that concrete term rewriting systems are
;;; noetherian: we have to find efectively the function fn0. I think
;;; there is no easier way to show noetherianity of a reduction ordering
;;; or a term rewriting system in the ACL2 logic. This is the main
;;; drawback in our formalization of rewriting.
;;; --------------------------------------------------------------------
;;; 4.2 The main property of reduction orderings
;;; --------------------------------------------------------------------
;;; The following function checks if every rule in a TRS is in the order
;;; defined by the genral reduction ordering red0< defined above.
(defun noetherian-red0< (R)
(if (endp R)
t
(and
(red0< (rhs (car R))
(lhs (car R)))
(noetherian-red0< (cdr R)))))
;;; Our goal is to prove that (noetherian-red0< R) implies noetherianity
;;; of the reduction relation defined by the TRS R. I.e., the following
;;; goal:
; ; (defthm R-noetherian-if-subsetp-of-a-reduction-ordering
; ; (implies (and
; ; (noetherian-red0< R)
; ; (system-s-p R)
; ; (term-s-p term)
; ; (eq-legal term op R))
; ; (red0< (eq-reduce-one-step term op) term)))
;;; Previous lemmas
(local
(encapsulate
()
(defthm e0-ord-<-irreflexive
(implies (e0-ordinalp x)
(not (e0-ord-< x x))))
(defthm red0<-irreflexive
(implies (term-s-p x) (not (red0< x x)))
:hints (("Goal"
:use (:instance red0<-well-founded-relation-on-term-s-p
(t1 x) (t2 x))
:in-theory (disable red0<-well-founded-relation-on-term-s-p))))))
;;; REMARK: We enable occurrence-position-relation because we are going
;;; to do a proof similar to the last part of equational-theories.lisp
;;; (eq-equiv-p is the least congruence relation containing the
;;; equational axioms in E)
(local (in-theory (enable occurrence-position-relation)))
(local
(defthm red0<-contains-noetherian-rule
(implies (and
(noetherian-red0< R)
(member (cons t1 t2) R))
(red0< t2 t1))))
;;; Not very good as rewriting rule, but it works
(local
(defthm member-rewrite-system-noetherian-consp
(implies (and (member rule R)
(not (consp rule)))
(not (noetherian-red0< R)))))
(local
(defthm term-s-p-system-s-p
(implies (and (member (cons l r) S) (system-s-p S) )
(and (term-s-p l) (term-s-p r)))
:hints (("Goal" :induct (system-s-p S)))))
;;; This is the main lemma:
(local
(defthm R-noetherian-if-subsetp-of-a-reduction-ordering-lemma
(implies (and
(noetherian-red0< R)
(system-s-p R)
(member (cons t1 t2) R)
(term-s-p s) (substitution-s-p sigma)
(position-p p s)
(equal (replace-term s p (instance t1 sigma))
term))
(red0< (replace-term s p (instance t2 sigma))
term))))
;;; And, as a particular case, the intended result.
(defthm R-noetherian-if-subsetp-of-a-reduction-ordering
(implies (and
(noetherian-red0< R)
(system-s-p R)
(term-s-p term)
(eq-legal term op R))
(red0< (eq-reduce-one-step term op) term)))
;;; REMARK: To enable or disable:
(defconst *equational-theories-and-rewriting*
'(eq-legal eq-reduce-one-step eq-reducible r-reduce))
;;; IMPORTANT REMARK: we disable eq-reduce-one-step, eq-legal,
;;; r-reduce and eq-reducible: we want these rules to work.
(in-theory
(set-difference-theories
(current-theory :here)
*equational-theories-and-rewriting*))
;;; ============================================================================
;;; 5. Normal form computation
;;; ============================================================================
;;; With the definition of r-reduce above we cold define the function
;;; r-normal-form to compute the normal form of a term w.r.t. a rewrite
;;; system R, in the following way:
; (defun r-normal-form (term R)
; (let ((red (r-reduce term)))
; (if (second red)
; (r-normal-form (first (r-reduce red R)))
; term)))
;;; But this is obviously non-terminanting (for example, if we use a
;;; non-terminating R, we can obtain an infinite chain).
;;; We have to assure that the system is noetherian and that we are
;;; dealing with terms in a the signature where we know that the
;;; reduction ordering is well-founded. Something like this:
; (defun r-normal-form (term R)
; (if (and (noetherian-red0< R) (term-s-p term))
; (let ((red (r-reduce term)))
; (if (second red)
; (r-normal-form (first (r-reduce red R)))
; term))
; nil))
;;; But this is obviously a waste of time in every recursive call. We
;;; adopt two approaches to compute and reason about normal forms in
;;; ACL2.
;;; 1) We will define r-normal-form with only one argument an being R an
;;; "external" rewrite system, known to be noetherian.
;;; 2) Define computation of n reduction steps. When n is big enough, a
;;; normal form can be computed in this way.
;;; So our goal in this section is:
;;; - Define (partially) a noetherian term rewriting system (justified
;;; by the general reduction ordering defined above and define and
;;; verify a function to compute the normal form of a term w.r.t. that
;;; term rewrite system.
;;; - Define computation of n reduction steps and show its relation with
;;; normal form computation.
;;; ---------------------------------------------------------------------
;;; 5.1 Normal form computation w.r.t. noetherian term rewriting systems
;;; ---------------------------------------------------------------------
;;; ·····································································
;;; 5.1.1 A noetherian term rewriting system
;;; ·····································································
(encapsulate
((RN () noetherian-rewrite-system))
(local (defun RN () nil))
(defthm RN-rewrite-system
(rewrite-system-s-p (RN)))
(defthm RN-noetherian-red<
(noetherian-red0< (RN))))
;;; ·····································································
;;; 5.1.2 Normal form w.r.t. a noetherian term rewrite system
;;; ·····································································
(defun RN-normal-form (term)
(declare (xargs :measure (if (term-s-p term) term 0)
:well-founded-relation red0<))
(if (term-s-p term)
(mv-let (reduced reducible)
(r-reduce term (RN))
(if reducible
(RN-normal-form reduced)
term))
term))
;;; REMARK: Note also that RN-normal-form is a typical case of a
;;; function of TWO "arguments" that cannot be admited: the first one is
;;; a term and the second one is a term rewrite system. Since the
;;; function is not terminating in general, unless the second "argument"
;;; is a terminating term rewrite system, such a function of two
;;; arguments cannot be defined. Nevertheles, we can still reason about
;;; the function for the terminating cases: we partially define a
;;; constant, (RN) in this case, having the properties needed for
;;; termination. We define the function, RN-NORMAL-FORM in this case,
;;; without the problematic argument and using the constant in its
;;; body. Admission of the function without using local properties of
;;; the constant ((RN) in this case) can be guaranteed by disabling the
;;; constant and its executable counterpart. Futhermore, reasoning about
;;; the function is done outside encapsulate and then no local
;;; properties of the constant are assumed and only the properties
;;; needed for termination can be used.
;;; The main disadvantage of this approach is that the function is not
;;; execuable. Nevertheless, we can define concrete instances of this
;;; definition, replacing (RN) for a particular terminating TRS.
;;; REMARK: Note how this functions is admited: r-reduce is expressed in
;;; terms of eq-reduce-one-step and eq-reducible, using the two main
;;; properties about r-reduce proved above. Then the main property about
;;; reduction orderings, proved above, is applied
;;; ·····································································
;;; 5.1.2 Properties of RN-normal-form
;;; ·····································································
;;; To verify RN-normal form, we must prove two properties:
;;; - (RN-normal-form term) returns an irreducible term.
;;; - (RN-normal-form term) is equivalent, w.r.t. to the equational
;;; theory of (RN)
;;; Irreducibility
;;; ··············
(defthm RN-normal-form-irreducible
(implies (term-s-p term)
(not (eq-legal (RN-normal-form term) op (RN)))))
;;; Normal form is an equivalent term
;;; ·································
;;; We show an equational proof justifying the equivalence of term and
;;; (RN-normal-form term):
(defun RN-proof-irreducible (term)
(declare (xargs :measure (if (term-s-p term) term 0)
:well-founded-relation red0<))
(if (term-s-p term)
(let ((red (eq-reducible term (RN))))
(if (not red)
nil
(let ((term2 (eq-reduce-one-step term red)))
(cons (make-r-step
:direct t :elt1 term :elt2 term2
:operator red)
(RN-proof-irreducible term2)))))
nil))
(defthm RN-normal-form-equivalent-term
(implies (term-s-p term)
(eq-equiv-s-p term
(RN-normal-form term)
(RN-proof-irreducible term)
(RN))))
;;; ---------------------------------------------------------------------
;;; 5.2 Application of a finite number of reduction steps to compute
;;; normal forms
;;; ---------------------------------------------------------------------
;;; An easy alternative (that will suffice in most practical cases to
;;; compute normal forms) is to apply r-reduce at most a given number of
;;; steps.
;;; The function normal-form-n-steps receives as input a natural number
;;; n, a term and a term rewriting system and returns a multivalue of
;;; two values. If an irreducible elelemt is obtained in less than n
;;; steps, the second value returned is t and the first value is that
;;; irreducible element. Otherwise the second value is nil (and the
;;; first is irrelevant).
;;; ·····································································
;;; 5.1.1 Definition
;;; ·····································································
(defun normal-form-n-steps (n term R)
(declare (xargs :guard (and (term-p term)
(system-p R)
(integerp n) (>= n 0))))
(mv-let (reduced reducible)
(r-reduce term R)
(cond ((not reducible) (mv term t))
((zp n) (mv nil nil))
(t (normal-form-n-steps (- n 1) reduced R)))))
;;; REMARK:
;;; Advantages of this definition:
;;; - It does not need to check noetherianity of the TRS.
;;; - It does not need to check that the term is in the signature.
;;; Disadvantages:
;;; - One needs to know in advance the number of steps needed. But in
;;; most practical case a big number suffices.
;;; ·····································································
;;; 5.1.2 Relating normal-form-n-steps and RN-normal-form
;;; ·····································································
(defthm normal-form-n-steps-RN-normal-form-relation
(implies (and (term-s-p term)
(second (normal-form-n-steps n0 term (RN))))
(equal (first (normal-form-n-steps n0 term (RN)))
(RN-normal-form term))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment