Life Goes On

まあまあだけど楽しんでる方です

鳥たちと戯れる

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

To Mock a Mockingbird

To Mock a Mockingbird