4

我指的是这个问题

type Churchlist t u = (t->u->u)->u->u

在 lambda 演算中，列表编码如下：

[] := λc. λn. n
[1,2,3] := λc. λn. c 1 (c 2 (c 3 n))

mapChurch :: (t->s) -> (Churchlist t u) -> (Churchlist s u)
mapChurch f l = \c n -> l (c.f) n

我正在考虑我可以在 Churchlists 上实现哪些其他列表功能，并成功编写了一个 conc2 函数来连接 2 个教堂列表

conc2Church l1 l2 c n = l1 c (l2 c n)

我还尝试了一个 zipWithChurch，它在普通列表上的运行方式与 zipWith 类似。但我找不到解决方案。谁能帮我？

4

1 回答 1

4

你想使用真正的元组还是教堂元组？我假设前者。

因此，从所需的类型签名开始。你希望它接受 2 个不同Churchlist的 s 并产生一个Churchlist元组。

churchZip :: Churchlist a u -> Churchlist b u -> Churchlist (a,b) u

现在你将如何实现这个？回想一下，Churchlists 由折叠它们的函数表示。因此，如果我们的结果是 a Churchlist (a,b) u，我们会希望它具有类型函数的形式((a,b) -> u -> u) -> u -> u（毕竟，这相当于类型 synonym Churchlist (a,b) u）。

churchZip l1 l2 c n = ???

你下一步怎么做？嗯，这取决于。是l1空的吗？怎么样l2？如果其中任何一个是，那么您希望结果是空列表。否则，您希望将每个列表中的第一个元素配对，然后将其余部分进行 ChurchZip 配对。

churchZip l1 l2 c n
  | isEmpty l1 || isEmpty l2 = n
  | otherwise                = c (churchHead l1, churchHead l2)
                                 (churchZip (churchTail l1) (churchTail l2) c n

这带来了一些问题。

  • 你可以递归地写这个函数吗？在纯 lambda 演算中，您必须使用定点运算符（又名 y 组合器）编写递归函数。
  • 你有churchHead, churchTail, 和isEmpty可用吗？你愿意写吗？你能写出来吗？
  • 有没有更好的方法来构造这个函数？任何事情都可以通过折叠来完成（请记住，l1实际上l2折叠功能在自身之上），但这是对这个问题的一个干净的解决方案吗？

假设对列表的教会编码有深刻的理解，达到这一点纯粹是机械的。我会把深入的思考留给你，因为这是家庭作业。

于 2012-03-23T22:26:30.143 回答