【问题标题】:Operations on Church Lists in HaskellHaskell 中的教会列表操作
【发布时间】:2012-03-23 20:54:07
【问题描述】:

我指的是this question

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 类似。但我找不到解决方案。谁能帮帮我?

【问题讨论】:

  • 您是否尝试过将问题从教会列表限制到教会数字? zip的数字模拟是min;写下来可能会给你一些见解。
  • 感谢您的建议,如果我发现有启发性的内容,我会尝试并报告
  • 我认为这更容易,就像我上面的 conc2church 示例一样。我认为在这种情况下,这对我来说是最重要的。还是谢谢你

标签: haskell lambda-calculus church-encoding


【解决方案1】:

您想使用真正的元组还是教堂元组?我会假设前者。

所以,从所需的类型签名开始。您希望它接收 2 个不同的 Churchlists 并生成一个 Churchlist 元组。

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

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

churchZip l1 l2 c n = ???

下一步是什么?嗯,这取决于。 l1 是空的吗? l2 呢?如果其中任何一个是,那么您希望结果是空列表。否则,您希望将每个列表中的第一个元素配对,然后将其余部分进行教堂压缩。

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 组合器)编写递归函数。
  • 您有churchHeadchurchTailisEmpty 可用吗?你愿意写吗?你能写出来吗?
  • 有没有更好的方法来构造这个函数?任何事情都可以通过折叠来完成(请记住,l1l2 实际上对其自身的折叠功能),但这是解决这个问题的一个干净的解决方案吗?

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

【讨论】:

  • 该死的,好答案。花了一段时间trying to work this out,现在我想回去使用 ChurchPair 和 ChurchMaybe。
  • 你也在使用非教会Bools。我想知道这是否允许。