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

Question

我试图理解的部分问题涉及以下内容：

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

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

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

score 2 · Accepted Answer

有两种看待这个的方式。

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

twice接受两个参数，因此您的表达式twice (twice) f x是twice (twice) f应用于x. （redex 是一个子项，您可以独立于该项的其余部分进行归约）。

展开twiceredex 中的定义：twice (twice) f x -> twice (twice f).

将其替换为原始术语 get ，这是我们可以扩展为 gettwice (twice f) x的另一个 redex （注意此步骤中的括号）。twicetwice f (twice f x)

我们有两个twice可以在这里展开的 redexes，展开括号内的那个稍微简单一些，giving twice f (f (f x))，它可以再次展开为 give f (f (f (f x)))。

您可以通过调用一个高阶组合器，即用于函数组合的“○”中缀组合器，以更直观的方式查看正在发生的事情：

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

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

twice f = f ○ f

使用它，我们可以非常直接地扩展，首先消除twice有利于组合组合器：

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 中广泛使用的标准运算符，非常值得习惯。

1 回答 1