什么是λ-微积分本质上？

Question

我有一个关于λ微积分的哲学问题。

当你探索λ微积分时，你会惊讶地看到你能在那里做的所有事情。你可以定义整数，算术运算，布尔，如果-然后-否则的语句，循环，递归函数，等等。我相信它已经被证明是计算完全的。

但是另一方面，如果您考虑了如何使用λ微积分中的函数，您就会意识到，您唯一能做的就是给它提供一个函数，然后它会返回另一个函数。这个过程永远不会结束。

那么，如何从计算中提取结果呢？

假设表达式的结果是函数f。您需要检查f是否如您所期望的那样。您可以测试它，接受您知道的函数，将f应用于它并接收g。但是要检查g是正确的，现在您需要验证g做了什么。然后你重新开始。那么，你怎么知道关于f的任何事情呢？

在我看来，您可以用一个单独的函数(恒等函数I = λx.x )代替λ-演算中的所有函数，而且所有的功能仍然像λ-演算中所描述的那样工作。教会数字3当被赋予f和x时返回f(f(f(x)))。但是由于f和x只能是I，所以它返回I。I应用于I，I也返回I。因此，I满足3的定义。“booleans”(λxy.x)和(λxy.y)需要两个参数，它们将是I和I，因此两个布尔人都将返回I。每一种行为都等同于身份，尽管它们的行为完全按照它们的定义。

那你是怎么做的呢？如何证明λ-微积分处理的不仅仅是一个函数？

是否有身份的概念？你能在没有评估的情况下立即识别一个函数吗？我相信已经证明，没有方法来测试两个函数的平等。

或者λ-微积分不是关于函数，而是关于它们所做的正式描述吗？这意味着λ表达式不仅定义了函数的作用，还定义了函数操作的数据。因此，在编写A B时，不将A应用于B，而是将字符串A描述的函数应用于包含在B中的函数的正式定义，返回另一个正式定义。

λ微积分到底是怎么回事？它所处理的数学对象是什么？

后续行动：

好的，从下面的答案看来，λ-微积分不是关于数学意义上的函数，而是关于可以用λ表达式表示的函数子集。或者更多关于λ高速公路的操作。

Answer 1

要确定lambda演算项的语义等价确实是不可能的。这是Rice定理的一个应用。然而，在语法上比较术语很容易，也就是说，测试它们是否具有完全相同的结构(等价地，如果它们的“字符串表示”是相同的)。你只需要这么做就可以得到结果了。

例如，要计算函数n = f(i)从自然值到自然值，您可以将i的教堂编码作为lambda演算函数的参数，应用约简规则直到停止，并检查结果项。如果它与教会数字的结构相匹配，则提取它编码的数字n。这就是你的结果。如果得到的术语看起来不像教会数字，或者表示没有停止，则函数在i中是未定义的。

术语有效地拉动双重职责，如“代码”和“数据”。这没什么特别的:图灵机的磁带(字母表上的字符串)可以--而且经常被解释为图灵机器的编码，或者它的某些方面。同样，von机器的主内存中的位可以是程序的编码，也可以是其他东西的编码。甚至同时兼而有之。唯一不同的是“默认透视图”。