Church Encoding in Haskell

　HaskellでChurch Encodingをしてみました。Church Encodingとは、すべての演算をラムダ算法でエンコードすることです。

　まずは、”数値”をラムダ式で表してみます。

これは、やってみて意味が分かりましたが、すごいことです。nという数値をf^(n) xで表すことにします。

1 -> f x

2 -> f (f x)

3 -> f (f (f x))

・・・・

n -> f^(n) x

という感じです。

fとxは何を選んでもいいですが、私たちが慣れ親しんだ数値と簡単に変換できるように

f = succ

x = 0

とします。そして、以下の2つの関数を定義します。

view plainprint?

1. -- integer -> church  
2. church n = \f -> \x -> iterate f x !! n  
3.   
4. -- church -> integer  
5. unChurch n = n succ 0  

-- integer -> church
church n = \f -> \x -> iterate f x !! n

-- church -> integer
unChurch n = n succ 0

churchは正数をチャーチ数に変換します。unChurchはチャーチ数を対応する正数に変換します。

　これだけだと、ふーんという感じですが、このチャーチ数に対して演算を定義してあげます。例えば、チャーチ数の足し算add m nは、

　　f ^(m) x + f ^(n) x = f ^(n+m) x

となるように定義すればよいので、

view plainprint?

1. add = \m -> \n -> \f -> \x -> m f (n f x)  

add = \m -> \n -> \f -> \x -> m f (n f x)

とします。

同様に、掛け算、べき乗、インクリメントを定義します。

view plainprint?

1. -- one  
2. one = \f -> \x -> f x  
3.   
4. -- n++  
5. inc = \n -> \f -> \x -> f (n f x)  
6.   
7. -- m*n  
8. mult = \m -> \n -> \f -> \x -> m (n f) x  
9.   
10. -- m^n  
11. expt = \m -> \n -> n (mult m) one  

-- one
one = \f -> \x -> f x

-- n++
inc = \n -> \f -> \x -> f (n f x)

-- m*n
mult = \m -> \n -> \f -> \x -> m (n f) x

-- m^n
expt = \m -> \n -> n (mult m) one

　ラムダ算法の世界でも、私たちが慣れ親しんだ計算の世界と同じようにきちんと計算ができていることを確認します。

view plainprint?

1. main = do let a = church 2  
2.             b = church 10  
3.         print $ unChurch $ add a b  
4.         print $ unChurch $ inc a  
5.         print $ unChurch $ mult a b  
6.         print $ unChurch $ expt a b  

main = do let a = church 2
            b = church 10
        print $ unChurch $ add a b
        print $ unChurch $ inc a
        print $ unChurch $ mult a b
        print $ unChurch $ expt a b

　このようにラムダ算法には、”値”という概念がないにもかかわらず、チャーチ数を利用することで、基本的な計算をシュミレートすることができます。

実際、ラムダ算法はチューリング完全なので、チューリングマシン上で実行できるすべての計算処理を記述することができます。さらにいうと、すべての演算は、たった３つの演算子で記述可能です。それについてはまた今度書きます。