sasaki-shigeo

;;;;
;;;; 自然数の符号化
;;;; ツェルメロ (Zermelo) による方法
;;;;
;;;; ノイマンの方式と比べると，順序の判定をするのに減算が必要なところが不便である。
;;;;

(define (succ x)
  (list x))

sasaki-shigeo

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

;;;;
;;;; Peano Axiom:
;;;;

sasaki-shigeo

;;;;
;;;; little endian binary list style
;;;;

(define (succ xs)
  (cond [(null? xs)     (cons 1 xs)]
        [(= (car xs) 1) (cons 0 (succ (cdr xs)))]
        [else           (cons 1 (cdr xs))]))

(define zero '())

sasaki-shigeo

;;;;
;;;; 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つとしてしばしば挙げられる。

sasaki-shigeo

;;;;
;;;; Church encoding
;;;;
;;;; ラムダ計算で自然数を符号化する方法
;;;;
;;;; 基本的アイディア：
;;;; one(f, x) = f(x)
;;;; two(f, x) = f(f(x))
;;;; three(f, x) = f(f(f(x)))
;;;; ...

sasaki-shigeo

;;;;
;;;; 自然数の符号化
;;;; ノイマン・スタイル
;;;;
;;;; 符号化した式が爆発して大変だが，これは集合での符号化を目的に考案されたものだから。
;;;; 集合では { x, x } = { x } なので，前者後者が区別されるような工夫が必要とされた。
;;;;

(define (succ x)
  (cons x x))

sasaki-shigeo

;;;;
;;;; 自然数の符号化
;;;; s の個数で自然数の値を表す
;;;; 空リストは 0を表す
;;;;

(define (succ x) (cons 's x))

(define zero  '())
(define one   (succ zero))  ; => (s)

sasaki-shigeo

;;;;
;;;; 自然数を評価可能な S式で符号化する
;;;;

(define (succ n) (list 's n))

(define zero  0)
(define one   (succ zero))    ; => (s 0)
(define two   (succ one))     ; => (s (s 0))
(define three (succ two))     ; => (s (s (s 0)))

sasaki-shigeo

float unit = 10;

void setup() {
  size(500, 500);
  noLoop();
}

void draw() {
  translate(10, 10);
  hilbert(20, 20, 480, 4);

sasaki-shigeo

(require srfi/1)        ; list library
(require srfi/13)       ; string library
(require srfi/26)       ; cut (function placeholder)
(require srfi/42)       ; comprehension
(require srfi/45)       ; lazy -- efficient `delay' for tail calls
;;(require rnrs/hashtables-6)
(require srfi/69)       ; hash-table

;;;
;;; power modulo: a^n mod m