haskell如何实现Church编码划分？

Question

我是 haskell 的初学者，正在尝试实现自然数的 Church 编码，如 this guide 中所述。

我想实现两个教堂数字之间的除法。

{-# 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

如果我在div_rec之前省略suc，它适用于后者，但不适用于前者。

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

如何定义除法以适用于这两种情况？

Answer 1

你可以直接实现<（使用递归），然后用它来定义除法函数。这是一个例子：

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)

haskell如何实现Church编码划分？

How to implement Church encoding division in haskell?

haskell

lambda-calculus

church-encoding