Natural Number Encoding by the series convergent to 1 / 自然数を 1に収束する級数で符号化

fraction-encoding.scm

;;;;
;;;; s_0 = 0
;;;; s_1 = 1/2
;;;; s_2 = 1/2 + 1/4 = 3/4
;;;; s_3 = 1/2 + 1/4 + 1/8 = 7/8
;;;; ...
;;;; s_n = 1/2 + 1/4 + ... + 1/2^n = (1-2^n)/2^n
;;;;
;;;; この s_n で自然数 n を表すことにするというもの。
;;;; s_ω = 1 となって無限の順序数を考察するのに直観が働きやすいことから，自然数のモデルの例の1つとしてしばしば挙げられる。
;;;;
;;;; add(s_m, s_n) = s_{m+n} となる関数 add を，モデル {s_n} 上の加算と定義すれば，自然数の加算と全く同じ性質が成り立つ。
;;;; 他の演算子も同じように定義してやれば，{s_n} を自然数と同一視できる。
;;;;

;;;;
;;;; ペアノの公理により，最初の自然数 (zero) および，次の自然数を得る関数 (succ) が与えれば，自然数を定義できる。
;;;; オリジナルのペアノの公理では自然数は 1から始まるが，算術演算を定義する目的からは，0も自然数に含めた方が良い。
;;;; プログラムによって関数定義するためには，前の自然数を得る関数 (pred) も必要。
;;;;
;;;; succ: 次の自然数を得る関数 (successor)
;;;; pred: 前の自然数を得る関数 (predecessor)
;;;;
;;;; zero := s_0 = 0
;;;;
;;;; succ(s_n) の位置を図形的に考えると，s_n と 1 の中点，すなわち平均値なので
;;;; succ(s_n) = (1 + s_n) / 2
;;;; 
;;;; ∴ pred(s_n) = 2 * s_n - 1
;;;;

(define (succ s) (* 1/2 (+ s 1)))
(define (pred s) (- (* 2 s) 1))

(define zero  0)
(define one   (succ zero))    ; 1/2
(define two   (succ one))     ; 3/4
(define three (succ two))     ; 7/8
(define four  (succ three))   ; 15/16
(define five  (succ four))    ; 31/32
(define six   (succ five))    ; 63/64
(define seven (succ six))     ; 127/128
(define eight (succ seven))   ; 255/256
(define nine  (succ eight))   ; 511/512
(define ten   (succ nine))    ; 1023/1024

(define (number->code n)
  (if (zero? n)
      zero
      (succ (number->code (- n 1)))))

;;;
;;; quick version of number->code
;;;
;;; s_n = 1 - 1/2^n = 1 - 2^(-n)
;;;
(define (encode n)
  (- 1 (expt 2 (- n))))

;;;
;;; lt?: less-than
;;;
;;; 順序関係は s_n の大小関係に従う
;;;
;;; m < n  iff.  s_m < s_n 
;;;
(define (lt? m n)  (< m n))