柯里化的前生今世(十三):WHNF

  1. 云栖社区>
  2. 博客>
  3. 正文

柯里化的前生今世(十三):WHNF

何幻 2016-10-28 17:51:04 浏览1468
展开阅读全文

1. 形式系统(Formal system)

在逻辑学与数学中,一个形式系统由两部分组成,一个形式语言加上一套推理规则

一个形式系统也许是纯粹抽象地制定出来的,只是为了研究其自身。
也可能是为了描述真实现象或客观事实而设计的。

2. λ演算(λ-caculus)

λ演算用于研究函数定义、函数应用和递归,它是一些形式系统的总称,
配备不同的推理规则集,就会得到不同的演算系统。

λ演算由Alonzo Church和Stephen Cole Kleene在20世纪三十年代引入,
Church在1936年证明了,两个λ表达式是否等价的问题,是不可判定的。
这是第一个被证明的不可判定问题,甚至早于停机问题

λ演算对函数式编程有巨大的影响。

1.1 λ项(λ-terms)

采用BNF,λ项的文法可以描述如下,

M ::= x | MM | λx.M

注:为行文简便,这里省略了()

它表明,合法的表达式,要么是一个变量:x
要么是一个函数调用(application):MM
要么是一个函数抽象(lambda abstraction):λx.M

例如:这些表达式是合法的,x(λx.x)5λx.y

1.2 α转换(α-conversion)

α转换是一种推理规则,它基于以下事实,
函数的形参只是占位符,替换形参和函数体中相应的符号,所产生的新表达式与原表达式等价。

例如,经过α转换之后,

λxy.x(xy) ≡ λuv.u(uv)

易见,α转换是一个等价关系(自反的,对称的,传递的)。

1.3 β归约(β-reduction)

函数调用表达式,可以化简,结果为函数体中的形参替换成实参后的表达式。
例如,(λx.x(xy))N可以一步β归约为N(Ny)
(λx.(λy.yx)z)v可以两步β归约为zv
(λx.xx)(λx.xx)可以无限制的进行β归约。

通常我们把一步或者多步β归约,简称为β归约。
如果某一λ项不可再进行β归约,就称该项为β范式(β-normal form)。

如果某一λ项可以β归约为两个不同的项,
那么,这两项必定可以再β归约为同一项,这种性质称为汇聚性(confluence)。

2. 惰性求值

大多数编程语言采用的策略是严格求值(strict evaluation),
即,求值子表达式总是在复合表达式之前进行,
或者说,在进入函数体之前,实参需要先求值。
例如:

head [3+2, 7*5] => head [5, 35] => 5

如果采用了这种求值策略,列表的长度就必须是有限的,
调用函数head之前,必须先确定列表中的每一个元素。

Haskell的实现ghc,并没有采用这种求值策略,它希望求值一个表达式越晚越好。
在这个例子中,ghc并不会先确定列表元素的值,
而是直接调用head,得到一个尚未被求值的列表元素3+2

而后,因为我们要在屏幕上显示结果,所以迫使3+2必须被求值,显示为5
这种求值方式,被称为惰性求值(lazy)。

2.1 WHNF(weak head normal form)

data MyList a = Empty | Prepend a (MyList a)
    deriving Show

infiniteNumbers :: MyList Int
infiniteNumbers = createInfiniteNumbers 1
    where
        createInfiniteNumbers n = Prepend n (createInfiniteNumbers (n + 1))

myHead :: MyList a -> a
myHead Empty = error "empty list"
myHead (Prepend x _) = x

现在我们来计算myHead infiniteNumbers

『希望求值一个表达式越晚越好』并不是一件简单的事情,
因为即使infiniteNumbers不事先求值,在带入myHead之后,还是不得不求值它,
仍然会导致createInfiniteNumbers无限递归。

其实,ghc在求值表达式时,并不会一次性的求值到底,
而是每次只将一个表达式求值到它的WHNF(weak head normal form),
即,求值到最外层的值构造器或者λ抽象为止。

值构造器以及λ抽象内部,就不会被求值了,
未被求值的部分用占位符来表示,称为thunk
ghc会记录多个相同thunk的不同引用,使得这些相同thunk只会被求值一次。

2.2 求值过程

myHead infiniteNumbers

我们来看上式的求值过程:
(1)myHead infiniteNumbers这个表达式是一个thunk,由于我们要在屏幕上显示它的值,所以不得不求值它。
(2)我们需要将上述thunk求值为WHNF,于是,将infiniteNumbers保存为另外一个新的thunk,调用函数myHead
(3)myHead会对参数进行模式匹配,因此参数不得不被求值。

(4)infiniteNumbers求值会导致createInfiniteNumbers 1被求值。因为,只需求值到WHNF,所以不会引起无限递归。
(5)结果为Prepend 1 (createInfiniteNumbers (1 + 1)),它是一个WHNF。其中,Prepend可被用于模式匹配,而1createInfiniteNumbers (1 + 1)都是thunk。
(6)现在myHead就可以对参数进行匹配了,myHead (Prepend x _) = x满足匹配条件,x匹配到了1,于是myHead返回了1,注意1还是一个thunk。

(7)为了把1这个thunk显示出来,继续求值,结果为数字1

注:
只有infiniteNumbers的值被需要的时候,才会调用createInfiniteNumbers 1
也就是说,thunk可以不是weak head normal form,
但是如果thunk被求值,其结果一定是weak head normal form。

因此,在这个例子中,调用myHead infiniteNumbers之前,
infiniteNumbers是未求值的,
即使是,它所对应的createInfiniteNumbers 1不是一个weak head normal form。

2.4 seq

为了对求值进行控制,ghc内置了seq函数。

ghci> :t seq
ghci> seq :: a -> b -> b

它首先将第一个参数求值为WHNF,然后返回第二个参数。
例如:

ghci> let x = 1 + 2 :: Int
ghci> let y = (x, x)

ghci> let u = 1 + 2 :: Int
ghci> let v= seq u (u, u)

ghci> let f (_, _) = 0
ghci> f y
ghci> f v

ghci> :sprint x
x= _

ghci> :sprint u
u = 3

注:
:sprint是ghci提供的功能,用于显示表达式的结果,但不会对它求值。

3. 参考

形式系统
Lambda-Calculus and Combinators
Beginning Haskell
Parallel and Concurrent Programming in Haskell
[:sprint for polymorphic values](http://stackoverflow.com/questions/21518584/sprint-for-polymorphic-values)
GHCi :sprint has odd/unhelpful behavior for values defined within the REPL

网友评论

登录后评论
0/500
评论
何幻
+ 关注