问题标签 [church-encoding]

假设我有一个名为 f 的函数，它接受一个名为 x 的整数参数并返回一个整数。我还有一个整数 n 表示函数必须调用自身的次数。因此，例如，如果我的函数调用f(x)在 n = 1 时看起来像这样，那么f(f(f(x)))当 n = 3 时它看起来像这样。在下面的示例中怎么会这样：

我最近一直在使用 Python 中的递归表达式。此类表达式的示例如下所示：

我正在尝试将这样的表达式转换为我可以直接计算的东西，例如，

直观地说，似乎需要某种形式的递归，但是，由于某种原因，我无法解决这个问题。

谢谢！

我想将十进制编码号更改为 chruch 编码号？

我的代码有什么问题？谢谢你。

自然数的著名 Church 编码可以推广到使用任意函子F。结果是类型，称为它C，定义为

在这里和下面，为简单起见，我们将假设它F是一个固定的、已经定义的函子。

众所周知，类型C是函子的固定点F，也是C初始F代数。例如，如果函子F a定义为

然后是F ais的固定点[a]（类型的值列表a）。另外，[a]是初始代数。列表的 Church 编码是众所周知的。但是我找不到这些陈述中的任何一个的严格证明（C是一个固定点，并且C是初始代数）。

问题是，如何严格证明两个陈述之一：

1. 该类型C是类型 isomorphism 的固定点F C ≅ C。换句话说，我们需要证明存在两个函数，fix :: F C -> C并且unfix :: C -> F C使得fix . unfix = id和unfix . fix = id。
2. 类型C是函子的初始代数F；即-F代数范畴中的初始对象。换句话说，对于任何给定A函数p :: F A -> A的类型（即是-A代数F），我们都可以找到一个唯一的函数q :: C -> A，它是 F-代数态射。这意味着，q必须使法律q . fix = p . fmap q成立。我们需要证明，给定A和p，这样q的存在并且是唯一的。

这两个语句不等价；但证明（2）意味着（1）。（Lambek 定理说初始代数是同构。）

fix函数的代码unfix可以相对容易地编写：

给定一个函数p :: F A -> A，函数的代码q写成

然而，似乎很难直接证明函数fix, unfix,q满足所需的性质。我找不到完整的证明。

C证明它是一个初始代数，即它q是唯一的，比证明它更容易fix . unfix = id吗？

在这个问题的其余部分，我将展示一些我能够为证明fix . unfix = id.

仅通过使用给定的函数代码来证明 (1) 或 (2) 是不可能的。我们需要额外的假设。与米田身份相似，

我们需要假设函数的代码是完全参数化的（没有副作用，没有特别选择的值或固定类型），以便可以应用参数化定理。所以，我们需要假设类型只包含满足适当自然法则C的类型函数。forall r. (F r -> r) -> r

参数化定理为这种类型签名给出了以下自然法则：对于任何类型Aand B，以及对于任何函数p :: F B -> Aand f :: A -> B，函数c :: forall r. (F r -> r) -> r必须满足等式

Using this naturality law with appropriately chosen pand f, one can show that the composition fix . unfixis a certain function of type C -> Cthat must be equal to \c -> (run c) fix.

然而，证明的进一步进展似乎是不可能的。不清楚为什么这个函数必须等于id。

让我们暂时定义函数m：

然后我得到的结果写成

也可以证明这一点unfix . fix = fmap (m fix)。

这还有待证明m fix = id。一旦证明了这一点，我们就证明了F C ≅ C。

相同的自然规律c与不同的选择p并f赋予了奇怪的身份

但不知如何从这个身份中推导出来m fix = id。

如何用 lambda 项表示以下函数？

如果 n != 0，则 f(n) = T。如果 n = 0，则为 F。

n 代表教堂数字。

我知道 0 := λf.λx.x 其中 λx.x 是恒等函数，所有其他自然数可以用 n := λf.λx.f (f ... (fx)) 表示，其中包含 fn 倍比 0 项。例如 3 := λf.λx.f (f (fx))。

但是我怎样才能为上面的函数推导出一个有效的 λ 项呢？我想我也需要获得 T/F。因此我可以用 λf.(λxy.fxy) 来表示数字 n，对吧？但是F和T呢？以下是上述函数的正确 λ 项吗？λf.(λxy.fxy(yFT)) 其中 T=λxy.x 且 F=λxy.y？

我正在尝试定义一个采用整数并以 Church 数字返回其表示的过程。任何人都可以帮我弄清楚我犯的错误吗？以下代码是我迄今为止能够做到的。

当我运行测试时：

我收到以下错误：

它似乎在期待一个数字？但给出了一个程序。我认为哪个符合程序的意图？感谢您对新手的帮助和评论。

我正在使用 OCaml 编译器进行练习，我正在做一个小任务，我们必须实现教堂数字，定义为：

zz = pair c0 c0; ss = λp. pair ( snd p) ( plus c1 (snd p)); prd = λm. fst (m ss zz );

并计算我想要实施的 ss 加：

plus = λm. λn. λs. λz. m s (n s z)

所以我的问题是，如何实现函数加，比如 n 次 succ 0？

我试过 了，plus = lambda m. lambda n. lambda s. lambda z. m s (n s z); 但在编译器中不正确。

我注意到我在 OCaml 编译器中工作，并将我的所有函数都写在 func.f 文件中而不是 .ml 文件中

https://www.cis.upenn.edu/~bcpierce/tapl/代码来自那里，fulluntyped 文件夹

我正在通过 SICP 工作，它zero为Church Numerals提供了以下定义：

我对此有几个问题：

1. 为什么语法复杂？只需使用以下内容，它似乎就很易读了：

   我们可以看到它是一个被调用的函数zero，它接受一个（未使用的）参数f并返回一个参数的函数，该函数将返回其参数。似乎该定义只是为了尽可能不直截了当。

2. 那里有什么x用？例如做类似的事情：

   返回100。只是x返回默认值吗？

继上一个问题之后，我询问了有关编写 curry 函数的问题，How to create a make-curry function like racket has，我已经开始编写 0、1、2 的固定大小写——它们与 Church Numerals 非常相似很整洁。这是我到目前为止所拥有的：

模式似乎是：

但是，我在“构建”n 嵌套 lambda 表达式时遇到了一些麻烦。我想我可以用类似的东西构建一个嵌套的 lambda：

但我不确定如何将变量“绑定”到每个 lambda 函数，以及如何最终将这些相同的变量（按顺序）传递给(func x1 x2 ... xn)函数。

这是不正确的，但我已经开始沿着......

怎么可能做到这一点？

好吧，假设我在教堂编码中有一组功能定义（带有语法树）：

给出定义 λx -> λy -> y，很清楚如何返回命名定义，应用与 alpha 等价的匹配就足够了。

但请考虑以下示例：

因此，当 3 遭受 beta 减少时，它将展开为某种定义，例如：

您可以看到术语很容易变大，当然，由于术语的大小，这不是表示纯数据的好方法。所以，我想知道是否有一种算法能够在经过评估后有效地重新命名每个定义。它们 3_unfolded 将再次变为 (succ (succ (succ 0)))，通过给出自然教堂编码的定义集（0，并且只有 succ）。

我知道有一些副作用，比如模棱两可的表示，但让我们忽略它（例如，如果你扩展 succ 的相同定义并重命名为 succ_2）。