Lambda 演算减少

Question

我能够做简单的 Lambda 演算减少但是，我不知道如何做那些获得 “currying”。

这是我想不通的两个例子：

1. ( ( ( lambda x . ( lambda y . ( j y ) ) ) j ) m )
2. ( ( lambda p . ( p j ) ) ( lambda x . ( q x )))

Answer 1

备注 评价有误，改为j m，所以自申请部分不相关。

Currying 是观察到您可以以不同方式查看一系列 lambda 抽象：

在数学术语中，( ( lambda x . ( lambda y . ( j y ) ) ) 可以被命名，然后写成：f(x,y) = j(y)。在您的示例中，您将评估 f(m,j) = j(j)。那么，如果我们对 f 没有两个论据，会发生什么？我们不能完全评估它，但我们可以定义一个新函数 g(y) = f(j,y)，我们只需插入第一个参数。这种逐步函数求值称为部分求值或柯里化。

在 lambda 演算中，这两个方面看起来完全一样。如果你想将两个参数都应用到你的术语中，你可以从第一个参数开始：

你的初始函数 f(m,j): ( ( ( lambda x . ( lambda y . ( j y ) ) ) j ) m ) 减少到 g(j): ( ( lambda y . ( j y ) ) ) j。当我们继续我们的评估时（我们仍然可以将我们的函数应用于 j），我们到达 j(j)：j j。现在我们不能再应用任何缩减规则，所以我们可以将j j 视为我们的计算结果。我们的结果是一个应用程序很好，但它被应用到它本身是很特别的。

（其余的不再与柯里化有关，而是与自我应用有关，这与@Matt 所写的内容有关）

也许应该解释一下这意味着什么：函数 j 将自己作为参数。有了这个，你可以实现递归。著名的 Y 组合子 Y：(lambda x . f x x) 正是这样做的：如果计算 Y Y，即 (lambda x . f x x) Y，则计算 f (Y Y)。当您再次评估内部 Y Y 时，您计算 f f (Y Y) 等等。这正是函数f 的递归应用。副作用是，对于某些f，评估将永远不会终止（如果您使用标识函数(lambda x.x)，则已经终止）。

20 世纪中叶的逻辑学家希望将 lambda 演算用作数据结构，其中应该禁止无限的求值序列。限制 lambda 演算的一种可能性是为每个变量赋予一个类型（非常类似于编程语言中的类型）。如果你想将一个变量应用到另一个变量，类型需要适合。

例如假设x 是int 类型，那么在应用程序f x 中，f 需要是一个类型，它接受int 类型的变量并计算结果，假设是string 类型.然后我们可以将 f 的类型写为int -> string。 f x 的类型是 string，因为这是我们在 x 上计算 f 时得到的。

抽象创造了一个新的功能。例如(lambda x . x)需要int类型的参数并产生int类型的术语，即它是int -> int类型。

但是现在像j j 这样的自我应用程序不再起作用了：假设内部j 的类型为t。那么外部 j 必须是 t -> t 类型。使这项工作的唯一方法是您的类型是t 的无限嵌套，这通常是被禁止的。

尽管这种方法似乎有点局限，但您可以在类型化 lambda 演算之上添加递归来构建 Haskell 或 OCaml 等编程语言。

Answer 2

假设您正在谈论使用按值调用评估策略的简单类型的 lambda 演算，第一个 reduce 像这样：

1. ( ( ( lambda x . ( lambda y . ( j y ) ) ) j ) m ) -- 用x 替换j
2. ( ( lambda y . ( j y ) ) m ) -- 用y 替换m
3. (jm)
4. 从这里开始，你被卡住了......

通常没有将变量应用于变量的缩减规则。这通常是我们使用类型系统的原因，以确保对于任何类型良好的程序，在评估时我们不会像第 3 步那样“卡住”。

Currying 不应该比您可能已经看到的增加任何额外的复杂性。通常，策略形式类似于e1 e2 ... en，您可以将其视为(((e1 e2) e3) ... en)。然后，您将减少 e1 e2，这应该会产生一个 lambda，然后您将其评估应用于 e3 等等。

我会让你弄清楚第二个作为练习。