Church数 1

Church数の引き算について、同じ疑問を持った人がいた。
http://www5d.biglobe.ne.jp/~y0ka/2006-07-31-6.html

それによるとWikipedediaに載ってるらしい。

Church数の1引く関数

 pred ≡ λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)  -- (1)

うむ。記号の意味から分からん。
Wikipedeiaの下のほうの参考文献の計算論の本をげと。
それによると、

ラムダ記法の省略記法

λx1x2x3…xn.M = lambda (x1) (lambda (x2) (lambda (x3) (...lambda (xn) (M)))...)

ラムダ式の適用に関して

M1M2M3…Mn = (…(((M1 M2) M3) M4) ･･･ Mn)

M1を M2を引数として実行（適用）、
した結果にM3を引数として･･･以下略
とあるので、
(1)の式をschemeに翻訳すると

(define pred
  (lambda (n)
	(lambda (f)
	  (lambda (x)
		(((n 
		   (lambda (g)
			 (lambda (h)
			   (h (g f))))) (lambda (u) x)) (lambda (u) u))))))

一日中ぼけっと眺めてましたが、さっぱり分からん。
何が何やら。

n に two = lambda (f) (lambda (x) (f (f x)))
を与えてどうなるか見てみる。

;; nを twoで置換え
(define sub1-two1
  (lambda (f)
    (lambda (x)
      (((two
	 (lambda (g)
	   (lambda (h)
	     (h (g f))))) (lambda (u) x)) (lambda (v) v))))

;; two を (lambda (f) (lambda (x) (f (f x))) で置換え
;; (f (f x)) の f がlambda (g)以下に相当するので置換え
;; xが被って見難いので x2に変更
(define sub1-two2
  (lambda (f)
    (lambda (x)
      ((
	( lambda (x2) ( (lambda (g)
			  (lambda (h)
			    (h (g f))))
			((lambda (g)
			   (lambda (h)
			     (h (g f)))) 
			 x2)))
	(lambda (u) x))
       (lambda (v) v))
      ))
  )
;;さらに置換え
;; x2 に (lambda (u) x)を適用
(define sub1-two3	
(lambda (f)
  (lambda (x)
    ((
      (lambda (g)
	(lambda (h)
	  (h (g f))))
      
      ((lambda (g)
	 (lambda (h)
	   (h (g f)))) 
       (lambda (u) x))      
     
      )
     (lambda (v) v))
    ))
)

;; さらに置換え
(define sub1-two4	

  (lambda (f)
    (lambda (x)
      ((
	(lambda (g)
	  (lambda (h)
	    (h (g f))))      
	(lambda (h)
	  (h x)
	  )
	)
       (lambda (v) v))
      ))
  )

(define sub1-two4-1
  (lambda (f)
    (lambda (x)
      ((lambda (h)
	  (h ((lambda (h) (h x)) f))
	  )
	(lambda (v) v)))))

(define sub1-two4-2
  (lambda (f)
    (lambda (x)
      ((lambda (h)
	  (h (f x))
	  )
       (lambda (v) v)))))

(define sub1-two5
  (lambda (f)
    (lambda (x)
      (f x))))

predに twoを適用したら oneが出てきました。
何の魔法ですか？ これ。
一生かかっても思いつける気がしません。
書いてあることが理解できる気もしません。
自分で式を展開した結果すら未だに飲み込めてません。

まあそれでも、私のような阿呆すら、関数を適用する手動置換の結果が正しいかどうかをいちいち実行して確かめられるのがschemeのいいところですね。

(sub1-two1 plus1) 0) ;; -> 1
(sub1-two2 plus1) 0) ;; -> 1
てな感じで。

あと、どうでもいいこと。
訳の分からんlambda式でも、emacsのインデントは偉いので、どのlambda式がどの引数で適用されているかが分かるんですね。しばらくインデントに頼らせてもらうことにしよう。

    ((lambda (x)以下とても難しい式1

        ･･･

     (lambda (y)以下とても難しい式2

       ･･･

こんな風なインデントになっていれば、ラムダ式1に式2を引数として適用してることが分かるわけだ。偉いな。meadowさんは。