ラムダ計算遊び用コード まとめ

昨日見つけたページに倣ってλ項の名前には全部頭に%をつけて、ついでに左から適用してく関数を%としてみた。
とりあえずxyzzyとSBCLで動いてるけど、真偽値の辺りちゃんとテストしてない。

; utility
(defun % (&rest arg)
  (reduce #'funcall arg))

(defun $ (&rest arg)
  (reduce #'funcall arg :from-end t))

; SUCC := λn f x.f (n f x)
(defvar %succ
  (lambda (n)
    (lambda (f)
      (lambda (x)
        (% f (% n f x))))))

; ZERO := λf x.x
(defvar %0
  (lambda (f)
    (lambda (x)
      x)))

(defvar %1
  (% %succ %0))

(defvar %2
  (% %succ %1))

(defvar %3
  (% %succ %2))

(defun cn (n)
  (do ((i 0 (1+ i))
       (f %0 (% %succ f)))
      ((= i n) f)))

; ADD := λn m f x.n f (m f x)
(defvar %add
  (lambda (m)
    (lambda (n)
      (lambda (f)
        (lambda (x)
          (% m f (% n f x)))))))

; MULT := λm n f.m (n f)
(defvar %mul
  (lambda (m)
    (lambda (n)
      (lambda (f)
        ($ m n f)))))

; POW := λm n.n m
(defvar %pow
  (lambda (m)
    (lambda (n)
      (% n m))))

; TET := λm n.n (POW m) one
;      = λm n.n (λk.k m) one
(defvar %tet
  (lambda (m)
    (lambda (n)
      (% n ($ %pow m) %1))))

; PRED := λ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)
(defvar %pred
  (lambda (n)
    (lambda (f)
      (lambda (x)
        (% 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)
      (% n %pred m))))

; MOD := λm n.ISZERO (SUB m n) (ISZERO (SUB n m) ZERO m) (MOD (SUB m n) n)
;      = λm n.(λp.p (ISZERO (SUB n m) ONE ZERO)
;                     (p FALSE DIV (MOD m n) n)) (ISZERO (SUB m n))
(defvar %mod
  (lambda (m)
    (lambda (n)
      (funcall
       (% (% %iszero (% %sub m n))
          (lambda () (% %iszero (% %sub n m) %0 m))
          (lambda () (% %mod (% %sub m n) n)))))))

; DIV := λm n.ISZERO (SUB m n) (ISZERO (SUB n m) ONE ZERO) (SUCC (DIV (SUB m n) n))
;      = λm n.(λp.p (ISZERO (SUB n m) ONE ZERO)
;                     (SUCC (p FALSE DIV (SUB m n) n))) (ISZERO (SUB m n))
(defvar %div
  (lambda (m)
    (lambda (n)
      (funcall
       (% (% %iszero (% %sub m n))
          (lambda () (% %iszero (% %sub n m) %1 %0))
          (lambda () (% %succ (% %div (% %sub m n) n))))))))


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

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

; AND := λp q. p q FALSE
(defvar %and
  (lambda (p)
    (lambda (q)
      (% p q %f))))

; OR := λp q. p TRUE q
(defvar %or
  (lambda (p)
    (lambda (q)
      (% p %t q))))

; NOT := λp. p FALSE TRUE
(defvar %not
  (lambda (p)
    (% p %f %t)))

; XOR := λp q. p (NOT q) q
(defvar %xor
  (lambda (p)
    (lambda (q)
      (% p (% q %f %t) q))))

; IFTHENELSE := λp x y. p x y
(defvar %if
  (lambda (p)
    (lambda (x)
      (lambda (y)
        (% p x y)))))

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


; GE := λm n.ISZERO (SUB m n)
(defvar %ge
  (lambda (m)
    (lambda (n)
      ($ %iszero (% %sub m n)))))

; LE := λm n.GE n m
(defvar %le
  (lambda (m)
    (lambda (n)
      (% %ge n m))))

; EQUAL
(defvar %eq
  (lambda (m)
    (lambda (n)
      (% %and (% %ge m n) (% %ge n m)))))


; CONS := λf r b.b f r
(defvar %cons
  (lambda (f)
    (lambda (r)
      (lambda (b)
        (% b f r)))))

; CAR := λp.p true
(defvar %car
  (lambda (p)
    ($ p %t)))

; CDR := λp.p false
(defvar %cdr
  (lambda (p)
    ($ p %f)))

; Y-combinator
(defvar %y
  (lambda (g)
    ($ (lambda (x)
         ($ g (lambda (&rest arg) (apply ($ x x) arg))))
       (lambda (proc)
         ($ g (lambda (&rest arg) (apply ($ x x) arg)))))))

参考

• ラムダ計算
• Church numerals and Lambda Calculus
• Y-combinator

Yコンビネータの解説は色々あったけど、これが一番分かりやすかった。