问题标签 [lambda-calculus]

我正在寻求解释如何证明计算模型是等价的。我一直在阅读有关该主题的书籍，但省略了等价证明。我对两个计算模型等效意味着什么有一个基本概念（自动机视图：如果它们接受相同的语言）。是否有其他思考等价的方法？如果你能帮助我理解如何证明图灵机模型等价于 lambda 演算，那就足够了。

在简单类型的 lambda 演算中类型推导是唯一的证明在纸上是微不足道的。我熟悉的证明是通过对类型推导的完全归纳来进行的。但是，我无法证明通过类型派生类型表示的类型派生是唯一的。在这里，如果变量的类型为 environment ，则谓词dec Γ x τ为真。类型谓词像往常一样定义，只需读取简单类型 lambda 演算的类型规则：xτΓJ

J在证明类型派生是唯一的时，我无法暴露类型术语的结构。例如，我可以对以下引理中的任何一个d1或d2在其中进行归纳，但不能对d1then destruct进行归纳d2，反之亦然。Coq 给出的错误消息（对术语进行抽象会导致输入错误的术语）有点模糊，并且 Coq wiki 没有提供任何帮助。作为参考，这是我试图证明的引理：

在归纳术语时我没有问题，例如，在证明类型是唯一的时。

编辑：我添加了最少数量的定义来说明我遇到问题的结果。作为对 huitseeker 评论的回应，之所以选择这种类型J是因为我想将派生类型作为结构化对象进行推理，以便执行提取等操作并证明唯一性等结果，这是我以前在 Coq 中没有做过的。

针对评论的第一部分，我可以执行inductionor d1，d2但执行后induction我不能使用destruct, case, orinduction剩下的术语。这意味着我不能公开两者的结构，d1并且无法d2对这两个证明树进行推理。当我尝试这样做时收到的错误表明，对剩余术语进行抽象会导致术语输入错误。

我已经尝试过从库中获得dependent induction一些结果Coq.Logic，但没有成功。推导是独一无二的，这似乎是一个容易证明的命题。

对我提出问题的愚蠢方式感到抱歉，这里有一些解释：我正在用 javascript 中的 lambda-calculus 进行试验，但遇到了一些小困难。（你不必知道任何关于 lambda 演算的知识来帮助我）

我有这个功能（教堂数字 1 顺便说一句）：

表现如预期，并给出与上面完全相同的东西。

表现出乎意料并给出：

为什么javascript不用函数num1替换'c'？但

给出：

并表明第一个 c 实际上已按预期被函数替换。如果'c'不会被替换，那么就会发生这种情况：

所以总而言之，代码正在做它应该做的事情，但它不会输出替换了“c”的函数。我能做些什么？稍后，我将使用更多功能，然后我将无法区分num1(asd)，num1(jkl)因为“c”没有被替换。

非常感谢您的帮助！

别人

我打算在 Java 中做一些基本的 lambda 表达式操作（最好使用类型化的 lambda）。

是否有我使用的库（稳定或其他）？

更新：更明确地说，我想操作 lambda 表达式，例如在一个文件中我解析一些 lambda 表达式并将其中一些组合成一个新的。基本上，它更多的是解析而不是函数式编程。

我发誓曾经有一件T 恤出售，上面印着不朽的文字：

哪一部分

你不明白吗？

就我而言，答案是……全部！

特别是，我经常在 Haskell 论文中看到这样的符号，但我不知道它是什么意思。我不知道它应该是什么数学分支。

我当然认识希腊字母表中的字母和诸如“∉”之类的符号（这通常意味着某物不是集合的元素）。

另一方面，我以前从未见过“⊢”（维基百科声称它可能意味着“分区”）。我也不熟悉这里的 vinculum 的使用。（通常，它表示分数，但这里似乎并非如此。）

如果有人至少可以告诉我从哪里开始寻找理解这个符号海洋的含义，那将很有帮助。

在 Agda 中， a 的类型以如下方式forall确定：Set1Set1SetASet

但是，以下具有类型Set：

我知道如果Set有 type Set，会有矛盾，但我看不出，如果上述三个术语中的任何一个有 type Set，我们就会有矛盾。这些可以用来证明False吗？它们可以用来证明Set : Set吗？

这是一个阿尔法转换。虽然我已经完成了这个，但我不太确定这是否是一个正确的答案。

这是一个正确的答案吗？

Lambda 项可以是：

• 多变的
• lambda 抽象（例如\x.t）
• 应用。如果t和s是lambda 项，那么ts是一个应用程序。

因此，在左侧（例如(\x.t)a）具有抽象的应用程序看起来不错。它看起来像函数调用。但是当左侧部分是变量或其他应用程序时，应用程序意味着什么？是什么意思ab，((\x.x)a)b或者a(\x.x)如果a和b是变量？

下面是我发现难以减少的 lambda 表达式，即我无法理解如何解决这个问题。

(λmn(λsz.ms(nsz)))(λsz.sz)(λsz.sz)

我迷失了。

如果有人能带领我朝着正确的方向前进，将不胜感激

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

这有效：

发生检查失败：

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