问题标签 [lambda-calculus]

我试图弄清楚如何为下面的表达式绘制语法树。首先，这究竟是如何表现的？看起来它需要 1 和 2 作为参数，如果n是 0，它只会返回m。

另外，有人可以指出解析树的起点，还是一个例子？我一直找不到。

我很好奇Kiselyov 和 Shan 在Function Pearl: Implicit Configurations文章 中讨论的对隐式参数的反对意见。

在存在隐式参数的情况下内联代码（β-reduce）是不合理的。

真的吗？我希望 GHC 应该内联到与传递的隐式参数相同的范围，不是吗？

我相信我理解他们的反对意见：

如果添加、删除或更改术语的签名，则术语的行为可能会发生变化。

GHC 的用户文档解释说，程序员必须注意多态递归和单态限制。这是否是他们所说的内联问题的意思？

我认为这个多态递归示例也涵盖了“对隐式参数进行泛化”的含义？还要别的吗？

Data.Reflection中的ReifiesStorable类型类真的是解决这些困难的明智之选吗？它似乎在每次访问时都会反序列化整个隐式数据结构，这听起来对性能来说是灾难性的。例如，我们可能希望我们的隐含信息是 Cayley 表或字符表，它们占据了 ram，并且必须在数百万次代数运算期间访问。

是否有一些更好的解决方案使用隐式参数，或者编译器可以在幕后轻松优化的另一种技术，同时仍然通过使用状态线程或其他方式的类型系统保证更多？

哪种 FP 语言在代码外观、感觉和行为上与 lambda 演算抽象最接近？

在学习函数式编程时，我看到过多次引用Church Rosser 定理，尤其是菱形属性图，但我没有遇到过很好的代码示例。

如果像 Haskell 这样的语言可以被视为一种 lambda 演算，那么一定可以使用该语言本身来举出一些例子。

如果该示例很容易显示步骤或减少如何导致易于并行化的执行，我会给予奖励积分。

我需要为我的学校作业消除这个 Scheme lambda 结构。

任何想法如何做到这一点？

我在 Haskell 中实现了一个不纯的无类型 lambda 演算解释器。

我目前坚持实施“alpha-congruence”（在某些教科书中也称为“alpha-equivalence”或“alpha-equality”）。我希望能够检查两个 lambda 表达式是否相等。例如，如果我在解释器中输入以下表达式，它应该产生 True（\用于指示 lambda 符号）：

问题是了解以下 lambda 表达式是否被认为是 alpha 等效的：

在这种情况下，\x.xy == \y.yx我猜答案是True。这是因为\x.xy => \z.zyand\y.yx => \z.zy和 两者的右侧相等（符号=>用于表示 alpha 减少）。

\x.yxy == \z.wzw我也猜想答案是True。这是因为\x.yxy => \a.yay和\z.wzw => \a.wawwhich（我认为）是平等的。

问题是我所有教科书的定义都指出，只有绑定变量的名称需要更改，两个 lambda 表达式才能被视为相等。它没有说明表达式中的自由变量也需要统一重命名。因此，即使y和w都在 lambda 表达式中的正确位置，程序如何“知道”第一个y代表第一个w，第二个y代表第二个w。我需要在实现中对此保持一致。

简而言之，我将如何实现函数的无错误版本isAlphaCongruent？为了使它起作用，我需要遵循哪些确切的规则？

我宁愿在不使用 de Bruijn 指数的情况下这样做。

我有一个有趣的问题，但我不确定如何表达它......

考虑 lambda 演算。对于给定的 lambda 表达式，有几种可能的归约顺序。但其中一些不会终止，而另一些会终止。

在 lambda 演算中，事实证明存在一个特定的归约顺序，如果确实存在一个不可约解，则它保证总是以不可约解结束。它被称为正常订单。

我写了一个简单的逻辑求解器。但问题是，它处理约束的顺序似乎对它是否找到任何解决方案有巨大的影响。基本上，我想知道我的逻辑编程语言是否存在类似正常顺序的东西。（或者仅仅是一台机器不可能确定性地解决这个问题。）

所以这就是我所追求的。据推测，答案主要取决于“简单逻辑求解器”究竟是什么。因此，我将尝试简要描述它。

我的程序非常基于The Fun of Programming (Jeremy Gibbons & Oege de Moor) 第 9 章中的组合器系统。该语言具有以下结构：

• 求解器的输入是单个谓词。谓词可能涉及变量。求解器的输出是零个或多个解。解决方案是一组使谓词变为真的变量赋值。

• 变量包含表达式。表达式是整数、变量名或子表达式的元组。

• 有一个相等谓词，它比较表达式（不是谓词）是否相等。如果用它的值替换每个（绑定的）变量使两个表达式相同，则满足。（特别是，每个变量都等于它自己，无论是否绑定。）这个谓词是使用统一来解决的。

• 还有用于 AND 和 OR 的运算符，它们以明显的方式工作。没有 NOT 运算符。

• 有一个“存在”运算符，它本质上是创建局部变量。

• 定义命名谓词的工具支持递归循环。

关于逻辑编程的“有趣的事情”之一是，一旦你编写了一个命名谓词，它通常会向前和向后工作（有时甚至是横向工作）。典型示例：连接两个列表的谓词也可用于将列表拆分为所有可能的对。

但有时向后运行谓词会导致无限搜索，除非您重新排列术语的顺序。（例如，交换 AND 或 OR somehwere 的 LHS 和 RHS。）我想知道是否有一些自动方法来检测运行谓词的最佳顺序，以确保在解决方案集完全正确的所有情况下立即终止有限。

有什么建议么？

在阅读 Wiki 中的 Lambda Calculus 时，遇到了Capture-avoiding substitutions一词。有人可以解释它的含义，因为我在任何地方都找不到定义。

谢谢

附言

我想知道的是告诉操作Capture-avoiding substitutions的原因。如果有人能做到这一点，那将是一个很大的帮助

我对 lambda 演算非常陌生，在阅读教程时遇到了这个问题。这是我的方程式。

现在如果我们应用另一个术语，比如说 F (YF)，那么我们如何才能减少它。如果我根据 beta 减少是正确的，我们可以将(ƛx.f(xx))中 的所有f替换为(ƛx. f(xx))，这是正确的，如果是，我们该怎么做。

谢谢

当我在阅读 lambda 演算时，遇到了Lambda 可定义性这个词。有人可以解释那是什么，因为我找不到任何好的资源。

谢谢