无类型Lambda演算的功能语言

Question

是否有无类型lambda演算的解释器(或编译器)？(根据这个帖子,它是可能的.)我认识到它作为一种编程语言几乎没有用处,特别是如果大部分语言(例如数字和布尔运算符)是由用户或库实现的.语言本身.但是,我仍然认为这对学习和探索微积分很有用.对于这个,解释器比编译器更可取,因为它们可以工作.有谁知道这样的节目？

Answer 1

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

1. 这些语言没有懒惰的评估.这意味着并非所有lambda术语都会收敛,即使它们具有正常形式.您必须考虑到这一点并相应地修改任务.
2. 您不会将结果视为正常形式的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)

并计算例如4 ³:

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

注意,Y组合器必须适合于使用η-展开进行严格评估,以及因为严格评估而避免无限递归的阶乘函数.

Answer 2

本杰明·皮尔斯提供了实现的的非类型化和简单类型的 λ演算伴随着他的教科书类型和编程语言.它们是用OCaml编写的,包含示例定义.然而,为简单的λ-calculi编写解释器或编译器并不困难.