问题标签 [lambda-calculus]

我刚刚找到了以下 lambda 演算表达式：

所以这是一个函数，它接受一个参数 f 并返回另一个函数，该函数接受一个参数 x 并产生 x 应用于 f 的结果。上述表达式的结果将是 (λ b . b)。

这让我想起了部分应用程序和柯里化，但是“由内而外”的函数应用程序 (fx) 引起了我的兴趣。

这个表达有更深层次的理论意义吗？

在“类型和编程语言”的 6.1.2 节中，他们讨论了用于对 lambda 表达式中的自由变量进行编号的命名上下文。使用他们提供的示例方案，两者都λx.xb将λx.xx具有其 de Bruijn 表示，λ.00因为它们显然是不同的术语。这是如何运作的？

我正在研究编译器/证明检查器，我想知道是否有这样的语法树，例如：

如果有办法检查Exprs 的 alpha 等价（等价模重命名）。然而，这Expr与 lambda 演算的不同之处在于 lambda 中的变量集是可交换的——即参数的顺序不会影响检查。

（但是，为了简单起见，Lambda ["x","y"] ...它与 不同Lambda ["x"] (Lambda ["y"] ...)，在这种情况下，顺序确实很重要）。

换句话说，给定两个Exprs，如何有效地找到从一个重命名到另一个的重命名？这种组合问题有 NP 完全问题的味道。

我记得在某处读到 Hindley Milner 是对 system-f 的限制。如果是这样的话，有人可以向我提供一些可以在 system-f 中输入但不能在 HM 中输入的术语。

考虑这个组合器：

将其应用于参数 XY：

它签订合同：

我将 S (SK) 转换为相应的 Lambda 项并得到以下结果：

我使用 Haskell WinGHCi 工具获取 (\xy -> xy) 的类型签名并返回：

这对我来说很有意义。

接下来，我使用 WinGHCi 获取 s (sk) 的类型签名并返回：

这对我来说没有意义。为什么类型签名不同？

注意：我将 s、k 和 i 定义为：

我现在了解的类型签名s (s k)：

我可以在 Haskell WinGHCi 工具中创建可以正常工作的示例：

示例：

返回2。

示例：

返回4。

其中successor定义为：

尽管如此，我仍然没有直观的感觉s (s k)。

组合s (s k)器采用任意两个函数f和g。和s (s k)有什么作用？你能给我大局观吗？fgs (s k)

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

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

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

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

我正在重写这个问题，因为它的格式很差。

我有上面的代码，它对 lambda 表达式（这是我想要的）进行 lambda 缩减。我的问题是，有人可以帮我重写这个实现（因为我对Scheme没有那么经验），以便我从正文中提取进行alpha转换的部分并将其放在单独的函数中，以及执行的部分β-减少也是如此。函数 reduce 是递归的，所以两个新创建的函数需要是单步的，这意味着它们将只转换一个有界变量并只减少一个表达式。

我指的是这个问题

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

我正在考虑我可以在 Churchlists 上实现哪些其他列表功能，并成功编写了一个 conc2 函数来连接 2 个教堂列表

我还尝试了一个 zipWithChurch，它在普通列表上的运行方式与 zipWith 类似。但我找不到解决方案。谁能帮我？

如果您要阅读问题陈述，例如在 TopCoder 上找到的内容，并将其转换为 lambda 演算表示，那么将其“转换”为 Haskell 或 Lisp 代码是否是一个简单的练习？

换句话说，是否可以使用 lambda 演算形式系统解决问题，然后用函数式编程语言轻松实现？