peano-arithmetic.scm

;;;;
;;;; Primitive Recursive Functions:
;;;; 
;;;; ペアノの公理を満たす自然数から，原始再帰関数を使って算術演算を定義したり，
;;;; 原始再帰的でない Hyper演算子や Ackermann 関数を定義する。
;;;;

;;;;
;;;; Peano Axiom:
;;;;
;;;; zero: a constant, the first value of natural numbers.
;;;; succ: the successor function.
;;;;
;;;; 1. ∃zero ∈ N
;;;; 2. ∀n ∈ N, ∃succ(n) ∈ N.
;;;; 3. ∀n ∈ N: succ(n) ≠ zero.
;;;; 4. ∀m, n: m ≠ n => succ(m) ≠ succ(n)
;;;; 5. P(0) and (∀n ∈ N: P(n) => P(succ(n))) => ∀n ∈ N: P(n)
;;;;

(define zero 0)
(define (succ n) (+ 1 n))

(define (pred n) (max 0 (- n 1)))

;;;;
;;;; Arithmetic Operators
;;;;
;;;; (n') means succ(n)
;;;;

;;;
;;; 0 + n  := n
;;; m' + n := (m+n)'
;;;
(define (add m n)
  (if (equal? m zero)
      n
      (succ (add (pred m) n))))

;;;
;;; m - 0   := m
;;; m' - n' := m - n
;;;
(define (sub m n)
  (if (equal? n zero)
      m
      (pred (sub m (pred n)))))

;;;
;;; 0  * n := 0
;;; m' * n := n + (m * n)
;;;
(define (mul m n)
  (if (equal? m zero)
      zero
      (add n (mul (pred m) n))))

;;;
;;; m ^ 0  := 1
;;; m ^ n' := m * (m ^ n)
;;;
(define (pow m n)
  (if (equal? n zero)
      (succ zero)
      (mul m (pow m (pred n)))))

;;;
;;; 0!  := 1
;;; n'! := n' * n!
;;;
(define (fac n)
  (if (equal? n zero)
      (succ zero)
      (mul n (fac (pred n)))))

;;;
;;; m < 0   := #f
;;; 0 < n'  := #t
;;; m' < n' := m < n
;;;
(define (lt? m n)
  (cond [(equal? n zero) #f]
        [(equal? m zero) #t]
        [else (lt? (pred m) (pred n))]))

;;;
;;; 0 - n   := 0   (exceptional)
;;; m - 0   := m
;;; m' - n' := m - n
;;;
(define (sub m n)
  (cond [(equal? m zero) zero]
        [(equal? n zero) m]
        [else (sub (pred m) (pred n))]))

;;;
;;; diff m n = | m - n |
;;;
(define (diff m n)
  (cond [(equal? n zero) m]
        [(equal? m zero) n]
        [else (diff (pred m) (pred n))]))

;;;
;;; remainder n m = n                (n < m)
;;;               = remainder n-m m  (otherwise)
;;;
;;; if m = 0, rem does not stop (fails into the infinite loop).
;;;
(define (rem n m)
  (if (lt? n m)
      n
      (rem (sub n m) m)))

;;;
;;; quotient n m = 0                     (n < m)
;;;              = 1 + (quotient n-m m)  (otherwise)
;;;
;;; if m = 0, quo does not stop (fails into the infinite loop).
;;;
(define (quo n m)
  (if (lt? n m)
      zero
      (succ (quo (sub n m) m))))


;;;;
;;;; The Hyper Operators
;;;; 
;;;; hyper0(m, n) = n + 1   ; the successor of n
;;;; hyper1(m, n) = m + n   ; addition        (n-times successor)
;;;; hyper2(m, n) = m * n   ; multiplication  (n-times addition)
;;;; hyper3(m, n) = m ^ n   ; exponential     (n-times multipication)
;;;; hyper4(m, n) = m ^^ n  ; n-times exponential of m
;;;; hyper5(m, n) = m ^^^ n ; n-times hyper4 of m
;;;;
;;;; Question: to define hyper-N(m, n)
;;;;

(define (hyper0 m n) (+ n 1))
(define (hyper1 m n) (+ m n))

(define (hyper2 m n)
  (if (zero? n)
      0
      (hyper1 m (hyper2 m (- n 1)))))

(define (hyper3 m n)
  (if (zero? n)
      1
      (hyper2 m (hyper3 m (- n 1)))))

(define (hyper4 m n)
  (if (zero? n)
      1
      (hyper3 m (hyper4 m (- n 1)))))

;;;
;;; fast version of hyper4
;;;
(define (hyper4 m n)
  (if (zero? n)
      1
      (expt m (hyper4 m (- n 1)))))

(define (hyper1 m n)
  (if (zero? n)
      m
      (hyper0 m (hyper1 m (- n 1)))))

(define (hyper m level n)
  (cond [(zero? level) (+ n 1)]
        [(zero? n)
         (cond [(= level 1) m]
               [(= level 2) 0]
               [else        1])]
        [else (hyper m (- level 1) (hyper m level (- n 1)))]))

;;;
;;; Ackermann function:
;;; ack(m, n) = hyper_m(2, n+3) - 3
;;; 
(define (ack m n)
  (cond [(zero? m) (+ n 1)]
        [(zero? n) (ack (- m 1) 1)]
        [else      (ack (- m 1) (ack m (- n 1)))]))