らむにゃー

Schemeでλ計算とか。

;; Church-encoding of nat
(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))
;; (add-1 zero) ->* (lambda (f) (lambda (x) (f x)))
;; (add-1 (add-1 zero)) ->* (lambda (f) (lambda (x) (f (f x))))
;; Define addtion of Church numerals
(define (add-ch n m) (lambda (f) (lambda (x) ((m f) ((n f) x)))))
;; Define multiplication of Church numerals
(define (mul-ch n m) (lambda (f) (lambda (x) ((m (n f)) x))))
;; Define exponentiation of Church numerals
(define (exp n m) (lambda (f) (lambda (x) (((m n) f) x))))

;; Truth Definition in Church encoding
(define t-ch (lambda (p) (lambda (q) p)))
(define nil-ch (lambda (p) (lambda (q) q)))
(define if-ch (lambda (p) (lambda (x) (lambda (y) ((p x) y)))))
;; Define isZero? in Church encoding
(define (isZero? n)
  (define false-constant (lambda (f) nil-ch))
  ((n false-constant) t-ch))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Define encoding, decoding of numerals
(define (encode-num n)
  (if (= n 0) zero
      (add-1 (encode-num (- n 1)))))
(define (decode-num n)
  (define (plus-one x) (+ x 1))
  ((n plus-one) 0))

;; Define encoding, decoding truth values
(define (encode-tval p) (if p t-ch nil-ch))
(define (decode-tval p) ((p #t) #f))

;;;;;;;;;;;;; あまりにしょぼいので加筆 ;;;;;;;;;;;;;;;;;;;;;;;;;

;; Define pairing functions and car, cdr
(define cons-ch (lambda (x) (lambda (y) (lambda (f) ((f x) y)))))
(define car-ch (lambda (p) (p t-ch)))
(define cdr-ch (lambda (p) (p nil-ch)))

;; Define Predecessor function
(define (pred-ch m)
  (define zz ((cons-ch zero) zero))
  (define ss (lambda (p) ((cons-ch (cdr-ch p)) (add-1 (cdr-ch p)))))
  (car-ch ((m ss) zz)))

Churchエンコーディングの話。
簡単なことしかやってませんがお許しを。結果は以下：

gosh> (decode-num (add-ch (encode-num 3)(encode-num 5)))
> 8

gosh> (decode-tval (isZero? (encode-num 0)))
> #t

gosh> (decode-tval (isZero? (encode-num 1)))
> #f

なんか本当にクソですね、すみません、死にます。
死にゃん