鳥たちと戯れる
To Mock a Mockingbird を読んでいます。言わずと知れたコンビネータ論理の教科書(?)です。
そこで算術や論理を関数で表すという、ラムダ計算でよくある話が登場するのですが、自然数の定義が一般的なチャーチ数と違っていて分かりにくかったので、検算用のコードを書きました。
ふつうのチャーチ数では、zero f x = x = KIfx、one f x = f x = Ifx、two f x = f (f x) = SBIfx と定義しますが、zero = I、one = V(KI)I、two = V(KI)(V(KI)I) という定義になってます。
こんな感じ(↓)で遊べます。
Main> toInt $ exp five (multi three two) 15625 Main> toBool $ greater (multi two five) (multi three three) True Main> toInt $ concat (multi three four) three 123
コンビネータの本なので、下にあげた plus とか greater みたいな再帰関数をコンビネータで(ポイントフリーで)書く方法なんかも載っていて、勉強するにはとてもいい本だと思います。お薦め。
ちょっと確認する程度ならこんなコードで十分だけど、unsafeCoerceも鬱陶しいし、やはりここはちゃんとした処理系の実装に挑戦しようかな。
import Prelude hiding (succ,pred,exp,even,not,and,or,length,concat) import Unsafe.Coerce u = unsafeCoerce -- 事前準備 各種コンビネータ i x = x k x y = x t x y = y x l x y = x (y (u y)) b x y z = x (y z) c x y z = x z y v x y z = z x y r x y z = y z x s x y z = x z (y (u z)) -- 論理 true = k false = k i not = v false true and = r false or = t true imply = r true equiv = c s not -- 算術 zero = i succ = v false one = succ zero two = succ one three = succ two four = succ three five = succ four ten = multi two five pred = t false isZero = t true -- 各種関数 plus m n = isZero m n $ plus (pred $ u m) (succ $ u n) multi m n = isZero m zero $ plus n (multi (pred $ u m) n) exp m n = isZero n one $ multi m (u exp m (pred $ u n)) even n = isZero n true $ not $ u even $ pred $ u n greater m n = isZero m false $ isZero n true $ greater (pred $ u m) (pred $ u n) length n = a1 zero n where a1 l n = a l n (u l) $ u a1 (succ l) n a l n = greater (exp ten l) n concat m n = plus (multi m (exp ten (length $ u n))) n -- 表示・デバッグ用関数 toBool b = b True False :: Bool toInt n = isZero n 0 $ (+) 1 $ toInt $ pred $ u n :: Int
- 作者: Professor of Philosophy Raymond M Smullyan
- 出版社/メーカー: Oxford University Press
- 発売日: 2000/11/30
- メディア: ペーパーバック
- 購入: 3人 クリック: 23回
- この商品を含むブログ (8件) を見る