【问题标题】:What is Weak Head Normal Form?什么是弱头范式?
【发布时间】:2011-10-15 22:03:08
【问题描述】:

弱头范式 (WHNF) 是什么意思? Head Normal form (HNF) 和 Normal Form (NF) 是什么意思?

Real World Haskell 状态:

熟悉的 seq 函数将表达式计算为我们所说的 head 范式(缩写为 HNF)。到达最外层后停止 构造函数(“头”)。这与范式 (NF) 不同,在 哪个表达式被完全评估。

你还会听到 Haskell 程序员提到弱头范式 (WHNF)。对于普通数据,弱头范式与头相同 正常形式。差异只出现在功能上,也是 深奥在这里关注我们。

我已经阅读了一些资源和定义(Haskell WikiHaskell Mail ListFree Dictionary),但我不明白。有人可以举个例子或提供一个外行定义吗?

我猜它会类似于:

WHNF = thunk : thunk

HNF = 0 : thunk 

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

seq($!) 与 WHNF 和 HNF 有什么关系?

更新

我还是一头雾水。我知道一些答案说忽略 HNF。从阅读各种定义来看,WHNF 和 HNF 中的常规数据似乎没有区别。但是,在功能方面似乎确实存在差异。如果没有区别,为什么foldl' 需要seq

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

常见的新手栈溢出代码:

myAverage = uncurry (/) . foldl' (\(acc, len) x -> (acc+x, len+1)) (0,0)

了解seq和weak head normal form (whnf)的人可以 立即明白这里出了什么问题。 (acc+x, len+1) 已经是 在 whnf 中,seq 将值减少到 whnf,对此没有任何作用。 此代码将像原始 foldl 示例一样构建 thunk, 他们只会在一个元组内。解决办法就是强制 元组的组成部分,例如

myAverage = uncurry (/) . foldl' 
          (\(acc, len) x -> acc `seq` len `seq` (acc+x, len+1)) (0,0)

-Haskell Wiki on Stackoverflow

【问题讨论】:

  • 一般我们说的是WHNF和RNF。 (RNF就是你所说的NF)
  • @monadic RNF 中的 R 代表什么?
  • @dave4420:减少
  • 现在WFH也很重要。

标签: haskell definition strictness weak-head-normal-form


【解决方案1】:

我会尽量用简单的术语来解释。正如其他人所指出的,head normal form不适用于Haskell,所以我不会在这里考虑。

正规形式

正常形式的表达式被完全评估,并且不能进一步评估子表达式(即它不包含未评估的 thunk)。

这些表达式都是正常形式的:

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

弱头范式

弱头范式的表达式已被评估为最外层的数据构造函数或 lambda 抽象(head)。子表达式可能已经被评估,也可能没有被评估。因此,每个范式表达式也是弱头范式,虽然反之一般不成立。

要判断一个表达式是否是弱头范式,我们只需要查看表达式的最外层部分。如果它是数据构造函数或 lambda,它是弱头范式。如果是函数式应用,则不是。

这些表达式是弱头范式:

(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 不提前减少内部表达式?那是因为 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。在下面的示例中,累加器是一个元组,因此它只会强制评估元组构造函数,而不是 acclen

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.

为避免这种情况,我们必须使评估元组构造函数强制评估acclen。我们通过使用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.

【讨论】:

  • 头范式要求 lambda 的主体也被缩减,而弱头范式没有这个要求。所以\x -> 1 + 1 是 WHNF 而不是 HNF。
  • 维基百科指出 HNF 是“如果头部位置没有 beta-redex,[a] 术语处于头部正常形式”。 Haskell 是否“弱”是因为它没有 beta-redex 子表达式?
  • 严格的数据构造函数是如何发挥作用的?他们只是喜欢在他们的论点上调用seq吗?
  • @CaptainObvious:1 + 2 既不是 NF 也不是 WHNF。表达式并不总是正常的形式。
  • @Zorobay:为了打印结果,GHCi 最终将表达式完全评估为 NF,而不仅仅是 WHNF。区分这两种变体的一种方法是使用:set +s 启用内存统计信息。然后你可以看到foldl' f ends up allocating more thunks than foldl' f'
【解决方案2】:

Haskell Wikibooks description of laziness 中关于 Thunks and Weak Head Normal Form 的部分提供了对 WHNF 的非常好的描述以及这个有用的描述:

逐步评估值 (4, [1, 2])。第一阶段是 完全未评估;所有后续形式都在 WHNF 中,最后一个 一个也是正常形式。

【讨论】:

  • 我知道人们说要忽略头部范式,但是你能在那个图中举一个例子,你知道头部范式是什么样的吗?
【解决方案3】:

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

要计算表达式,请将所有函数应用程序替换为其定义。执行此操作的顺序无关紧要,但仍然很重要:从最外面的应用程序开始,从左到右进行;这称为惰性求值

例子:

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

当没有更多功能应用程序可供替换时,评估停止。结果是范式(或简化范式,RNF)。无论您以何种顺序计算表达式,最终都会得到相同的范式(但仅当计算终止时)。

惰性求值的描述略有不同。也就是说,它说您应该仅将所有内容评估为 weak head normal form。 WHNF 中的表达式恰好有三种情况:

  • 构造函数:constructor expression_1 expression_2 ...
  • 参数太少的内置函数,如(+) 2sqrt
  • 一个 lambda 表达式:\x -> expression

换句话说,表达式的头部(即最外层的函数应用程序)无法进一步计算,但函数参数可能包含未计算的表达式。

WHNF 示例:

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

注意事项

  1. WHNF 中的“头”不是指列表的头,而是指最外层的函数应用程序。
  2. 有时,人们将未计算的表达式称为“thunk”,但我认为这不是理解它的好方法。
  3. Head normal form (HNF) 与 Haskell 无关。它与 WHNF 的不同之处在于 lambda 表达式的主体也在一定程度上被计算。

【讨论】:

  • foldl' 中使用seq 是否会强制评估从WHNF 到HNF?
  • @snmcdonald:不,Haskell 不使用 HNF。评估 seq expr1 expr2 会将第一个表达式 expr1 评估为 WHNF,然后再评估第二个表达式 expr2
【解决方案4】:

http://foldoc.org/Weak+Head+Normal+Form 给出了一个很好的示例解释,头部范式甚至简化了函数抽象内部的表达式位,而“弱”头部范式在函数抽象处停止。

如果你有的话,来自源代码:

\ x -> ((\ y -> y+x) 2)

那是弱头范式,但不是头范式......因为可能的应用程序卡在一个无法评估的函数内部。

实际的头部范式很难有效地实现。它需要在函数内部四处寻找。所以弱头范式的优点是你仍然可以将函数实现为不透明类型,因此它更兼容编译语言和优化。

【讨论】:

    【解决方案5】:

    WHNF 不希望评估 lambda 的主体,所以

    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
    

    【讨论】:

    • 或者我理解错误的例子,或者你在WHNF和HNF中混合了1和2。
    【解决方案6】:

    基本上,假设您有某种 thunk,t

    现在,如果我们想将 t 评估为 WHNF 或 NHF,除了函数之外它们是相同的,我们会发现我们会得到类似的结果

    t1 : t2 其中t1t2 是thunk。在这种情况下,t1 将是您的 0(或者更确切地说,是对 0 的 thunk,因为没有额外的拆箱)

    seq$! 评估 WHNF。请注意

    f $! x = seq x (f x)
    

    【讨论】:

    • @snmcdonald 忽略 HNF。 seq 表示当 this 被评估为 WHNF 时,将第一个参数评估为 WHNF。
    【解决方案7】:

    在图约简的实现中,对 HNF 的惰性求值迫使您处理 lambda 演算的名称捕获问题,而对 WHNF 的惰性求值可以避免它。

    Simon Peyton Jones 在Chapter 11 of The Implementation of Functional Programming Languages 中对此进行了解释。

    【讨论】:

      【解决方案8】:

      我意识到这是一个老问题,但这是 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 是任意项。

      • 如果它是任何术语 e 的 lambda 术语 λ x. e 或者它的形式,则该术语在 WHNF 中

        x e1 e2 ... em
        

        其中x 是一个变量,e1, e2, ..., em 是任意项。


      现在考虑一种编程语言,其构造函数 a,b,c... 的arity na, nb, nc...,这意味着只要t1, t2, ..., tm 在NF 中,那么术语a t1 t2 ... tm其中m = na 是一个redex,可以进行评估。例如,Haskell 中的加法构造函数 + 具有 2,因为它只有在给定两个正常形式的参数(在这种情况下是整数,它们本身可以被视为空值)时才评估构造函数)。

      • 如果一个词具有以下形式,则它属于 NF

        λ x1. λ x2. ... λ xn. (x t1 t2 ... tm)
        

        其中xnm < n 的变量或构造函数,t1, t2, ..., tm 在 NF 中。

      • 一个术语在 HNF 中,如果它具有以下形式

        λ x1. λ x2. ... λ xn. (x e1 e2 ... em)
        

        其中x 是变量或arity n 的构造函数,而e1, e2, ... em 是任意项只要第一个n 参数不是全部 NF.

      • 如果它是任何术语 e 的 lambda 术语 λ x. e 或它的形式,则该术语在 WHNF 中

        x e1 e2 ... em
        

        其中x 是变量或arity n 的构造函数,而e1, e2, ... em 是任意项只要第一个n 参数不是全部 NF.


      特别是,NF 中的任何术语都属于 HNF,HNF 中的任何术语都属于 WHNF,但反之则不然。

      【讨论】:

      • 为什么要求第一个n 参数不能全部在NF 中?
      • @dfeuer 以+为例,有二元数,那么(+ 2 3)的WHNF是5,因为23在NF中,但是@987654363的WHNF @ 是 (+ 2 (+ 2 1)),因为 (+ 2 1) 不在 NF 中。如果构造函数cn)的第一个n 参数e_1 ... e_n 在NF 中,那么(c e_1 ... e_n) 可能是一个约简,如+ 的情况。我应该指出,构造函数是指具有归约规则的构造函数。
      • 在我看来,您似乎不了解 WHNF 的定义。 Tomek Dobrzynski 的回答在this text 的第 11 章中指出了这一点。 (+ 2 (+ 2 1)) 不在 WHNF 中,因为它是一个完全应用的非构造函数(+ 的元数为 2,并应用于 2 个参数)。
      • @dfeuer 请查看正文第 10 页了解 redex 的定义。 (+ 2 (+ 2 1)) 不是 redex。
      • 我明白你在说什么,但我怀疑他们是否打算将第 10 页上的定义适用于此。惰性图缩减的整个想法是将表达式缩减为 WHNF,因为它们要么是 1. lambda 表达式,2. 部分应用程序,要么 3. 完全应用的数据构造函数。图形缩减引擎不会来到(+ 2 (+ 2 1)) 并且只是扔掉它的手。 (续)
      【解决方案9】:

      头部正常形式意味着没有头部还原

      (λx.((λy.y+x)b))b

      归结为:R,代表 redex(是的,里面还有另一个 redex,但这无关紧要)。这是一个 head redex,因为它是最左边的 redex(唯一的 redex),并且在它之前没有 lambda 项(变量或 lambda 表达式(应用程序或抽象)),只有 0 到 n 个抽象器(如果 R 是 redex (λx.A)B R 的抽象器是λx),在本例中为 0。

      因为有一个 head redex,它不在 HNF 中,因此它也不在 NF 中,因为有一个 redex。

      WHNF 表示它是 lambda 抽象或在 HNF 中。以上不在 HNF 中,也不是 lambda 抽象,而是一个应用程序,因此不在 WHNF 中。

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

      这是一个 lambda 抽象,但不是在 HNF 中,因为有一个头部 λx.Rb

      减少到λx.((b+x)b)。没有 redex,因此它是正常形式。

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

      所有 NF 都在 HNF 和 WHNF 中。所有 HNF 都是 WHNF。

      【讨论】:

        猜你喜欢
        • 1970-01-01
        • 1970-01-01
        • 2020-05-20
        • 1970-01-01
        • 2015-09-03
        • 1970-01-01
        • 1970-01-01
        • 2014-08-18
        • 2015-04-25
        相关资源
        最近更新 更多