在 Haskell 中实现 Smullyan 的算术鸟

Posted 2023-02-22

【中文标题】在 Haskell 中实现 Smullyan 的算术鸟

【英文标题】：Implementing Smullyan's arithmetical birds in Haskell

【发布时间】：2014-02-04 19:37:55

【问题描述】：

在搜索 Raymond Smullyan 的 To Mock a Mockingbird 的信息时，我偶然发现了 Stephen Tetley's Haskell code for the basic combinators。我认为这是一个有趣的想法，并决定使用这些组合器来实现 To Mock a Mockingbird 的第 24 章中的“可以做算术的鸟”。我已经定义了真、假、继任者、前任和零校验组合器，以及将组合布尔值更改为 Haskell 布尔值的函数，反之亦然。但是当我尝试创建一个接受组合数字并返回整数的函数时，我一直遇到问题。我想知道如何使这个功能工作。这是我到目前为止所得到的：

-- | The first 7 combinators below are from Stephen Tetley's Data.Aviary.Birds
-- | (http://hackage.haskell.org/package/data-aviary-0.2.3/docs/Data-Aviary-Birds.html),
-- | with minor modifications.


-- | S combinator - starling. 
-- Haskell: Applicative\'s @(\<*\>)@ on functions.
-- Not interdefined.
st :: (a -> b -> c) -> (a -> b) -> a -> c
st f g x = f x (g x)

-- | K combinator - kestrel - Haskell 'const'.
-- Corresponds to the encoding of @true@ in the lambda calculus.
-- Not interdefined.
ke :: a -> b -> a
ke a _b = a 

-- | I combinator - identity bird / idiot bird - Haskell 'id'.
id' :: a -> a 
id' = st ke ke 

-- | B combinator - bluebird - Haskell ('.').
bl :: (b -> c) -> (a -> b) -> a -> c
bl = st (ke st) ke

-- | C combinator - cardinal - Haskell 'flip'.
ca :: (a -> b -> c) -> b -> a -> c
ca = st(st(ke st)(st(ke ke)st))(ke ke)

-- | T combinator - thrush.
-- Haskell @(\#)@ in Peter Thiemann\'s Wash, reverse application.
th :: a -> (a -> b) -> b
th = ca id'

-- | V combinator - vireo.
vr :: a -> b -> (a -> b -> d) -> d
vr = bl ca th




-- | The code I added begins here. 




-- | Truth combinator. Functionally superfluous since it can  
-- | be replaced with the kestrel. Added for legibility only.
tr :: a -> b -> a
tr = ke

-- | Falsity combinator.
fs :: a -> b -> b
fs = ke id'

-- | Successor combinator.
sc :: a -> ((b -> c -> c) -> a -> d) -> d
sc = vr fs 

-- | Predecessor combinator.
pd :: ((((a -> a) -> b) -> b) -> c) -> c
pd = th (th id')

-- | Zerocheck combinator.
zc :: ((a -> b -> a) -> c) -> c
zc = th ke



-- | Below are 2 functions for changing combinatory booleans 
-- | to Haskell booleans and vice versa. They work fine as 
-- | far as I can tell, but I'm not very confident about 
-- | their type declarations. I just took the types 
-- | automatically inferred by Haskell.

-- | Combinatory boolean to Haskell boolean.
cbhb :: (Bool -> Bool -> Bool) -> Bool
cbhb cb  = cb True False

-- | Haskell boolean to combinatory boolean.
hbcb :: Bool -> a -> a -> a
hbcb hb | hb     = tr
        | not hb = fs




-- | Combinatory number to Haskell number. 
-- | This is the problematic function that I'd like to implement. 
-- | I think the function is logically correct, but I have no clue
-- | what its type would be. When I try to load it in Hugs it 
-- | gives me a "unification would give infinite type" error. 
cnhn cn | cbhb (zc cn) = 0
        | otherwise    = 1 + cnhn (pd cn)

这是我对代码问题的粗略猜测：“cnhn”函数将任何组合数字作为参数。但是不同的组合数有不同的类型，比如

零) id' :: a -> a

one) vr(ke id')id' :: ((a -> b -> b) -> (c -> c) -> d) -> d

两个) vr(ke id')(vr(ke id')id') :: ((a -> b -> b) -> (((c -> d -> d) -> (e -> e) -> f) -> f) -> g) -> g

等等。因此，将任何组合数作为参数的函数必须能够采用无限多种类型的参数。但是 Haskell 不允许这样的函数。

简而言之，这是我的 3 个主要问题：

1) 'cnhn' 函数有什么问题？ （我上面的猜测正确吗？）

2) 可以修复吗？

3) 如果没有，我可以使用什么其他语言来实现 Smullyan 的算术鸟？

感谢您阅读这么长的问题。

【问题讨论】：

你需要更高等级的类型来为 Haskell 中 Church 编码的 naturals 提供合理的类型。

【参考方案1】：

似乎后继组合子不太正确。这是 Haskell 中 Church 算法的编码，unchurch 函数是 cnhn（我猜是 Church 编号到 Haskell 编号？）试图实现的功能。

tr :: a -> b -> a
tr x y = x

fl :: a -> b -> b
fl x y = y

succ :: ((a -> b) -> c -> a) -> (a -> b) -> c -> b
succ n f x = f (n f x)

unbool :: (Bool -> Bool -> t) -> t
unbool n = n True False

unchurch :: ((Int -> Int) -> Int -> a) -> a
unchurch n = n (\i -> i + 1) 0

church :: Int -> (a -> a) -> a ->a
church n =
  if n == 0
  then zero
  else \f x -> f (church (n-1) f x)

zero :: a -> b -> b
zero = fl

one :: (a -> a) -> a -> a
one = succ zero

two :: (a -> a) -> a -> a
two = succ one

ten :: (a -> a) -> a -> a
ten = succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))

main = do
  print (unchurch ten)
  print (unchurch (church 42))

所以一个以任意组合数作为参数的函数必须是 能够接受无限多种类型的论据。但哈斯克尔没有 允许这样的功能。

啊，但它确实如此，因为 Haskell 允许参数多态性。如果您查看数字的编码，它们都具有签名（(a -> a) -> a -> a），因此采用教堂编号的函数的参数只需要使其第一个参数将其第一个参数的类型变量与编码教堂编号的函数统一起来.

例如，我们还可以定义一个乘法运算，它实际上只是一个高阶函数，它需要两个教堂编号并将它们相乘。这适用于任何两个教会号码。

mult :: (a -> b) -> (c -> a) -> c -> b
mult m n f = m (n f)

test :: (a -> a) -> a -> a
test = mult ten ten

main = print (unchurch test) -- 100

【讨论】：

或者，church n = foldr (.) id . replicate n

我刚刚又查阅了这本书，发现这本书中使用的数字方案是由 Henk Barendregt 发明的，与 Church 的相似但不同。在该方案中，后继组合子定义为 V(KI)，其中 Vxyz = zxy，Kxy = x，并且 Ix = x。因此，尽管 unchurch 做了我试图用 cnhn 做 Church 算术的事情，但我想知道是否有一个函数可以做 Barendregt 算术。

我看到你对参数多态性的看法是对的。显然 Haskell 允许这样的事情，因为有许多函数需要多种类型的参数，例如id。所以cnhn 的问题一定是别的。

在 Barendregt 算术中没有这样的东西。您所描述的方案正是教堂算术，只是重新排列了组合器的参数。

我想我在这里用错了词。这不是不同的算术，它只是相同算术的不同数值方案。我想说的是，鉴于这个以 V(KI) 作为继任者的不同数值方案，似乎 cnhn 应该和 unchurch 做同样的事情，但它给出了一个错误。所以我想弄清楚它有什么问题。