问题标签 [church-encoding]

我一直在尝试研究如何在 Scala 中实现 Church 编码的数据类型。似乎它需要 rank-n 类型，因为您需要 type 的一流const函数forAll a. a -> (forAll b. b -> b)。

但是，我因此能够对对进行编码：

对于列表，我能够编码cons：

但是，空列表问题更大，我无法让 Scala 编译器统一类型。

你能定义 nil，这样，给定上面的定义，下面的编译吗？

我可以使用方案相当容易地定义教堂数字：

但是，这并不容易识别(f f)0 和 (f (ff)) 是 1。有没有办法让这些数字更具可读性？理想的情况是：

该示例在方案中，但我会在任何 lisp 中回答。

我被困在以下步骤中。如果有人可以帮助我，那就太好了：

我的步骤是：

括号好不好？我真的对替换和括号感到困惑。有没有一种正式的、更简单的技术来解决这些问题？

我正在练习 SML，我正在做一个小任务，我们必须实现教堂数字，定义为：

示例值

我已经实现了以下功能：

并SUC返回 Church 数字的后继。

现在我必须实现该功能

它返回 (predecessor, current numeric) 的元组。我不允许使用churchToInt，我应该直接使用 Church 数字。显然，这可以通过传递特定参数在一行中解决。

我一直在考虑SUC一遍又一遍地使用，直到我们找到正确的数字，但我无法比较 2 个 Church 数字。我完全坚持这一点。

我正在通过 SICP 工作，问题 2.6让我陷入了困境。在处理 Church 数字时，将零和 1 编码为满足某些公理的任意函数的概念似乎是有意义的。此外，使用零的定义和 add-1 函数推导出单个数字的直接公式是有意义的。我不明白如何形成加号运算符。

到目前为止，我有这个。

查看lambda calculus的维基百科条目，我发现 plus 的定义是 PLUS := λmnfx.mf (nfx)。使用该定义，我能够制定以下程序。

我不明白的是，如何仅使用先前派生过程提供的信息直接派生该过程。谁能以某种严格的类似证明的形式回答这个问题？直觉上，我想我明白发生了什么，但正如理查德·费曼曾经说过的，“如果我不能建造它，我就无法理解它……”

我正在尝试在 Haskell 中实现教堂数字，但我遇到了一个小问题。Haskell 抱怨无限类型

发生检查：无法构造无限类型：t = (t -> t1) -> (t1 -> t2) -> t2

当我尝试做减法时。我 99% 肯定我的 lambda 演算是有效的（如果不是，请告诉我）。我想知道的是，我是否可以做些什么来让 haskell 与我的函数一起工作。

教堂数字可以用 C++0x (C++11?) 使用语言的新 lambda 部分表达，如下所示：

是否可以使用 Boost.Bind 和 C++03 来表达 Church 数字？如果是这样，怎么做？

我一直在阅读的《计算机程序的结构和解释》一书通过定义零和增量函数来介绍 Church 数字

这对我来说似乎很复杂，我花了很长时间才弄清楚并推导出一个 ( λf.λx. f x) 和两个 ( λf.λx. f (f x))。

用这种方式编码数字不是更简单吗，零是空的 lambda？

现在很容易推导出一个 ( λ. λ) 和两个 ( λ. λ. λ)，依此类推。

这似乎是用 lambda 表示数字的一种更直接、更直观的方式。这种方法是否存在问题，因此有充分的理由说明教堂数字以它们的方式工作吗？这种方法是否已经得到证实？

我必须实现 haskell map 函数来处理教堂列表，这些列表定义如下：

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

本练习的示例解决方案是：

我不知道这个解决方案是如何工作的，也不知道如何创建这样的功能。我已经有 lambda 演算和教堂数字的经验，但是这个练习让我很头疼，我必须能够理解和解决这些问题，以便下周的考试。有人可以给我一个很好的资源，让我可以学习解决这些问题，或者给我一些关于它如何工作的指导吗？

Church 编码（又名访客模式）是一种将数据表示为函数的方式：而不是

你可以定义

. 尽管将任何东西表示为函数的能力很好，但我一直认为第一个版本更可取，因为它更简洁并且不需要语言扩展（显式forall）。但是，您有时可以在公共图书馆中找到教堂编码的数据。使用它有什么好处？

公共图书馆中教堂编码的例子：

• 迭代者
• 修订控制单子
• （请帮我扩展列表）