Lambda微积分缩减

Question

我可以做简单的Lambda削减，然而，我不知道如何做那些获得“运行”。

以下是我所不明白的两个例子：

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

Answer 1

备注

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演算的一种可能性是给每个变量一个类型(非常类似于编程语言中的类型)。如果您想要将一个变量应用到另一个变量，则需要匹配这些类型。

例如，假设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演算，那么第一个方法可以简化为：

1. (( lambda x.)( lambda y.(j，y)(J)(M)-用x代替j
2. )(兰姆达。(j，y)m)-用y代替m
3. (j、m)
4. 从这里开始你被困住了..。

通常不存在将变量应用于变量的约简规则。这就是为什么我们使用类型系统，以确保对于任何类型良好的程序，当我们评估，我们永远不会“卡住”，就像我们在步骤3。

跑不应该增加任何额外的复杂性，你可能已经看到了。一般来说，策略是某种形式的e1 e2 ... en，您可以把它看作是(((e1 e2) e3) ... en)。然后，您将减少e1 e2，这应该会产生一个lambda，而不是应用于e3等等的评估。

我会让你把第二个作为练习。