一旦在 lambda 演算中找到了解决方案，将其转换为代码有多容易？答案

【问题标题】：Once a solution has been found in lambda calculus, how easy is it to convert this to code?一旦在 lambda 演算中找到了解决方案，将其转换为代码有多容易？
【发布时间】：2012-04-18 06:21:16
【问题描述】：

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

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

【问题讨论】：

我相信（但不能/不会证明）将用简单类型的 lambda 演算编写的任何程序转换为 Haskell 是微不足道的（您可以在无类型的 lambda 演算中编写一些函数你不能用 Haskell 写）。 Glasgow Haskell deugars to SystemF - 粗略地说是简单类型的 lambda 演算的更强大版本 - 所以 Haskell 已经“包含”了 STLC。您的翻译只需要转换为未加糖的 Haskell 的一小部分子集 - 自然，结果会非常冗长且不惯用。
@stephentetley：事实上没有什么可以证明的。翻译很简单，λx:τ. M 被翻译成\(x :: τ) -> M 并且函数应用程序M N 保持不变。无类型的 lambda 演算会出现问题，因为有些术语在没有滚动/展开无限类型的情况下无法输入（非常好的示例是 Y 组合器）。

标签： haskell functional-programming lisp lambda-calculus

【解决方案1】：

Haskell 的语法与 lambda 演算非常相似。您的问题是 Haskell 的类型检查器不会接受无类型 lambda 演算中的某些术语。

出于好奇，谁地狱使用 lambda 演算解决了 TopCoder？那听起来很不平凡。 o_O

【讨论】：

所以从这个意义上说 Lisp 可能更容易翻译，因为它也是无类型的？
我在睡眠中有高级（无意识）的想法。我的猫在凌晨 3 点叫醒了我，这就是我的意识。我在脑海中听到了这个问题，并开始考虑使用 lambda 演算作为问题的中间表示。我会这样做是因为它可以允许将冗长的问题陈述转换为纯象征性的东西。理想情况下，这样的结果将是一个简单的、简单的计算问题，而不是高级描述。本质上，目的是将“现实世界”系统简化为数学/计算系统。
(λnmfx. n(mf)x)(λfx. f(fx))(λfx. f(fx)) 是一个非常、真的罗嗦的方式来表达2 + 2。 ;-)

【解决方案2】：

这是一个很难的问题。理论上，是的。在实践中，有点。一般来说，我会说定义的可计算函数可以有效地实现（在程序员努力的时间空间内），是的，但这实际上取决于对编程语言和所讨论数学的熟悉程度，而不是这样做的可能性.例如，我想可以实现一个 lambda 演算解释器，我将您引导至 ['Visual Automata Simulator]'1，以获取包含在平凡包装器中的图灵模型示例。

【讨论】：

“我想可以实现一个 lambda 演算解释器”——是的，很容易。无类型 lambda 演算是类型和编程语言中呈现的一系列日益复杂的语言中的第一个。实现在 OCaml 中：cis.upenn.edu/~bcpierce/tapl
那本书的介绍：“类型系统是一种在程序中强制执行抽象级别的语法方法。”失败！