我知道这是一个老问题，但这里有一个明确的WHNF, HNF和NF的数学定义。在纯lambda演算中:

如果一个项的形式是这样的，那么它就是NF λx1。λ x2. ...λ xn. (x t1 t2…tm) 其中x是一个变量，t1, t2，…， tm在NF中。 一个术语是HNF，如果它的形式是 λx1。λ x2. ...λ xn. (x e1 e2…em) 其中x是一个变量，e1, e2，…， em是任意的术语。 在WHNF中，如果一个项是任意项e的λ项xe，或者它是这样的形式 X e1 e2…新兴市场 其中x是一个变量，e1, e2，…， em是任意的术语。

---

现在考虑一种具有构造函数a,b,c…集合na, nb, nc…，这意味着无论何时t1, t2，…， tm在NF中，那么术语a t1 t2…Tm，其中m = na是一个redex，可以计算。例如，Haskell中的加法构造函数+具有arity 2，因为它只在给出两个标准形式的参数时才计算值(在本例中，整数本身可以被视为null构造函数)。

A term is in NF if it is of the form λ x1. λ x2. ... λ xn. (x t1 t2 ... tm) where x is either a variable or a constructor of arity n with m < n, and t1, t2, ..., tm are in NF. A term is in HNF if it is of the form λ x1. λ x2. ... λ xn. (x e1 e2 ... em) where x is either a variable or a constructor of arity n, and e1, e2, ... em are arbitrary terms so long as the first n arguments are not all in NF. A term is in WHNF if it is either a lambda term λ x. e for any term e or if it is of the form x e1 e2 ... em where x is either a variable or a constructor of arity n, and e1, e2, ... em are arbitrary terms so long as the first n arguments are not all in NF.

---

特别地，NF中的任何项都在HNF中，HNF中的任何项都在WHNF中，但不是相反的。

Haskell程序是表达式，它们通过执行求值来运行。

要计算表达式，请将所有函数应用程序替换为它们的定义。这样做的顺序并不重要，但仍然很重要:从最外层的应用程序开始，从左到右;这被称为惰性求值。

例子:

   take 1 (1:2:3:[])
=> { apply take }
   1 : take (1-1) (2:3:[])
=> { apply (-)  }
   1 : take 0 (2:3:[])
=> { apply take }
   1 : []

当没有剩余的功能应用程序需要替换时，计算就会停止。结果是标准形式(或简化标准形式，RNF)。无论以何种顺序求值表达式，最终都会得到相同的标准形式(但只有在求值结束时)。

对于惰性求值的描述略有不同。也就是说，你应该只计算弱头范式。表达式在WHNF中有三种情况:

构造函数:构造函数expression_1 expression_2… 内置函数的参数太少，比如(+)2或平方根 一个lambda表达式:\x ->表达式

换句话说，表达式的头(即最外层的函数应用程序)不能再求值，但函数参数可以包含未求值的表达式。

WHNF的例子:

3 : take 2 [2,3,4]   -- outermost function is a constructor (:)
(3+1) : [4..]        -- ditto
\x -> 4+5            -- lambda expression

---

笔记

WHNF中的“头”不是指列表的头，而是指最外层的函数应用程序。 有时，人们称未求值的表达式为“thunk”，但我不认为这是理解它的好方法。 头部标准型(HNF)与Haskell无关。它与WHNF的不同之处在于，lambda表达式的主体也在某种程度上被求值。

WHNF不希望对lambdas的主体进行计算，因此

WHNF = \a -> thunk
HNF = \a -> a + c

seq希望它的第一个参数在WHNF中，因此

let a = \b c d e -> (\f -> b + c + d + e + f) b
    b = a 2
in seq b (b 5)

计算结果为

\d e -> (\f -> 2 + 5 + d + e + f) 2

而不是，什么会使用HNF

\d e -> 2 + 5 + d + e + 2

头部正常形式意味着没有头部redex

(λx (y(λ。y + x) b)) b

简化为:R，代表redex(是的，它里面还有另一个redex，但这是不相关的)。这是一个头部redex，因为它是最左边的redex(唯一的redex)，在它之前没有lambda项(变量或lambda表达式(应用或抽象))，只有0到n个抽象者(如果R是一个redex (λx. a)B, R的抽象者是λx)，在这种情况下是0。

因为有一个头部索引，它不在HNF中，因此也不在NF中，因为有一个索引。

WHNF意味着它是一个lambda抽象或在HNF中。上述内容不在HNF中，也不是lambda抽象，而是一个应用程序，因此不在WHNF中。

λx.((λy.y+x)b)b在WHNF中

它是λ抽象，但不是在HNF中因为有一个头部λx。Rb

还原到λx.((b+x)b)。没有redex，所以是正常形式。

考虑λx.(λy.zyx)b)，化简为λx。R，所以不在HNF中。λx.(k(λy.zyx)b)化简为λx。因此它是在HNF中，而不是在NF中。

所有的NF均为HNF和WHNF。所有HNF均为WHNF。

Haskell Wikibooks对懒惰的描述中关于坦克和弱头正常形式的部分提供了对WHNF的非常好的描述，以及以下有用的描述:

逐步计算值(4，[1,2])。第一阶段是 完全未鉴定的;所有随后的形式都在WHNF中，而最后 一个也是正形式。

我试着用简单的语言解释一下。正如其他人指出的那样，head范式并不适用于Haskell，所以我在这里不考虑它。

标准形式

正常形式的表达式被完全求值，没有子表达式可以被进一步求值(即它不包含未求值的符号)。

这些表达式都是标准形式:

42
(2, "hello")
\x -> (x + 1)

这些表达式不是正常形式:

1 + 2                 -- we could evaluate this to 3
(\x -> x + 1) 2       -- we could apply the function
"he" ++ "llo"         -- we could apply the (++)
(1 + 1, 2 + 2)        -- we could evaluate 1 + 1 and 2 + 2

弱头正常型

弱head标准形式的表达式已经被求值到最外层的数据构造函数或lambda抽象(head)。子表达式可以求值，也可以不求值。因此，每个正规形式的表达式也是弱头正规形式，尽管相反的情况并不普遍。

要确定表达式是否为弱头正规形式，我们只需查看表达式的最外层。如果它是一个数据构造函数或，它是弱头正规形式。如果是函数应用，就不是。

这些表达式是弱头范式:

(1 + 1, 2 + 2)       -- the outermost part is the data constructor (,)
\x -> 2 + 2          -- the outermost part is a lambda abstraction
'h' : ("e" ++ "llo") -- the outermost part is the data constructor (:)

如上所述，上面列出的所有正规形式表达式也是弱头正规形式。

这些表达式不是弱头正规形式:

1 + 2                -- the outermost part here is an application of (+)
(\x -> x + 1) 2      -- the outermost part is an application of (\x -> x + 1)
"he" ++ "llo"        -- the outermost part is an application of (++)

堆叠溢位

将一个表达式求为弱头标准式可能需要先将其他表达式求为WHNF。例如，要计算1 +(2 + 3)到WHNF，我们首先必须计算2 + 3。如果对单个表达式求值会导致太多这样的嵌套求值，则会导致堆栈溢出。

当您构建一个大型表达式时，该表达式直到对其中的大部分进行了计算才会产生任何数据构造函数或lambda，就会发生这种情况。这通常是由foldl的这种用法引起的:

foldl (+) 0 [1, 2, 3, 4, 5, 6]
 = foldl (+) (0 + 1) [2, 3, 4, 5, 6]
 = foldl (+) ((0 + 1) + 2) [3, 4, 5, 6]
 = foldl (+) (((0 + 1) + 2) + 3) [4, 5, 6]
 = foldl (+) ((((0 + 1) + 2) + 3) + 4) [5, 6]
 = foldl (+) (((((0 + 1) + 2) + 3) + 4) + 5) [6]
 = foldl (+) ((((((0 + 1) + 2) + 3) + 4) + 5) + 6) []
 = (((((0 + 1) + 2) + 3) + 4) + 5) + 6
 = ((((1 + 2) + 3) + 4) + 5) + 6
 = (((3 + 3) + 4) + 5) + 6
 = ((6 + 4) + 5) + 6
 = (10 + 5) + 6
 = 15 + 6
 = 21

请注意，在将表达式转换为弱头部正常形式之前，它必须走得相当深。

你可能会想，为什么Haskell不提前减少内心的表达?那是因为哈斯克尔的懒惰。由于不能一般地假定每个子表达式都需要，所以表达式是由外向内求值的。

(GHC有一个严格性分析器，它可以检测到总是需要子表达式的某些情况，然后它可以提前计算它。然而，这只是一个优化，您不应该依赖它来避免溢出)。

另一方面，这种表达是完全安全的:

data List a = Cons a (List a) | Nil
foldr Cons Nil [1, 2, 3, 4, 5, 6]
 = Cons 1 (foldr Cons Nil [2, 3, 4, 5, 6])  -- Cons is a constructor, stop. 

为了避免在知道必须对所有子表达式求值时构建这些大表达式，我们希望强制提前对内部部分求值。

seq

Seq是一个特殊的函数，用于强制表达式求值。它的语义是，seq x y意味着每当y被求为弱头标准形式时，x也被求为弱头标准形式。

它是用于foldl'定义的其他地方，foldl的严格变体。

foldl' f a []     = a
foldl' f a (x:xs) = let a' = f a x in a' `seq` foldl' f a' xs

每次迭代foldl'迫使累加器到WHNF。因此，它可以避免构建一个大表达式，从而避免堆栈溢出。

foldl' (+) 0 [1, 2, 3, 4, 5, 6]
 = foldl' (+) 1 [2, 3, 4, 5, 6]
 = foldl' (+) 3 [3, 4, 5, 6]
 = foldl' (+) 6 [4, 5, 6]
 = foldl' (+) 10 [5, 6]
 = foldl' (+) 15 [6]
 = foldl' (+) 21 []
 = 21                           -- 21 is a data constructor, stop.

但正如HaskellWiki上的例子所提到的，这并不是在所有情况下都可以节省您的时间，因为累加器只计算到WHNF。在下面的例子中，累加器是一个元组，因此它只强制求元组构造函数的值，而不是acc或len。

f (acc, len) x = (acc + x, len + 1)

foldl' f (0, 0) [1, 2, 3]
 = foldl' f (0 + 1, 0 + 1) [2, 3]
 = foldl' f ((0 + 1) + 2, (0 + 1) + 1) [3]
 = foldl' f (((0 + 1) + 2) + 3, ((0 + 1) + 1) + 1) []
 = (((0 + 1) + 2) + 3, ((0 + 1) + 1) + 1)  -- tuple constructor, stop.

为了避免这种情况，必须在求元组构造函数值时强制求acc和len值。我们通过使用seq来做到这一点。

f' (acc, len) x = let acc' = acc + x
                      len' = len + 1
                  in  acc' `seq` len' `seq` (acc', len')

foldl' f' (0, 0) [1, 2, 3]
 = foldl' f' (1, 1) [2, 3]
 = foldl' f' (3, 2) [3]
 = foldl' f' (6, 3) []
 = (6, 3)                    -- tuple constructor, stop.