4

私は Haskell の初心者で、このガイドで説明されているように、自然数の Church エンコーディングを実装しようとしています。

2 つの教会の数字の間の分割を実装したいと思います。

{-# LANGUAGE RankNTypes #-}

import Unsafe.Coerce

y :: (a -> a) -> a
y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x))

true = (\x y -> x)
false = (\x y -> y)

newtype Chur = Chr (forall a. (a -> a) -> (a -> a))

zer :: Chur
zer = Chr (\x y -> y)

suc :: Chur -> Chur
suc (Chr cn) = Chr (\h -> cn h . h)

ci :: Chur -> Integer
ci (Chr cn) = cn (+ 1) 0

ic :: Integer -> Chur
ic 0 = zer
ic n = suc $ ic (n - 1)


-- church pair
type Chp = (Chur -> Chur -> Chur) -> Chur

pair :: Chur -> Chur -> Chp
pair (Chr x) (Chr y)  f = f (Chr x) (Chr y)

ch_fst :: Chp -> Chur
ch_fst p = p true

ch_snd :: Chp -> Chur
ch_snd p = p false

next_pair :: Chp -> Chp
next_pair = (\p x -> x (suc (p true)) (p true))

n_pair :: Chur -> Chp -> Chp
n_pair (Chr n) p = n next_pair p

p0 = pair zer zer
pre :: Chur -> Chur
pre (Chr cn) = ch_snd $ n_pair (Chr cn) p0

iszero :: Chur -> (a->a->a)
iszero (Chr cn) = cn (\h -> false) true

unchr :: Chur -> ((a -> a) -> (a -> a))
unchr (Chr cn) = cn

ch_sub :: Chur -> Chur -> Chur
ch_sub (Chr cn1) (Chr cn2) = cn2 pre (Chr cn1)

-- only works if b is a multiple of a
ch_div :: Chur -> Chur -> Chur
ch_div a b = suc $ y div_rec a b n0
div_rec :: (Chur -> Chur -> Chur -> Chur)-> Chur -> Chur -> Chur -> Chur
div_rec = (\r a b n -> iszero (ch_sub a b) n $ r (ch_sub a b) b (suc n))

n0 = zer
n1 = ic 1
n2 = ic 2
n3 = ic 3
n4 = ic 4

ch_div倍数の割り算 ( など9 / 3) では機能しますが、分数 ( など9 / 2) では機能しません。

*Main> ci $ ch_div (ic 9) n3
3
*Main> ci $ ch_div (ic 9) n2
5

sucbeforeを省略するdiv_recと、後者では機能しますが、前者では機能しません。

*Main> ci $ ch_div (ic 9) n3
2
*Main> ci $ ch_div (ic 9) n2
4

両方のケースで機能する除算を定義するにはどうすればよいですか?

4

1 に答える 1

4

(再帰を使用して) 直接実装<し、それを使用して除算関数を定義できます。次に例を示します。

type ChBool a = a -> a -> a

-- 'less than' function
lt :: Chur -> Chur -> ChBool x
lt = y (\r a b -> iszero a (iszero b 
                                   false           -- a = 0 & b = 0
                                   true)           -- a = 0 & b > 0
                           (r (pre a) (pre b)))    -- lt (a - 1) (b - 1)

ch_div :: Chur -> Chur -> Chur
ch_div = y (\r a b -> lt a b
                         zer
                         (suc (r (ch_sub a b) b)))

テスト:

λ> ci $ ch_div (ic 9) (ic 1)
9
λ> ci $ ch_div (ic 9) (ic 2)
4
λ> ci $ ch_div (ic 9) (ic 3)
3
λ> ci $ ch_div (ic 9) (ic 4)
2
λ> ci $ ch_div (ic 9) (ic 5)
1
λ> ci $ ch_div (ic 9) (ic 9)
1
λ> ci $ ch_div (ic 9) (ic 10)
0

そして（コメントですでに述べたように）代わりにy、安全な固定小数点コンビネータを使用することをお勧めします。

を実装するために再帰は必要ないことを付け加えなければなりませんlt。次のように実行できます。

-- boolean negation
ch_not a = a false true

-- greater or equal
ge a b = iszero $ ch_sub b a

-- less than
lt a b = ch_not (ge a b)
于 2016-04-25T12:58:22.333 に答える