问题标签 [church-encoding]

对于正整数的 Church 编码N，可以定义一个递归原理nat_rec：

equal_rec以下 Churchequal平等编码的递归原则是什么？

在以下代码中，该语句add'_commut被 Coq 接受，但add_commut由于 Universe 不一致而被拒绝。

如何让它通过？

人们可以轻松地对这样的对进行 Church-encode：

然后很容易将其推广到这样的依赖对：

但是最后一个定义失败并显示错误消息：

我理解这里的问题。但是解决方案是什么？换句话说，如何对依赖对进行 Church 编码？

我已经实现了 CEK 机器。鉴于该算法的闭包结果以及该闭包是 Church 编码数字的知识，打印出数字的最佳方法是什么？

使用以下类型：

编辑：为了让这个模糊的问题更清楚一点：用(\n f x -> f (n f x)) (\f x -> x)( s z) 启动我的机器，我最终得到：

这是一个数据结构，表示代表教堂数字的闭包。我怎样才能将此结构具体化为一个数字？我是否必须遍历闭包的环境并替换Term（听起来效率低下）中的变量？我需要为此重命名吗？

编辑：实际代码：

结果是：

我想使用 Agda 作为我的类型检查器和评估器来测试系统 F 中的一些定义。

我第一次尝试介绍 Church 自然数是通过写作

这将像常规类型别名一样使用：

然而，定义Num不输入（种类？）检查。使其工作并尽可能接近系统 F 表示法的最合适方法是什么？

我是函数式编程和 F# 的初学者。作为一个练习，我试图实现教堂数字。
首先，我将数字编码为：

然后我编写了辅助函数来查看我的数字是否有效：

例如：

正如预期的那样打印 3。
我还实现了一些算术函数：

所有这些似乎都工作正常：

但我真的很难实现减法：

上面的方法看起来像某种指数而不是减法。
我也试过（正如维基建议的那样）：

但是当我尝试使用它时会导致类型不匹配：

我被卡住了，我做错了什么？我也很感激任何关于如何改进我的代码的建议。

我正在尝试将 Church Encoding 转换为数字。我已经定义了我自己的 Lambda 定义如下：

我已经写了一个数字到教堂编码的转换，它可以按照我的预期工作，这是我定义它的方式：

我运行了自己的测试，这是测试 0、1 和 2 时终端的输出：

现在我正试图做相反的事情，我只是无法围绕需要传递的论点。这是我所拥有的：

我尝试替换(App e (Var x))为，(Var x)但是当我尝试测试将教堂编码从 0 转换为 Just 0 的基本情况时，我都遇到了这个错误：

我理解 3 个数字的 lambda 编码的方式是这样的：

0：\s。\z。z

1：\s。\z。sz

2：\s。\z。小号 (sz)

所以我认为我的逻辑是正确的，但我很难弄清楚反向转换是如何进行的。我对 Haskell 相当陌生，因此非常感谢任何帮助解释我可能做错的事情。

我正在使用免费库中的FreeT类型来编写这个“运行”底层的函数：StateT

但是，我正在尝试将其转换为FT，教堂编码版本，而不是：

但我的运气不太一样。我得到的每一种组合似乎都不太奏效。我得到的最接近的是

但是第一个洞m r -> StateT s m r的类型是，第二个洞的类型是StateT s m r -> m r......这意味着我们必然会在这个过程中失去状态。

我知道所有FreeT功能都可以用FT. 有没有一种不涉及往返的好方法来编写这个FreeT（也就是说，以一种需要明确匹配Pureand的方式Free）？（我尝试过手动内联事物，但我不知道如何使用s定义中的不同 s来处理递归runStateFree）。或者这可能是显式递归数据类型必然比教堂（mu）编码更高效的情况之一？

关于本科水平计算机科学的主题。
在复习该理论时，我遇到了一个令人烦恼的问题，即关于(0 m)lambda 演算中教堂数字的取幂。
据我所知，(0 m)当减少结果时λx. x，这不是1 (= m^0)预期的，甚至不在教堂的数字内。

我在由教堂编码编码的 lambda 演算中采用自然数的 n，通常如下所示

n := λfx. (f^n x) = (f ... (f x))

很多文献都这么说

EXP(m, n) := λmn. (n m)

返回m^n给定m和n教堂的数字，我知道该功能在大多数情况下都能正确响应。但情况并非如此，n = 0因为

(0 m) = ((λfx. x) m) → λx. x

在数学中，1是自然数的单位元，被视为一个乘法群，即对于中x * 1 = 1 * x的任何一个。因此，如果我以以下形式设置功能xNEXP

EXP’(m, n) := λmn. (n (MUL m) 1)

因为MUL(m, n) = m * n，这似乎工作正常，与数学m^0中经常定义的事实相吻合。1在超操作的意义上，这似乎也很简单。

超操作： https ://en.m.wikipedia.org/wiki/Hyperoperation

我预计会有一些批评，比如m^0不一定1是数学，而死板的数学家会说这一切都取决于定义。但是，采用前一种风格是否有任何合乎逻辑的支持EXP(m, n)？当 时它不会返回教堂的数字n = 0，所以对我来说似乎仍然定义不明确。

问题是

1. “为什么定义EXP(m, n) := λmn. (n m)通常被接受，m^n即使它的输出可以是非教堂的数字，用于教堂的数字输入？”</p>

2. “你知道任何轻微的修正，EXP因此该功能适用​​于所有教堂的数字输入吗？”</p>

3. “对我的批评有任何问题或误解(0 m)。”</p>

另外，作为函数组合的单位元的(0 m)to be的结果是否有逻辑背景λx. x，而不是 1？这只是巧合还是我想得太认真了？

欢迎任何想法。

如有必要，我想遵循与教堂数字相关的代数的维基百科定义。

教会的编码：https ://en.m.wikipedia.org/wiki/Church_encoding

谢谢。

对于 Church 数字的后继和前任，我有以下代码：考虑以下代码：

假设我在 pred 函数中进行了以下更改：

返回 x 和 (x) 有什么区别？返回 (x) 在语法和逻辑上究竟意味着什么？