是否有无类型 lambda 演算的解释器（或编译器）？ （根据this thread 这是可能的。）我认识到它作为一种编程语言几乎没有用处，特别是如果许多语言（例如数字和布尔运算符）被实现（由用户或由库）在语言本身。但是，我仍然认为这将是一个有趣的工具，对学习和探索微积分很有用。为此，解释器比编译器更可取，两者都可以。有人知道这样的程序吗？
【问题讨论】：
标签： compiler-construction functional-programming interpreter lambda-calculus untyped-variables
您可以使用任何具有 lambda 抽象的无类型语言。例如 Python 或 JavaScript。有两个主要缺点：
知道了这一点，让我们用 Python 做一个例子： 首先，我们创建辅助函数来在数字和 Church 数字之间进行转换：
# Construct Church numeral from an integer
def int2church(n):
def repeat(f, m, x):
if (m == 0): return x
else: return f(repeat(f, m-1, x))
return lambda f: (lambda x: repeat(f, n, x))
def church2int(l):
return l(lambda x: x + 1)(0)
现在我们可以定义数字的标准运算了：
zero = int2church(0)
one = int2church(1)
pred = lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f)))(lambda u: x)(lambda u: u)
mul = lambda m: lambda n: (lambda f: m(n(f)))
expn = lambda n: lambda m: m(n)
tetra = lambda n: lambda m: m(expn(n))(one)
并计算例如 43:
expn = lambda n: (lambda m: m(n))
a = int2church(4)
b = int2church(3)
print church2int(expn(a)(b))
a = int2church(5)
b = int2church(2)
print church2int(tetra(a)(b))
为了能够表达更有趣的东西，我们可以定义 Y 组合子：
y = lambda f: (lambda x: f(lambda v: x(x)(v))) (lambda x: f(lambda v: x(x)(v)))
并计算例如阶乘：
true = lambda x: (lambda y: x)
false = lambda x: (lambda y: y)
iszero = lambda n: n(lambda x: false)(true)
fact = y(lambda r: lambda n: iszero(n)(one)(mul(n)(lambda x: r(pred(n))(x))))
print church2int(fact(int2church(6)))
请注意，Y 组合器必须适应使用 η-expansion 的严格评估，以及阶乘函数以避免由于严格评估而导致的无限递归。
【讨论】：
Benjamin Pierce 提供了 implementations 中的 untyped 和 simply-typed λ 微积分，随他的教科书 Types and Programming Languages。它们是用 OCaml 编写的，并包含示例定义。不过，为简单的 λ-calculi 编写解释器或编译器应该不难。
【讨论】：
使用一些技巧，几乎可以在任何函数式语言中做到这一点。至少我在 Haskell 和 OCaml 中看到过类似的东西。但是，有时您必须绕过类型系统的限制。通常，您通过将其实现为统一系统来获得“无类型”功能。所以每个 lambda 函数都会有类型
type lambda = lambda -> lambda
在默认设置中，例如 OCaml 不允许这样的递归类型，但可以通过定义来规避：
type lambda = L of lambda -> lambda
【讨论】：
我是函数式编程课程的助教。出于教学目的，我们在网上看到这个lambda calculus reducer 是一个有趣且有用的工具来探索微积分。如果您想使用它，他们也有可用的 SML 源代码。
【讨论】：
我写了一篇，今年早些时候。 Here it is.
【讨论】：
我为基于 lambda 演算的语言创建了一个 web hosted interpreter，我称之为 pureƒn，以努力学习 Lambda 演算的工作原理。对于希望以交互方式以最小的符号复杂度学习和体验计算机科学的一些基本原理的人来说，它可能会很有用。
pureƒn 是一个基于 Lambda 演算功能的编程环境，但具有简化的符号。 pureƒn 允许定义、应用和减少功能抽象。符号和语法是最少的，但足以让基本概念易于理解。
底层编译器是用 Python 编写的，并将抽象编译成函数，这些函数在相互应用时会自动归约为正常形式（如果可能）。这意味着如果您定义 S、K 和 I 组合函数，然后将它们作为 SKK 应用，则返回的函数将是 I 函数，而不仅仅是行为类似于 I 的函数，这意味着以下情况将成立：
>>>S(K)(K) is I
True
【讨论】：
Here 是用 Python 编写的。它看起来很不成熟，但它是实现一个 Python 的一个有趣的开始。这取决于模块ply。
Here 是 C++ 的另一种（有点）——非常有趣。
如果您的主要目的是在学习 lambda 演算（例如，尝试为自己推导算术运算）和特定的 Church 数字和布尔值中获得一些基本的自动化，那么一个简单但易于实施的解决方案是限制自己到 Python 的一个小子集，您可以在其中定义自己的 Church 数字和运算符，并通过将它们转换为常规 Python 类型的函数来检查它们。为 Church 数字执行此操作的函数：
lambda churchnum: churchnum(lambda x: x+1)(0)
还有一个用于教堂布尔值：
lambda churchbool: churchbool(True)(False)
【讨论】：