;; lambda.lsp - newLISPでラムダ計算をしてみるテスト

;; newLISPの以下の性質を利用することで、動的束縛を静的束縛のように振舞わせる
;; * 読取器が大文字小文字を区別すること
;; * ラムダ式がオープン(リストのサブタイプ)であり、変更が容易なこと
;; * 大文字から始まるシンボルを展開する関数(expand)が用意されている

;; 当然ながら、変数が重複するとシンボルの展開がおかしくなるのでエラー
;; 場合によってはラムダ式の仮引数が展開されて妙なことに (しかもエラーの通知がない)

;; 参考リンク
;; - Lambda calculus - http://en.wikipedia.org/wiki/Lambda_calculus
;; - ラムダ計算 - http://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97
;; - Y Function - http://www.newlisp.org/index.cgi?Y_Function


(define-macro (LAMBDA)
  (append (lambda ) (expand (args))))

(define DEFINE define)


;;;##自然数と算術 (number)

(DEFINE ZERO  (LAMBDA (F) (LAMBDA (X) X)))             ; 0 := λfx.x
(DEFINE ONE   (LAMBDA (F) (LAMBDA (X) (F X))))         ; 1 := λfx.fx
(DEFINE TWO   (LAMBDA (F) (LAMBDA (X) (F (F X)))))     ; 2 := λfx.f(fx)
(DEFINE THREE (LAMBDA (F) (LAMBDA (X) (F (F (F X)))))) ; 3 := λfx.f(f(fx))

(DEFINE (SUCC N) (LAMBDA (F) (LAMBDA (X) (F (N F X))))) ; SUCC := λnfx.f (n f x)

(DEFINE (PLUS M N) (LAMBDA (F) (LAMBDA (X) ((M F) ((N F) X))))) ; PLUS := λmnfx.m f (n f x)
(DEFINE (MULT M N) (LAMBDA (F) (LAMBDA (X) ((N (M F)) X))))     ; MULT := λmnf.m (n f)
(DEFINE (POW B E) (E B))                                        ; POW := λbe.e b

(define (to-number x) ((x (lambda (n) (+ n 1))) 0))
(define (to-lambda n) (if (< 0 n) (SUCC (to-lambda (- n 1))) (ZERO)))

(to-number ZERO)                        ;=> 0
(to-number ONE)                         ;=> 1
(to-number TWO)                         ;=> 2
(to-number (PLUS ONE TWO))              ;=> 3


;;;##論理記号と述語 (boolean)

(DEFINE TRUE (LAMBDA (X Y) X))          ; TRUE := λx y. x
(DEFINE FALSE (LAMBDA (X Y) Y))         ; FALSE := λx y. y

(DEFINE (AND P Q) (P Q FALSE))          ; AND := λp q. p q FALSE
(DEFINE (OR P Q) (P TRUE Q))            ; OR := λp q. p TRUE q
(DEFINE (NOT P) (P FALSE TRUE))         ; NOT := λp. p FALSE TRUE
(DEFINE (IF P X Y) (P X Y))             ; IFTHENELSE := λp x y. p x y

(DEFINE ZEROP (LAMBDA (N) (N (LAMBDA (X) FALSE) TRUE)))

(define bool (lambda (p) (p "TRUE" "FALSE")))

;(IF TRUE (LAMBDA () (+ 10 2)) (LAMBDA () (* 10 2)))

;(bool (AND TRUE FALSE))             ;=> "FALSE"
;(bool (OR TRUE FALSE))              ;=> "TRUE"
;(bool (OR FALSE FALSE))             ;=> "FALSE"
;(bool (NOT FALSE))                  ;=> "TRUE"
;(bool (ZEROP (PLUS ZERO ZERO)))     ;=> "TRUE"

;;;##対 (pair)

(DEFINE (CONS X Y) (LAMBDA (M) (M X Y))) ; CONS := λx y m. m x y
(DEFINE (CAR P) (P TRUE))                ; CAR := λp. p TRUE
(DEFINE (CDR P) (P FALSE))               ; CDR := λp. p FALSE

;(CDR (CONS (CONS 1 2) 3))               ;=> 3


;;;##再帰 (recursion)

;; *** あまり再帰が深いとスタックを食い潰すので使えない

(define IF if)

(DEFINE Y
  (LAMBDA (F)
    ((LAMBDA (H) (LAMBDA (X) ((F (H H)) X)))
     (LAMBDA (H) (LAMBDA (X) ((F (H H)) X))))))

(DEFINE FACT
  (Y (LAMBDA (F)
       (LAMBDA (N)
         (IF (= N 0) 1 (* N (F (- N 1))))))))

;; (define F
;;   (lambda (Q)
;;     (LAMBDA (n)
;;       (if (= n 1) 1 (* n ((Q Q) (- n 1)))))))
;((F F) 10)         ;=> 3628800

;;; EOF