ラムダ計算で除算・剰余

sub、iszero、あと再帰でなんとか書けた。

; TRUE := λx y.x
(defvar true
  (lambda (x) (lambda (y) x)))

; FALSE := λx y.y
(defvar false
  (lambda (x) (lambda (y) y)))

; ISZERO := λn.n (λx.false) true
(defvar iszero
  (lambda (n)
    (app n ($ true false) true)))

; PRED := λn f x.n (λg h.h (g f)) (λu.x) (λu.u)
(defvar pred
  (lambda (n)
    (lambda (f)
      (lambda (x)
        (app n
             (lambda (g)
               (lambda (h)
                 ($ h g f)))
             (lambda (u) x)
             (lambda (u) u))))))

; SUB := λm n.n pred m
(defvar sub
  (lambda (m)
    (lambda (n)
      (app n pred m))))

; ISZERO := λn.n TRUE FALSE
(defvar iszero
  (lambda (n)
    (app n ($ true false) true)))

; MOD := λm n.ISZERO (SUB m n)
;                     (ISZERO (SUB n m) zero m)
;                     (MOD (SUB m n) n)
(defvar mod
  (lambda (m)
    (lambda (n)
      (funcall
        (app (app iszero (app sub m n))
             (lambda () (app iszero (app sub n m) zero m))
             (lambda () (app mod (app sub m n) n)))))))

; DIV := λm n.ISZERO (SUB m n)
;                     (ISZERO (SUB n m) one zero)
;                     (SUCC (DIV (SUB m n) n))
(defvar div
  (lambda (m)
    (lambda (n)
      (funcall
        (app (app iszero (app sub m n))
             (lambda () (app iszero (app sub n m) one zero))
             (lambda () (app succ (list div (app sub m n) n))))))))

(time (app mod (cn 40) (cn 11) #'1+ 0))
; 7
; "47 msec"

重っ！

再帰使ってるとこを遅延評価しないと無限ループになっちゃうんでapply使っちゃったんだけど、Grassで遅延評価って…?

MOD := λm n.(λp.p (ISZERO (SUB n m) zero m)
                    (p FALSE MOD (SUB m n) n)) (ISZERO (SUB m n))
DIV := λm n.(λp.p (ISZERO (SUB n m) one zero)
                    (SUCC (p FALSE DIV (SUB m n) n))) (ISZERO (SUB m n))

pに(ISZERO (SUB m n))の結果が入って、pにFALSEとMOD (or DIV)を適用してこれを再帰用の関数にする、という。
FALSEは2引数の関数なら何でもいいんだけど。
こんな感じでいいのかな。

あとPREDをGrassで書くための指針

n f x.n (λg h.h (g f)) (λu.x) (λu.u)

を

λn f x.n ((λi g h.h (g i)) f) ((λj u.j) x) (λu.u)

こう書けば、中の3つの関数は全部外に出せる。

ググったら

Schemeでラムダ計算を解説してるページがあった。
→Church numerals and Lambda Calculus
なるほど、>=か…

いかん

DIVは書きかけだった。後で直す。