Haskellでチャーチ数 - capriccioso String Creating(Object something){ return My.Expression(something); }

色々と記事にしたいネタはあるのですが、どれもちゃっちゃと書ける感じでは無いので、今日はちょっと小ネタ更新します。

前々から、「チャーチ数とかHaskellなら簡単に表現できんじゃね？」とか思ってたのですが、どうやってshowするか思いつかないし考えるのも面倒だから放置していたのですが、つい最近、ふとした拍子にめちゃくちゃ簡単だという事に気づきまして・・・

せっかくなのでちょいと遊んでみましょう。

で、とりあえずまず、いつもの感じでghciを起動して、こんな関数を定義します。*1

Prelude> let showChurch f = f succ 0

で、そのままラムダ式でチャーチ数を書いて、この関数に適用してやります。

Prelude> showChurch ((\f x -> x) :: (t -> t) -> t -> t) --0の場合のみ、明示的に型を指定する必要がある
0
Prelude> showChurch (\f x -> f x)
1
Prelude> showChurch (\f x -> f (f x))
2
Prelude> showChurch (\f x -> f (f (f x)))
3
Prelude> showChurch (\f x -> f (f (f (f x))))
4

これが、まぁ、思いつきの割にはすんなりと動いてくれたので、調子に乗ってWikipediaにある定義を色々と実装して遊びます。

まずはsucc

Prelude> let succChurch n f x = f (n f x)
Prelude> showChurch $ succChurch (\f x -> f x)
2
Prelude> showChurch $ succChurch (\f x -> f (f x))
3
Prelude> showChurch $ succChurch (\f x -> f (f (f x)))
4

足し算とか・・・

Prelude> showChurch $ plusChurch (\f x -> f (f (f x))) (\f x -> f (f x))
5
Prelude> showChurch $ plusChurch (\f x -> f (f (f (f x)))) (\f x -> f (f (f x)))
7

かけ算も元気に動く

Prelude> let multChurch m n f = m (n f)
Prelude> showChurch $ multChurch (\f x -> f (f (f (f x)))) (\f x -> f (f (f x)))
12

で、論理記号なんかも実装します。
trueとfalseは何もラムダ式で書くまでもなく・・・

Prelude> let true = const
Prelude> let false = const id

andとかorはWikipediaのそのまんま書く。

Prelude> let andc p q = p q false
Prelude> let orc p q = p true q

で、同大百科によると、if-then-elseの定義は次のようになっていますが・・・

IFTHENELSE := λp x y. p x y

でもこれいらなくね？いらないよね？？
ってな感じで無視してそのまんまいじります。

Prelude> showChurch $ (andc true true) (\f x -> f x) (\f x -> f (f x))
1
Prelude> showChurch $ (andc true false) (\f x -> f x) (\f x -> f (f x))
2
Prelude> showChurch $ (andc false false) (\f x -> f x) (\f x -> f (f x))
2
Prelude> showChurch $ (orc false false) (\f x -> f x) (\f x -> f (f x))
2
Prelude> showChurch $ (orc false true) (\f x -> f x) (\f x -> f (f x))
1

あと、述語 iszero はこんな感じ・・・

let iszero n = n (\x -> false) true
Prelude> showChurch $ (iszero ((\f x -> x) :: (t -> t) -> t -> t)) (\f x -> f x) (\f x -> f (f x))
1
Prelude> showChurch $ (iszero (\f x -> f x)) (\f x -> f x) (\f x -> f (f x))
2
Prelude> showChurch $ (iszero (\f x -> f (f x))) (\f x -> f x) (\f x -> f (f x))
2

とまぁ、このへんの概念は自分の手で簡約してナンボってのはあるのですけど、実際にPC上でちゃんと動いてる所見るのもなかなか楽しいもんですね。

*1:数値を返してて全然showしてないじゃん！！とかいうツッコミは無しで。今は表示できれば良いんです！！