Haskellでチャーチ数

あとで説明をつける予定

はじめに

これはうまく動く版だ。代数的データ型で明示的に再帰的な型を定義している。Cや.$.を消して読むと理解しやすいだろう。「うまく動かない版」を先に見ておくほうが理解しやすいだろう。

• うまく動かない版
• うまく動く版

型

church.hs

data C = C { (.$.) :: C -> C } | A C | Z

本質的にはコンストラクCのみで良い。
整数値との相互変換のためにコンストラクトAやZが必要になる。

整数値との相互変換

チャーチ数から整数へ

church.hs

toInt :: C -> Int
toInt Z = 0
toInt (A c) = 1 + toInt c
toInt n = toInt $ n .$. C A .$. Z

整数からチャーチ数ヘ

church.hs

toChurch :: Int -> C
toChurch 0 = zero
toChurch n = s .$. toChurch (n - 1)

ブール値と条件分岐

church.hs

false, true, _if :: C
false = C $ \x -> C $ \y -> y
true = C $ \x -> C $ \y -> x
_if = C $ \b -> C $ \x -> C $ \y -> b .$. x .$. y

数

church.hs

zero = C $ \f -> C $ \x -> x
s = C $ \n -> C $ \f -> C $ \x -> f .$. (n .$. f .$. x)
one = s .$. zero
two = s .$. one
three = s .$. two
four = s .$. three
five = s .$. four
six = s .$. five

数の演算

church.hs

add, mul, pre :: C
add = C $ \m -> C $ \n -> C $ \f -> C $ \x -> m .$. f .$. (n .$. f .$. x)
mul = C $ \m -> C $ \n -> C $ \f -> m .$. (n .$. f)
pre = C $ \n -> C $ \f -> C $ \x ->
        n .$. C (\g -> C $ \h -> h .$. (g .$. f)) .$. C (\u -> x) .$. C (\u -> u)

述語

church.hs

isZero :: C
isZero = C $ \n -> n .$. C (\x -> false) .$. true

例

church.hs

zeroToOne :: C
zeroToOne = C $ \n -> _if .$. (isZero .$. n) .$. one .$. n