haskell - Haskell 中的 beta 减少策略

Question

这是我第一次学习函数式编程。我确实了解简单的贝塔减少是如何工作的。

例如:

(\x->2*x)5

表示您将 xs 替换为 5。

2*5=10

但是，其他例子让我感到困惑

(\f->f(f 0))(\x->x+1)

我们已经了解了一些评估策略、头部范式和弱头部范式。

从我的笔记中，我了解到 head 范式意味着没有 redex 表达式，而弱 head 范式意味着存在 lambda 抽象。

这对我来说没有任何意义。两者之一适用于最后一个例子吗？如果是这样，其他策略的例子是什么？

Answer 1

术语

(\f -> f (f 0)) (\x -> x+1)

既不是头部正常形态，也不是弱头部正常形态。该项是 lambda(具体来说，\f -> f (f 0))对项(具体来说，\x -> x+1)的应用，所以:

1. 有一个 redex。回想一下，redex 被定义为 lambda 对项的应用。由于表达式中某处有一个 redex - 特别是在本例中的最顶层 - 这不是 head 正常形式。
2. 该术语的顶层是一个应用程序，而不是 lambda，因此这不是弱头范式。

“头部范式”和“弱头部范式”都不是评估策略。形式是描述术语的形容词；一般来说，评估策略是描述如何将一个术语更改为另一个术语的动词。