ラムダ計算でハマる

2008-02-02
#math

チャーチ数は、関数 f を x に何回適用したか、で数を表すらしい。 まずは０から、

  • zero = λf.λx. x

１進めた数は succ で得られる

  • succ = λn.λf.λx. f (n f x)

２つの数 m、n の足し算は、初期値 m にさらに n 回 f を適用すれば得られる

  • plus = λm.λn.λf.λx. n f (m f x)

掛け算は、m の加算を n 回行う、ってことかな？

  • mult = λm.λn.λf.λx. n (m f) x

ここまではなんとなくわかったんだけど、指数がどうして次のようになるのかわからない：

  • exp = λm.λn. n m

手で展開してみる： exp 3 2

2 = λf.λx. f (f x)
3 = λf.λx. f (f (f x))
exp 3 2 = (λm.λn.λf.λx. n m f x) 3 2
        = (λf.λx. (λg.λy. g (g y)) m f x)    -- n = 2 = λg.λy. g (g y) に置き換え
        = (λf.λx. (λy. m (m y)) f x)    -- g を m に置き換え
        = (λf.λx. (m (m f)) x)    -- y を f に置き換え
                                    -- この時点で、(mult m m) の形になってる
        = (λf.λx. ((λh.λz. h (h (h z))) ((λh.λz. h (h (h z))) f)) x)    -- m = 3 = λh.λz. h (h (h z))
        = (λf.λx. ((λh.λz. h (h (h z))) (λz. f (f (f z)))) x)    -- h を f に置き換え
        = (λf.λx. ((λz. (λw. f (f (f w))) ((λw. f (f (f w))) ((λw. f (f (f w))) z)))) x)    -- h を (λw. f (f (f w))) に置き換え
        = (λf.λx. ((λz. (λw. f (f (f w))) ((λw. f (f (f w))) (f (f (f z)))))) x)    -- w を z に置き換え
        = (λf.λx. ((λz. (λw. f (f (f w))) (f (f (f (f (f (f z)))))))) x)    -- w を (f (f (f z))) に置き換え
        = (λf.λx. ((λz. (f (f (f (f (f (f (f (f (f z))))))))))) x)    -- w を (f (f (f (f (f (f z)))))) に置き換え
        = (λf.λx. f (f (f (f (f (f (f (f (f x)))))))))    -- z を x に置き換え
        = 9

ちゃんと計算はできてる、けどなぜかはわからない…。 n に m を適用するってなんだ？

succ の逆に、-1 する pred もよくわからない：

  • pred = λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)

引き算は、記述はもっともだけど

  • minus = λm.λn. n pred m

なんで計算できるのかはわからない 。なぜかというと、Haskell でテストしようとしてもエラーが出てしまったから：

zero = \f x -> x
succ = \n f x -> f (n f x)
plus = \m n -> \f x -> n f (m f x)
mult = \m n -> \f x -> n (m f) x
exp  = \m n -> n m

pred = \n f x -> n (\g h -> h (g f)) (\u -> x) (\u -> u)
minus = \m n -> n pred m

コンパイルは通る：GHCi で

-- チェック用：チャーチ数を整数に変換
import Prelude( (+) )

p f = f (+1) 0

one   = succ zero
two   = succ one
three = succ two

p zero  ;=> 0
p one   ;=> 1
p (plus one two)   ;=> 3
p (mult three two)   ;=> 6
p (exp three two)   ;=> 9
p (pred three)  ;=> 2

引き算で、２以上を引こうとすると無限エラーが出る：

> p (minus three zero)
3
> p (minus three one)
2
> p (minus three two)

<interactive>:1:15:
    Occurs check: cannot construct the infinite type:
      t1 = (t1 -> t2) -> (t2 -> t3) -> t3
    Probable cause: `two' is applied to too few arguments
    In the second argument of `minus', namely `two'
    In the first argument of `p', namely `(minus three two)'

謎。

いろいろ資料：

関連記事

新着記事