; Multiset Ordering and Iterative Implementation of Ackermann's
;  Function.
; Copyright (C) 2004  John R. Cowles, University of Wyoming

; This program is free software; you can redistribute it and/or 
; modify it under the terms of the GNU General Public License as
; published by the Free Software Foundation; either version 2 of
; the License, or (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free 
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
; USA.

; Written by: John R. Cowles
; email:      cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.

(in-package "ACL2")

#|
 Using the Multiset Ordering in ACL2,

    by John R. Cowles, University of Wyoming, April 1997.

 Let S be a well-founded ordered set. Zohar Manna, in his 
 monograph: Lectures on the Logic of Computer Programming, SIAM, 
 1980, ISBN: 0-89871-164-9, considers a well-founded ordering on 
 bags of elements from S that is useful for termination proofs.

 Let M and M' be bags of elements from S. Under the MULTISET 
 ORDERING, M > M', iff M' can be obtained from M by the removal of 
 at least one occurrence of an element from M and/or the 
 replacement of at least one occurrence of an element in M with any
 FINITE number of smaller elements.

 Eg. Let S be the set of all nonnegative integers. Then 

     {4,2,2,2,0,0} > {4,2,2}           because 2,0,0 are removed
{4,2,1,1,1,0,0}   because 2 is replaced by
                                        1,1,1,0,0
{3,3,2,2,2}       because 4 is replaced by
                                        3,3,2,2,2 and 1,1,1,0,0
                                        is removed.

 Manna states the following:

 Theorem. Let S be a partial ordering. Then the multiset ordering
          on bags of elements from S is well-founded iff S is
          well-founded.

 Bags are implemented in ACL2 using lists by simply ignoring the 
 order in which the elements of a given list are listed. For 
 example, '(a a b c c) and '(a b c a c) are equal as bags. If the 
 purported bag is a consp that is not a true list, such as 
 '(a a b c c . d) then the final cdr is ignored, ie. 
 '(a a b c c . d) is treated as the bag '(a a b c c).

 It is assumed that the reader is familiar with the implementation 
 of  the ordinals less than esilon-0 in ACL2. See E0-ORD-< and 
 E0-ORDINALP in the ACL2 documentation.

 The multiset ordering is implemented in ACL2 by mapping bags 
 (ie. lists) into the ordinals less than epsilon-0 using the 
 following two step process:

 1. Transform bags into bags of ordinals by leaving elements that 
    are noninteger ordinals alone and replacing all other elements 
    by adding 1 to their acl2-count. Also the final cdr of the bag
    is replaced by the acl2-count of that final cdr. So '(0 1 1 2)
    is transformed into '(1 2 2 3 . 0) and '(0 1 1 2 . 3) is 
    transformed into '(1 2 2 3 . 3).

 2. Order the ordinals in a bag of ordinals in nonincreasing order,
    ignoring the final cdr. So '(1 2 2 3 . 3) becomes 
    '(3 2 2 1 . 3).

 The effects of this process are achieved in ACL2 with the next two
 definitions. 
|#

(defun
  insert-E0-ord-< ( x lst )
  (declare (xargs :guard t))
  (if (consp lst)
      (if (e0-ord-< (car lst) x)
	  (cons x lst)
	  (cons (car lst)
		(insert-E0-ord-< x (cdr lst))))
      (cons x lst)))

(defun
  ordinate ( x )
  (declare (xargs :guard t))
  (if (consp x)
      (if (and (consp (car x))
	       (e0-ordinalp (car x)))
	  (insert-E0-ord-< (car x)
			   (ordinate (cdr x)))
	  (insert-E0-ord-< (+ 1 (acl2-count (car x)))
			   (ordinate (cdr x))))
      (acl2-count x)))

#|
 The next three theorems show that the range of ORDINATE is 
 included, as a subset, in the ordinals less that epsilon-0:
|#

(defthm
  Asymmetry-of-E0-ord-<
  (implies (e0-ord-< x y)
	   (not (e0-ord-< y x)))
  :rule-classes :forward-chaining)

(defthm
  E0-ordinalp-insert-E0-ord-<
  (implies (and (e0-ordinalp x)
		(not (equal x 0))
		(e0-ordinalp lst))
	   (e0-ordinalp (insert-E0-ord-< x lst))))

(defthm
  E0-ordinalp-ordinate
  (e0-ordinalp (ordinate x)))

#|
 The utility of the multiset ordering is demonstrated by showing 
 that an iterative (ie., tail recursive) program to compute 
 Ackermann's function is correct. This  demonstration is based on 
 ideas in Manna's monograph, pages 13-14.

 Here is the ``recursive'' definition of Ackermann's function
 (together with a type-prescription and guard verification):
|#

(defun
  pair ( x y )
  (declare (xargs :guard t))
  (cons (+ 1 (acl2-count x))
	(acl2-count y)))

(defun
  A ( x y )
  "The R. Peter version (1935) of Ackermann's function."
  (declare (xargs :guard (and (integerp x)
			      (>= x 0)
			      (integerp y)
			      (>= y 0))
		  :measure (pair x y)
		  :verify-guards nil))
  (if (zp x)
      (+ 1 y)
      (if (zp y)
	  (A (- x 1) 1)
	  (A (- x 1)(A x (- y 1))))))

(defthm
    Non-neg-int-A
    (implies (and (integerp y)
                  (>= y 0))
             (and (integerp (A x y))
                  (>= (A x y) 0)))
    :rule-classes :type-prescription)

(verify-guards A)

#|
 The iterative version of Ackermann's function is an implementation
 in ACL2, using tail recursion, of the following algorithm:

 A-iter( x y )
   {x and y are nonnegative integers}
   stk <- (x)
   top <- y

   {Loop invariant:                          }
   {[stk = (s_n,...,s_2,s_1) and             }
   { A(x,y)= A(s_n,...,A(s_2,A(s_1,top))...)]} 
   {or                                       }
   {[stk = empty and A(x,y) = top]           }
   while  stk is not empty  do
     if  head( stk ) = 0  then
        stk <- tail( stk )
        top <- top + 1
        {stk = (s_n,...,s_2) or stk = empty}
     else if  top = 0  then
         s  <- head( stk )
        stk <- tail( stk )
        stk <- cons( s - 1, stk )
        top <- 1
        {stk = (s_n,...,s_2,s_1 - 1)}
     else
         s  <- head( stk )
        stk <- tail( stk )
        stk <- cons( s - 1, stk )
        stk <- cons( s, stk )
        top <- top - 1
        {stk = (s_n,...,s_2,s_1 - 1,s_1)}
     end if
   end while
   return[ top ]

 The while loop is implemented in ACL2 with tail recursion
 (with TOP being a nonnegative integer and STK being a list
  of nonnegative integers): 

 (defun
   A-loop ( stk top )
   (if (consp stk)
       (cond ((zp (car stk))
	     (A-loop (cdr stk) 
		     (+ 1 top)))
	    ((zp top)
	     (A-loop (cons (- (car stk) 1)(cdr stk))
		     1))
	    (t
	     (let ((second (car stk)))
	          (A-loop (list* second
				 (- second 1)
				 (cdr stk))
			  (- top 1)))))
       top))

 The iterative version of A, A-iter is obtained by initializing
 STK and TOP in A-loop:

 (defun 
   A-iter( x y )
   "Iterative (ie, tail recursive) version of Ackermann's 
    function."
   (declare (xargs :guard (and (integerp x)
			      (>= x 0)
			      (integerp y)
			      (>= y 0))))
   (A-loop (list x) y))

 To show that A-iter is correct requires two proofs:
  1. A-loop terminates whenever TOP is a nonnegative integer and 
     STK is a list of nonnegative integers.
  2. A(x,y) = A-iter(x,y) whenever both x and y are nonnegative
     integers.

 To prove termination, use is made of the multiset ordering on 
 bags of pairs formed from STK and TOP in the following way:

  If STK = (s_n,...,s_2,s_1), then the bag is
       ( pair(s_n + 1,0),...,pair(s_2 + 1,0),pair(s_1,TOP) ).

 The details in ACL2 follow: 
|#

(defun
  pair1 ( x y )
  (declare (xargs :guard t))
  (cons (+ 2 (acl2-count x))
	(acl2-count y)))

(defun
  pair-with-0-lst ( lst )
  (declare (xargs :guard t))
  (if (consp lst)
      (cons (pair1 (car lst) 0)
	    (pair-with-0-lst (cdr lst)))
      nil))

(defun
  pair-lst ( lst x )
  (declare (xargs :guard t))
  (if (consp lst)
      (cons (pair (car lst) x)
	    (pair-with-0-lst (cdr lst)))
      nil))

(defun
  Non-neg-int-listp ( lst )
  (declare (xargs :guard t))
  (if (consp lst)
      (let ((first (car lst)))
	   (and (integerp first)
		(>= first 0)
		(non-neg-int-listp (cdr lst))))
      t))

(defthm
  Transitivity-of-E0-ord-<
  (implies (and (e0-ord-< x y)
		(e0-ord-< y z))
	   (e0-ord-< x z))
  :rule-classes :forward-chaining)

(defthm
  E0-ord-<-insert-E0-ord-<-a
  (implies (e0-ord-< x y)
	   (e0-ord-< (insert-e0-ord-< x ord)
		     (insert-e0-ord-< y ord))))

(defthm
  E0-ord-<-insert-E0-ord-<-b
  (implies (and (e0-ord-< x z)
		(e0-ord-< y z))
	   (e0-ord-< (insert-e0-ord-< x
				      (insert-e0-ord-< y ord))
		     (insert-e0-ord-< z ord))))

(defthm
  E0-ord-<-insert-E0-ord-<-c
  (implies (e0-ord-< y z)
	   (e0-ord-< (insert-e0-ord-< y ord)
		     (insert-e0-ord-< x
				      (insert-e0-ord-< z ord)))))

(defthm
   Associate-constants-left-+
   (implies (and (syntaxp (and (consp x)
			       (eq (car x) 'quote)))
		 (syntaxp (and (consp y)
			       (eq (car y) 'quote))))
	    (equal (+ x y z)
		   (+ (+ x y) z))))

(defthm
  A-special-case-a
  (implies (and (integerp stk1)
		(< 0 stk1))
	   (e0-ord-< (insert-e0-ord-< (cons stk1 1)
				      ord)
		     (insert-e0-ord-< (cons (+ 1 stk1) 
					    (acl2-count top))
				      ord)))
  :hints (("goal"
	   :use (:instance 
		 e0-ord-<-insert-e0-ord-<-a
		 (x (cons stk1 1))
		 (y (cons (+ 1 stk1) 
			  (acl2-count top))))
	   :in-theory (disable e0-ord-<-insert-e0-ord-<-a))))

(defthm
  A-special-case-b
  (implies
   (and (integerp stk1)
        (< 0 stk1)
        (integerp top)
        (< 0 top))
   (e0-ord-<
    (insert-e0-ord-< (cons (+ 1 stk1) (+ -1 top))
		     (insert-e0-ord-< (cons (+ 1 stk1) 0)
				      ord))
    (insert-e0-ord-< (cons (+ 1 stk1) top)
		     ord)))
 :hints (("goal"
	  :use (:instance 
		e0-ord-<-insert-e0-ord-<-b
		(x (cons (+ 1 stk1) (+ -1 top)))
		(y (cons (+ 1 stk1) 0))
		(z (cons (+ 1 stk1) top)))
	  :in-theory (disable e0-ord-<-insert-e0-ord-<-b))))

(defthm
  A-special-case-c
  (e0-ord-< (insert-e0-ord-< (cons (+ 1 (acl2-count stk3))
				   (acl2-count (+ 1 top)))
			     ord)
	    (insert-e0-ord-< x
			     (insert-e0-ord-< 
			      (cons (+ 2 (acl2-count stk3)) 0)
			      ord)))
  :hints (("goal"
	   :use (:instance 
		 e0-ord-<-insert-e0-ord-<-c
		 (y (cons (+ 1 (acl2-count stk3))
			  (acl2-count (+ 1 top))))
		 (z (cons (+ 2 (acl2-count stk3)) 0)))
	   :in-theory (disable e0-ord-<-insert-e0-ord-<-c))))

(defun
  A-loop ( stk top )
  (declare (xargs :guard (and (integerp top)
			      (>= top 0)
			      (non-neg-int-listp stk))
		  :measure (ordinate (pair-lst stk top))))
  (if (consp stk)
      (cond ((zp (car stk))
	     (A-loop (cdr stk) 
		     (+ 1 top)))
	    ((zp top)
	     (A-loop (cons (- (car stk) 1)(cdr stk))
		     1))
	    (t
	     (let ((second (car stk)))
	          (A-loop (list* second
				 (- second 1)
				 (cdr stk))
			  (- top 1)))))
      top))

(defun 
  A-iter( x y )
  "Iterative (ie, tail recursive) version of Ackermann's function."
  (declare (xargs :guard (and (integerp x)
			      (>= x 0)
			      (integerp y)
			      (>= y 0))))
  (A-loop (list x) y))

#|
 Having just established that A-iter terminates, we show it 
 computes Ackermann's function, ie., A(x,y) = A-iter(x,y) whenever
 both x and y are nonnegative integers.
|#

(defun
  concat ( x y )
  (declare (xargs :guard t))
  (if (consp x)
      (cons (car x)
	    (concat (cdr x)
		    y))
      y))

(defthm
  A-loop-A-loop-concat
  (equal (A-loop stk2 (A-loop stk1 top))
	 (A-loop (concat stk1 stk2) top)))

(defthm
  A-special-case
  (implies (and (integerp y) 
		(<= 0 y))
	   (equal (A-loop '(0) y)
		  (A-loop nil (+ 1 y)))))

(defthm
  A-iter=A
  (implies (and (integerp x)
		(>= x 0)
		(integerp y)
		(>= y 0))
	   (equal (A-iter x y)
		  (A x y))))