lambda-calculus - 如何转换为 lambda 语法？

Question

我试图理解的问题的一部分涉及到:

twice (twice) f x , where twice == lambda f x . f (f x)

我试图理解如何进行这种替换，以及它的含义。

我的理解是(lambda x y . x + y) 2 3 == 2 + 3 == 5。我不明白twice(两次)是什么意思，或者f ( f x )。

Answer 1

看待这个问题的两种方式。

β-还原的机械应用

您可以通过展开两次 F X形式的任何子项来机械地解决这个问题 - 使用这个项，您最终将消除所有两次出现的情况，尽管您需要注意自己真正理解了lambda 演算的语法树以避免错误。

twice 采用两个参数，因此您的表达式 twice (twice) f x 是应用于 的 redex twice (twice) f x。 (redex 是一个子项，您可以独立于该项的其余部分来减少它)。

在 redex 中扩展 twice 的定义:twice (twice) f x -> Double (twice f)。

将其代入原始术语中，得到twice (twice f) x，这是另一个我们可以展开twice来得到twice f (twice f x)(注意此步骤中的括号)。

我们有两个twice redexes，我们可以在这里展开，展开括号内的那个要简单一些，给出twice f (f (f x))，这又可以展开为 f (f (f (f x)))。

通过抽象实现两次语义

通过调用高阶组合器(用于函数组合的“○”中缀组合器)，您可以更直观地了解发生的情况:

f ○ g = lambda x. f (g x)

很容易验证twice f x和(f ○ f) x都扩展为相同的范式，即f (f x), 所以通过外延性，我们有

twice f = f ○ f

使用它，我们可以非常直接地进行扩展，首先消除两次以支持组合组合器:

twice (twice) f x
= (twice ○ twice)  f x
= (twice (twice f)) x         /* expand out '○' */
= (twice (f ○ f)) x
= ((f ○ f) ○ (f ○ f)) x

然后展开“○”:

= (f ○ f) ((f ○ f) x)
= (f ○ f) (f (f x))
= (f (f (f (f x))))

这是更多的扩展步骤，因为我们首先扩展到包含“○”运算符的术语，然后将这些运算符扩展出来，但这些步骤更简单、更直观，您不太可能误解自己在做什么。 '○' 在 Haskell 中被广泛使用，是标准运算符，非常值得习惯。