Lambda演算需要解释

html5 • • 问答

在这种对letlambda 演算版本的处理let中给出

(f.z)(x.y)

用词

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

let f x = y in z

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

let <definitions> in <expression>

但是这种最一般的 lambda 演算描述令人困惑。例如，我假设可能有一个 Haskell lambda 函数版本的let f x = y in z. 有人可以在 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)

  • Note that in Haskell that equivalence between `let` and its lambda encoding only works when `f` is monomorphic. Indeed, `let f = ..` can give a polymorphic type to `f`, while `(f -> ...)...` does not. This is due to how type inference works, and this distinction I think was first introduced by the Hindley-Milner type system.
以上是Lambda演算需要解释的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>