compiler-construction - 无类型 Lambda 演算的函数式语言

Question

是否有用于无类型 lambda 演算的解释器(或编译器)？ (根据 this thread 这是可能的。)我认识到它作为一种编程语言几乎没有用，特别是如果大部分语言(例如数字和 bool 运算符)都已实现(由用户或库实现)在语言本身。但是，我仍然认为这将是一个有趣的工具，可用于学习和探索微积分。为此，解释器比编译器更可取，两者都可以。有人知道这样的程序吗？

Answer 1

您可以使用任何具有 lambda 抽象的无类型语言。例如 Python 或 JavaScript。有两个主要缺点:

这些语言没有惰性求值。这意味着并非所有 lambda 项都会收敛，即使它们具有范式。您必须考虑到这一点并相应地修改任务。

您不会将结果视为正常形式的 lambda 项。您必须知道对结果的期望并使用语言将其评估为可以显示的内容。

知道了这一点，让我们用Python做一个例子:
首先，我们创建辅助函数来在数字和教堂数字之间进行转换:

# 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))

或 tetration :

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)))

请注意，必须使用 η-expansion 调整 Y 组合器以进行严格评估。 ，以及避免由于严格评估而导致无限递归的阶乘函数。