Lambda 演算需要解释

如何解决Lambda 演算需要解释

在 let 的 this 处理中，给出了 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 版本与 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)