Lambda Calculus Reduction / 评估表达式

Question

我正在阅读这些关于 lambda 演算的 notes，但我在开始减少/评估其中一个表达式时遇到了一些麻烦。

特别是功能 (λf.λx.f(f(x)))(λy.y^2)(5).

我该如何开始呢？他说答案是 625。我的数学直觉告诉我们我们是这样进行的： (λf.λx.f(f(x)))(5^2) 并且他之前说过f(x)是地图

x |-> x^2

所以 f(f(x)) 是 f o f = (f)^2 = x^4

所以进一步减少我们得到的 lambda 表达式

(λf.λx.x^4))(5^2)

但是我们将 25 代入 x^4，得到 25*25*25*25 = 390,625。

(λf.(390,625))

那么当我们到达这里时，我完全不知道这个表达式代表什么？

我误解了 Lambda 演算的哪一部分？我减少表达式的方式正确吗？

Answer 1

我对 lambda 演算一无所知，所以如果我错了，请随意投反对票让我忘记 :) 再加上我的术语将被关闭，所以希望有经验的人能回答这个问题。无论如何，这可能应该发布到math.stackexchange.com。

前面是作为示例给出的，并不打算延续到后续问题。

首先，您似乎没有正确复制表达式。根据PDF，它是：

现在操作顺序很重要（括号在前！）。

我们从：

我们为左侧的 lambda 项 提供参数 。这意味着 f 被平方函数替换。

所以现在我们有：

编辑：

作为 的参数给出的原因是我们可以将整个表达式写成：

如果我们看第一部分，更容易看出 适用于第一个参数：

Answer 2

正确的正常顺序（最左边的）beta-reduction 到正常形式：

   (λ f. (λ x. f (f x))) (λ y. y ^ 2) 5
=  (λ x. (λ y. y ^ 2) ((λ y. y ^ 2) x)) 5
=  (λ x. ((λ y. y ^ 2) x) ^ 2) 5
=  (λ x. (x ^ 2) ^ 2) 5
=  (5 ^ 2) ^ 2
=  25 ^ 2
=  625

2、5 和 ^ 等数字原语虽然是 encodable，但不是语法的一部分。指数乘法等直观的传统代数归约规则不适用；只有 beta 和可能的 eta 减少。