需要解释 Lambda 演算答案

【问题标题】：Lambda Calculus let explanation needed需要解释 Lambda 演算
【发布时间】：2021-01-30 00:52:11
【问题描述】：

在this 对let 的处理中，给出了let 的lambda 演算版本

(\f.z)(\x.y)

用词

f由f x = y定义在表达式中z，然后为

let f x = y in z

我从初学者的角度知道 Haskell 的 let 是如何工作的，即定义遵循 let 和表达式（对这些定义做一些事情）遵循 in。

let <definitions> in <expression>

但是这个最一般的 lambda 演算描述令人费解。例如，我假设可能有 let f x = y in z 的 Haskell lambda 函数版本。有人可以在 Haskell 中写出这个——或许可以举一两个例子吗？只是猜测，似乎第一个 lambda 函数需要第二个 lambda 函数——不知何故？

(\x -> y)(\f -> z)

但这只是猜测。

【问题讨论】：

标签： haskell let lambda-calculus

【解决方案1】：

Haskell 版本与 lambda 演算版本完全相同，但使用的是 Haskell 语法：

(\f -> z) (\x -> y)

为什么？

let f x = y in z
    ^^^^^^^ "local" function called "f"

let f = (\x -> y) in z
    ^^^^^^^^^^^^^ same thing without the function syntax

我们只是引入了一个新变量f，它的值是(\x -> y)。

我们如何在 lambda 演算中引入变量？我们定义一个函数然后调用它，像这样：

(\x.zzzzzzzzzzzzzzzzzzz) 1
    ^^^^^^^^^^^^^^^^^^^ inside this part, x is 1

（lambda 演算没有数字，但你懂的）

所以我们只是引入了一个名为f 的变量，其值为(\x.y)

【讨论】：

所以f = (\x -> y) in z 我们可能有z 是f 1。 (\f -> z) (\x -> y) 的 Beta 减少（在 Haskell 中）将是 (\x -> y) z ？
@147pm 否。(\f -> z) 1 的 Beta 减少是 z，但所有免费的 fs 都替换为 1s。 (\f -> z) (\x -> y) 的 beta 减少是 z，但所有免费的 fs 都替换为 (\x -> y)。因此，如果z 中没有f，那么它只是z。如果z 代表f 42 "hello" 之类的东西，那么它就是(\x -> y) 42 "hello"
那么我们可以有(\f -> f 3)(\x -> x^2) ==> 9 和(\f -> f)(\x -> x^2) (3) ==> 9
请注意，在 Haskell 中，let 与其 lambda 编码之间的等价关系仅在 f 是单态的情况下才有效。事实上，let f = .. 可以为f 提供多态类型，而(\f -> ...)... 不能。这是由于类型推断的工作原理，我认为这种区别首先是由 Hindley-Milner 类型系统引入的。
@147pm (\f -> f 3)(\x -> x^2)的Beta减少是(\x -> x^2) 3，不是9，你必须减少更多的次数才能得到9。 Beta 减少两次给你3^2，然后评估得到 9