什么是弱头标准型(WHNF) ?Head Normal form (HNF)和Normal form (NF)是什么意思?

Real World Haskell声明:

我们熟悉的seq函数将表达式求值为 呼叫头标准型(简称HNF)。它一旦到达就会停止 最外层的构造函数(“head”)。这与正常情况不同 形式(NF),其中表达式被完全求值。 您还会听到Haskell程序员提到弱头正常 表单(WHNF)。对于正规数据,弱头正规形式与 头部正常形式。这种差异只出现在函数中,也是如此 这里涉及到我们的深奥。

我读了一些资源和定义(Haskell维基和Haskell邮件列表和免费字典),但我不明白。谁能举个例子或者给出一个外行的定义?

我猜它会类似于:

WHNF = thunk : thunk

HNF = 0 : thunk 

NF = 0 : 1 : 2 : 3 : []

seq和($!)如何与WHNF和HNF相关?

更新

我还是很困惑。我知道有些答案说忽略HNF。从各种定义来看,WHNF和HNF中的常规数据似乎没有区别。然而,当涉及到函数时,似乎确实有区别。如果没有区别,为什么seq是必要的foldl'?

另一个混淆点来自Haskell Wiki,它声明seq简化为WHNF,并且不会对下面的示例执行任何操作。然后他们说他们必须使用seq来强制求值。这不是强迫它去HNF吗?

Common newbie stack overflowing code: myAverage = uncurry (/) . foldl' (\(acc, len) x -> (acc+x, len+1)) (0,0) People who understand seq and weak head normal form (whnf) can immediately understand what goes wrong here. (acc+x, len+1) is already in whnf, so the seq (in the definition of foldl'), which reduces a value to whnf, does nothing to this. This code will build up thunks just like the original foldl example, they'll just be inside a tuple. The solution is just to force the components of the tuple, e.g. myAverage = uncurry (/) . foldl' (\(acc, len) x -> acc `seq` len `seq` (acc+x, len+1)) (0,0)

-Haskell Wiki在Stackoverflow上


当前回答

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表达式的主体也在某种程度上被求值。

其他回答

头部正常形式意味着没有头部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中,而最后 一个也是正形式。

我知道这是一个老问题,但这里有一个明确的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