λ演算需要解释

Question

对于let，给出了let的λ演算版本

(f.z)(x.y)

和

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

let f x = y in z

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

let <definitions> in <expression>

但是这个最一般的λ演算描述是令人困惑的。例如，我假设可能有一个Haskell lambda函数版本的let f x = y in z。有人能用Haskell写出来吗?或许还能举一两个例子?只是猜测，似乎第一个函数需要第二个函数——不知怎么的?

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

但这只是一个猜测。

Answer 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)。

如何在微积分中引入一个变量?我们定义一个函数，然后调用它，像这样:

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

(lambda演算没有数字，但你懂的)

我们引入一个名为f的变量它的值是(x.y)