;22-5-1
;Ulrich Berger (University of Wales Swansea)
;
;Higher type Programs for ordinal hierarchies of number theoretic functions
;
;Appendix to the paper (http://www-compsci.swan.ac.uk/~csulrich/recent-papers.html)
;
;"Program extraction from Gentzen's proof of transfinite induction up to epsilon_0"
;
;submitted to the Dagstuhl seminar "Proof Theory in Computer Science", 
;7.10.2001-12.10.2001, organized by R. Kahle (München), P. Schroeder-Heister (Tübingen), 
;R. Stärk (Zürich) .


;The following are implementations of ordinal recursive and higher type definitions
;of the fast growing and similara hierarchies, as described in the paper mentioned above.

;The programs are written in the functional language Scheme (tp://www.scheme.com./)

(begin

;Preliminaries

(define (iterate u k v)
  (if (zero? k)
      v
      (iterate u (- k 1) (u v))))

(define (exp2 k)
  (if (zero? k)
      1
      (* 2 (exp2 (- k 1)))))


;Step functions

(define phi-zero
  (lambda (k) k)) ;slow and Hardy
;  (lambda (k) (exp2 k)) ;fast


(define (phi-suc g) 
;  (lambda (k) (+ (g k) 1))) ;slow
;  (lambda (k) (iterate g k k))) ;fast
  (lambda (k) (g (+ k 1)))) ;Hardy

(define (phi-lim h)
  (lambda (n) ((h n) n))) ;slow, fast and Hardy

;Ordinal functions

(define (zero-ord? x) (and (integer? x) (zero? x)))
(define (non-zero-ord? x) (and (list x) (= (length x) 2)))

(define last-exp car)
(define rest-sum cadr)

(define cons-ord list) 


;Definition of the hierarchy using fundamental sequences

(define (suc-ord? x)
  (and (non-zero-ord? x)
       (zero-ord? (last-exp x))))

(define (lim-ord? x)
  (and (non-zero-ord? x)
       (non-zero-ord? (last-exp x))))


(define pred-ord rest-sum) 

(define (fund-seq x k)
  (let ((y (last-exp x))
	(z (rest-sum x)))
    (cond ((suc-ord? y) (iterate (lambda (u) (cons-ord (pred-ord y) u)) k z))
	  ((lim-ord? y) (cons-ord (fund-seq y k) z)))))


;It's interesting to watch what happens if the display below is switched on
; i.e. the ";" is removed

(define (hier-fund x)
;  (display x) (newline) (newline)     
  (cond ((zero-ord? x) phi-zero)
	((suc-ord? x) (phi-suc (hier-fund (pred-ord x))))
	((lim-ord? x) (phi-lim (lambda (k) (hier-fund (fund-seq x k)))))))

;Definition of the hierarchy using higher type functionals

(define (r n)
  (if (zero? n)
      phi-lim
      (lambda (u)
	(lambda (v)
	  ((r (- n 1)) (lambda (k) ((u k) v)))))))

(define (t n)
  (cond ((= 0 n) phi-zero)
	((= 1 n) phi-suc)
	((< 1 n) (lambda (u)
		   (lambda (v)
		     ((r (- n 2)) (lambda (k) (iterate u k v))))))))

(define (t2 n x)
  (if (zero-ord? x)
      (t n)
      ((t2 (+ n 1) (last-exp x)) (t2 n (rest-sum x)))))

(define (hier-high x)
  (t2 0 x))


;Material for testing

(define x '(((0 0) 0) 0))
(define y '((0 0) 0))
(define z '((0 0) (0 0)))

(define (omega n)
  (if (zero? n)
      '(0 0)
      (cons-ord (omega (- n 1)) 0)))

(define (omega1 n)
  (if (zero? n)
      '(0 0)
      (cons-ord (omega1 (- n 1)) (omega1 (- n 1)))))


)

;this won't terminate in reasonable time:
((hier-fund x) 3)


((hier-fund y) 10)

;also this takes too long:
((hier-fund (omega1 3)) 1)

((hier-high z) 3)

(omega1 3)

;here the result is always 2, interesting are the run times.
((hier-fund (omega 10000)) 1)
((hier-high (omega 10000)) 1)

;run time for ((hier-fund/high (omega n)) 1)  (Hardy)
; n    fund   high  
;
; 500     2      1   seconds
;1000     5      2
;1500     9      4
;2000    14      6
;2500    22      7
;3000    35      9
;10000  360    175
; comment: when I ran the examples on lmu-scheme the differences
; between the runtimes where more significant (factor 4.5)