问题标签 [church-encoding]

我指的是这个问题

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

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

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

我在 Haskell 中玩一些 lambda 演算的东西，特别是教堂数字。我定义了以下内容：

这有效：

发生检查失败：

我玩过我的常量iszero，mult它们似乎是正确的。有什么方法可以使这个可打字吗？我不认为我在做什么太疯狂了，但也许我做错了什么？

或者具体来说，为什么我们使用 foldr 来编码列表和迭代来编码数字？

很抱歉介绍冗长，但我真的不知道如何命名我想问的事情，所以我需要先做一些说明。这很大程度上来自这篇 CAMcCann 帖子，它不能完全满足我的好奇心，而且我还将讨论 rank-n-types 和无限懒惰事物的问题。

将数据类型编码为函数的一种方法是创建一个“模式匹配”函数，该函数为每种情况接收一个参数，每个参数都是一个函数，该函数接收与该构造函数相对应的值，并且所有参数都返回相同的结果类型。

对于非递归类型，这一切都按预期进行

然而，与模式匹配的很好的类比在递归类型中被打破了。我们可能会想做类似的事情

但是我们不能在 Haskell 中编写那些递归类型定义！通常的解决方案是强制将 cons/succ 案例的回调应用于所有级别的递归，而不仅仅是第一个级别（即，编写折叠/迭代器）。在这个版本中，我们使用r递归类型的返回类型：

虽然此版本有效，但它使定义某些功能变得更加困难。例如，如果您可以使用模式匹配，则为列表编写“tail”函数或为数字编写“predecessor”函数是微不足道的，但如果您需要使用折叠来代替，则变得很棘手。

所以我的真正问题是：

1. 我们如何确定使用折叠的编码与假设的“模式匹配编码”一样强大？有没有办法通过模式匹配来获取任意函数定义，然后机械地将其转换为仅使用折叠的函数？（如果是这样，这也将有助于在 foldr 方面使诸如 tail 或 foldl 之类的棘手定义变得不那么神奇）

2. 为什么 Haskell 类型系统不允许“模式匹配”编码中需要的递归类型？. 是否有理由只允许在通过定义的数据类型中使用递归类型data？模式匹配是直接使用递归代数数据类型的唯一方法吗？它与类型推断算法有关吗？

dlist包包含DList数据类型，它有很多实例，但没有Foldableor Traversable。在我看来，这是两个最“类似列表”的类型类。是否存在DList不是这些类的实例的性能原因？

此外，该包确实实现了foldrand unfoldr，但没有实现其他折叠功能。

有人可以使用替换向我解释我们如何得到一个数字“零”或其余的自然数吗？

例如值：“零”

如果我将此表达式应用于另一个表达式：

然后使用替换：

我错过了什么？我应该如何解释这些数字表达式？

我已经看到了教堂数字的以下数据构造函数

但这是一元数。我们如何以这种方式在 Haskell 中实现二进制数的数据构造函数？

我试过这个：

在此之后我们可以得到，十进制 5 编码为BinC [One,Zero,One]

但我想我在这里遗漏了一些东西。我的解决方案似乎不如教会的解决方案聪明。毫不奇怪，我不是教会。稍微思考一下，我发现我的解决方案依赖于列表，而 Nat 不依赖于任何像列表这样的外部结构。

我们是否也可以编写一个类似于 Church 的解决方案，对二进制数使用 Succ 类型构造函数？如果是，如何？我尝试了很多，但似乎我的大脑无法摆脱对列表或其他类似结构的需求。

我还没有看到在 lambda 演算中提到二进制数字。教会数字是一元系统。我在这里问了一个关于如何在 Haskell 中执行此操作的问题：How to implement Binary numbers in Haskell 但即使在我看到并理解了这个答案之后，我仍然无法理解如何在纯无类型的 lambda 演算中执行此操作。

所以这是我的问题：是否在无类型 lambda 演算中定义了二进制数字，并且是否也为它们定义了后继函数和前驱函数？

我正在尝试在 lambda 演算中定义二进制指数运算符，例如运算符 CARAT。例如，这个运算符可能有两个参数，数字 2 的 lambda 编码和数字 4 的 lambda 编码，并计算数字 16 的 lambda 编码。我不知道我的答案是对还是错，但我花了一天时间这样做。我使用了教堂数字定义。

这是我的答案。如果我的回答有误，请纠正我。我不知道如何以正确的方式做到这一点。如果有人知道，请帮我找出简短的答案。

加一的后继函数可以用和next定义自然数：zeronext

根据以上结论，我们可以定义next如下函数：

因此，我们可以有把握地证明……

加法只是继任者的迭代。我们现在可以根据以下条件定义加法next：

在将值替换为 'next' 和随后的 'two' 之后，我们可以进一步将上述形式简化为

即四个。

同样，乘法是加法的迭代。因此，乘法定义如下：

在将值替换为“three”、“next”和随后的“add”，然后再次替换“next”后，上述形式将简化为

即六个。

最后，幂可以通过迭代乘法来定义

假设取幂函数被称为 CARAT

现在，将上述表达式归约并代入“next”和“four”并进一步归约，我们得到以下形式

即十六。

我必须为 > 、 < 和 != 创建一些 Lambda 函数

我不知道怎么做，有人可以帮我吗？PS：我们刚开始学习 Lambda 演算，所以请不要假设任何先前的知识。

谢谢你的期待！

编辑- 我的意思是Lambda 演算中的算术

编辑 2 - 更准确：寻找 Church-encoding (lambda calculus) 来定义 < , > , !=

编者注：我认为这是 OP 试图问的：

我正在尝试使用 Church 编码在无类型 lambda 演算中实现以下操作：

1. 大于（GT或>）。
2. 小于（LT或<）。
3. 不等于 (NE或!=)。

我已经知道如何实现以下内容：

1. 布尔真（TRUE或λx.λy.x）。
2. 布尔假（FALSE或λx.λy.y）。
3. 逻辑和（AND或λp.λq.p q p）。
4. 逻辑或（OR或λp.λq.p p q）。
5. 逻辑非（NOT或λp.λa.λb.p b a）。

您将如何在无类型 lambda 演算中编写GT、LT和函数？NE

我从书中读到，Church Numerals 的后继形式为： (\lambda nf x. f (nfx) )

昨晚我想出了这个： (\lambda ab c. (ab) (bc) )

我相信它也执行后继功能的功能。但是，我不是 100% 肯定我的减少是正确的。有人可以检查它并告诉我吗？

以下是我的简化：设一个教堂数字为 (\lambda f x. f^nx)，其中 f^nx 实际上是 (f(f(f(f...(x)))..它代表数字n，期望的结果应该是n+1，即(\lambda f x. f^{n+1} x)

(\lambda ab c. (ab) (bc) )(\lambda f x. f^nx)

= (\lambda b c. ( (\lambda f x. f^nx) b) (bc) ) // a 替换

= (\lambda b c. ( (\lambda x. b^nx) (bc) ) // f 替换

= (\lambda b c. ( (\lambda x. b^nx) (bc) ) // 不是 100% 确定，我可以用 (bc) 替换 x 吗？

= (\lambda b c. ( b^n (bc) )

= (\lambda b c. ( b^(n+1) c )

这种减少是否正确，尤其是从第 3 步到第 4 步？谢谢！