Haskell 中的 Beta 减少策略

Question

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

例如：

(\x->2*x)5

意味着您将 xs 替换为 5。

2*5=10

然而，其他例子让我感到困惑

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

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

从我的笔记中，我明白头部范式意味着没有 redex 表达式，而弱头部范式意味着存在 lambda 抽象。

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

Answer 1

期限

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

既不是头部范式也不是弱头部范式。该术语是 lambda（特别是\f -> f (f 0)）对术语（特别是\x -> x+1）的应用，因此：

1. 有一个还原。回想一下，redex 被定义为将 lambda 应用于一个术语。由于表达式中的某处有一个 redex——特别是在最顶层，在这种情况下——这不是正常形式。
2. 该术语的顶级是应用程序，而不是 lambda，因此这不是弱头范式。

“头范式”和“弱头范式”都不是评估策略。形式是描述术语的形容词；评估策略通常是描述如何将一个术语变为另一个术语的动词。