问题标签 [church-encoding]

最近我在阅读有关 Lambda 演算和 Church Encoding 的文章，虽然我对它们的含义有了一个初步的了解，但我很难找到使用高阶函数来表示数值或列表而不是直接使用数值或列表的目的.

在编程中，对 Church-Encoded 表达式执行 Lambda 演算非常耗费机器资源，而且似乎是一种效率相当低的技术。我发现程序员通常认为这是不好的编程习惯，除了 Scheme 或 Haskell 程序员，出于奇怪的原因。

使用 Church 编码是否有任何实际的实际理由？还是只对理论研究有用？

好的，所以我正在尝试实现lambda calculus 的基础知识。就这样吧。

我的号码：

它们的部分（实际上，非）应用版本是这样的：

在继续之前，我定义了一些类型：

很好，succ功能是这样的（应用程序顺序应该完全一样！我在这里定义了）：

它的未应用版本变得如此可怕：

请原谅，这里是缺少的类型：

但我被困在这个add功能上。如果符合类型和定义（也采用此处），它就像

但我想a成为一个普通的数字类型FFZ[Z]。

那么 - 我如何定义加法？

我是 haskell 的初学者，并尝试实现自然数的 Church 编码，如本指南中所述。

我想实现两个教堂数字之间的划分。

ch_div在除以倍数时有效（例如9 / 3），但不适用于分数（例如9 / 2）。

如果我省略了sucbefore div_rec，它适用于后者，但不适用于前者。

如何定义适用于这两种情况的部门？

我很难理解为什么这些是各自教会数字的最通用类型：

我认为所有教堂数字都有相同的类型：

另外，我将如何找到 add 运算符的通用类型

任何帮助将不胜感激，谢谢！

人们常说

在“我们可以使用这些术语来执行测试布尔值的真实性的操作”的意义上表示 True 和 False。

但这隐藏了一个重要的警告，因为它似乎只在无类型的 lambda 演算中是正确的。如果我只是将这些值插入haskell，我可以编写一个函数：

它在类型级别区分 tru 和 fls。这么说是多么错误/真实：

• 在 STLC中tru，fls是一些提升'Boolean类型的价值级别见证，它有类型'True和'False
• 在 STLC 中（强制）类型值(tru :: ∀ t . t → t → t)并(fls :: ∀ t . t → t → t)表示 True 和 False（并且在未类型化中，通常情况下）

编辑：我现在意识到感谢@Daniel Wagner 的回答，我在我的问题中考虑的是二阶 Lambda 微积分而不是 STLC。

使用 Church 编码，可以在不使用内置 ADT 系统的情况下表示任意代数数据类型。例如，Nat可以表示（在 Idris 中的示例）为：

Pair可以表示为：

等等。现在，编写这些类型、构造函数、匹配器是一项非常机械的任务。我的问题是：是否可以将 ADT 表示为类型级别的规范，然后从这些规范中自动派生类型本身（即Nat/ Par）以及构造函数/析构函数？同样，我们可以使用这些规范来派生泛型吗？例子：

给定以下定义的结构和类型，需要编写乘以两个数字的函数。很难做到这一点。任何建议将不胜感激。

我是Haskell的新手。

我正在寻找是否有任何方法可以创建类类型的实例。

有没有办法让这段代码在不使用数据或新类型的情况下工作？

当我尝试在 GHCi 中加载模块时，它告诉我：

我正在尝试在 Swift 3 中实现教堂数字。目前，我有：

在我的函数 numToChurch 的这一行：

我不断收到一个编译时错误，即“关闭非转义参数'f'可能允许它转义”。作为快速修复，我接受了包含@escaping 的建议更改：

但即使在进行了更改之后，我仍然被告知同样的错误，它建议在“f:”之后添加另一个 @escaping。我知道这与将函数参数标记为 @escaping 以告诉编译器可以存储或捕获参数以进行函数式编程有关。但我不明白为什么我不断收到这个错误。

原始非转义问题已解决

帮助理解 Swift 中的教堂编码（续）：

关于 lambda 演算的维基百科条目定义了一些适用于教堂数字的公式，例如

在 Churches 论文中，他首先定义了他的 lambda 演算，他说

..两个变量的函数，当采用格式良好的公式 F 和 X 时，其值为公式{F}(X)，是递归的。

后来在他的论文中，他称这个函数为B(m,n)。

如何使用所有这些信息来描述类似的功能如何B在SUCC 1

我知道我们将不得不将输入和输出计算为素数的幂，因为他在整篇论文中都使用了哥德尔的编号系统，但是我发现很难将它们拼凑在一起。