1. 形式系統(tǒng)（Formal system）
在邏輯學(xué)與數(shù)學(xué)中，一個(gè)形式系統(tǒng)由兩部分組成，一個(gè)形式語(yǔ)言加上一套推理規(guī)則。
一個(gè)形式系統(tǒng)也許是純粹抽象地制定出來(lái)的，只是為了研究其自身。
也可能是為了描述真實(shí)現(xiàn)象或客觀事實(shí)而設(shè)計(jì)的。
2. λ演算（λ-caculus）
λ演算用于研究函數(shù)定義、函數(shù)應(yīng)用和遞歸，它是一些形式系統(tǒng)的總稱(chēng)，
配備不同的推理規(guī)則集，就會(huì)得到不同的演算系統(tǒng)。
λ演算由Alonzo Church和Stephen Cole Kleene在20世紀(jì)三十年代引入，
Church在1936年證明了，兩個(gè)λ表達(dá)式是否等價(jià)的問(wèn)題，是不可判定的。
這是第一個(gè)被證明的不可判定問(wèn)題，甚至早于停機(jī)問(wèn)題。
λ演算對(duì)函數(shù)式編程有巨大的影響。
1.1 λ項(xiàng)（λ-terms）
采用BNF，λ項(xiàng)的文法可以描述如下，
M ::= x | MM | λx.M
注：為行文簡(jiǎn)便，這里省略了(和)。
它表明，合法的表達(dá)式，要么是一個(gè)變量：x，
要么是一個(gè)函數(shù)調(diào)用（application）：MM，
要么是一個(gè)函數(shù)抽象（lambda abstraction）：λx.M。
例如：這些表達(dá)式是合法的，x，(λx.x)5，λx.y。
1.2 α轉(zhuǎn)換（α-conversion）
α轉(zhuǎn)換是一種推理規(guī)則，它基于以下事實(shí)，
函數(shù)的形參只是占位符，替換形參和函數(shù)體中相應(yīng)的符號(hào)，所產(chǎn)生的新表達(dá)式與原表達(dá)式等價(jià)。
例如，經(jīng)過(guò)α轉(zhuǎn)換之后，
λxy.x(xy) ≡ λuv.u(uv)
易見(jiàn)，α轉(zhuǎn)換是一個(gè)等價(jià)關(guān)系（自反的，對(duì)稱(chēng)的，傳遞的）。
1.3 β歸約（β-reduction）
函數(shù)調(diào)用表達(dá)式，可以化簡(jiǎn)，結(jié)果為函數(shù)體中的形參替換成實(shí)參后的表達(dá)式。
例如，(λx.x(xy))N可以一步β歸約為N(Ny)，
(λx.(λy.yx)z)v可以兩步β歸約為zv，
而(λx.xx)(λx.xx)可以無(wú)限制的進(jìn)行β歸約。
通常我們把一步或者多步β歸約，簡(jiǎn)稱(chēng)為β歸約。
如果某一λ項(xiàng)不可再進(jìn)行β歸約，就稱(chēng)該項(xiàng)為β范式（β-normal form）。
如果某一λ項(xiàng)可以β歸約為兩個(gè)不同的項(xiàng)，
那么，這兩項(xiàng)必定可以再β歸約為同一項(xiàng)，這種性質(zhì)稱(chēng)為匯聚性（confluence）。
2. 惰性求值
大多數(shù)編程語(yǔ)言采用的策略是嚴(yán)格求值（strict evaluation），
即，求值子表達(dá)式總是在復(fù)合表達(dá)式之前進(jìn)行，
或者說(shuō)，在進(jìn)入函數(shù)體之前，實(shí)參需要先求值。
例如：
head [3+2, 7*5] => head [5, 35] => 5
如果采用了這種求值策略，列表的長(zhǎng)度就必須是有限的，
調(diào)用函數(shù)head之前，必須先確定列表中的每一個(gè)元素。
Haskell的實(shí)現(xiàn)ghc，并沒(méi)有采用這種求值策略，它希望求值一個(gè)表達(dá)式越晚越好。
在這個(gè)例子中，ghc并不會(huì)先確定列表元素的值，
而是直接調(diào)用head，得到一個(gè)尚未被求值的列表元素3+2。
而后，因?yàn)槲覀円谄聊簧巷@示結(jié)果，所以迫使3+2必須被求值，顯示為5，
這種求值方式，被稱(chēng)為惰性求值（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
現(xiàn)在我們來(lái)計(jì)算myHead infiniteNumbers。
『希望求值一個(gè)表達(dá)式越晚越好』并不是一件簡(jiǎn)單的事情，
因?yàn)榧词?code>infiniteNumbers不事先求值，在帶入myHead之后，還是不得不求值它，
仍然會(huì)導(dǎo)致createInfiniteNumbers無(wú)限遞歸。
其實(shí)，ghc在求值表達(dá)式時(shí)，并不會(huì)一次性的求值到底，
而是每次只將一個(gè)表達(dá)式求值到它的WHNF（weak head normal form），
即，求值到最外層的值構(gòu)造器或者λ抽象為止。
值構(gòu)造器以及λ抽象內(nèi)部，就不會(huì)被求值了，
未被求值的部分用占位符來(lái)表示，稱(chēng)為thunk。
ghc會(huì)記錄多個(gè)相同thunk的不同引用，使得這些相同thunk只會(huì)被求值一次。
2.2 求值過(guò)程
myHead infiniteNumbers
我們來(lái)看上式的求值過(guò)程：
（1）myHead infiniteNumbers這個(gè)表達(dá)式是一個(gè)thunk，由于我們要在屏幕上顯示它的值，所以不得不求值它。
（2）我們需要將上述thunk求值為WHNF，于是，將infiniteNumbers保存為另外一個(gè)新的thunk，調(diào)用函數(shù)myHead。
（3）myHead會(huì)對(duì)參數(shù)進(jìn)行模式匹配，因此參數(shù)不得不被求值。
（4）infiniteNumbers求值會(huì)導(dǎo)致createInfiniteNumbers 1被求值。因?yàn)?，只需求值到WHNF，所以不會(huì)引起無(wú)限遞歸。
（5）結(jié)果為Prepend 1 (createInfiniteNumbers (1 + 1))，它是一個(gè)WHNF。其中，Prepend可被用于模式匹配，而1和createInfiniteNumbers (1 + 1)都是thunk。
（6）現(xiàn)在myHead就可以對(duì)參數(shù)進(jìn)行匹配了，myHead (Prepend x _) = x滿足匹配條件，x匹配到了1，于是myHead返回了1，注意1還是一個(gè)thunk。
（7）為了把1這個(gè)thunk顯示出來(lái)，繼續(xù)求值，結(jié)果為數(shù)字1。
注：
只有infiniteNumbers的值被需要的時(shí)候，才會(huì)調(diào)用createInfiniteNumbers 1，
也就是說(shuō)，thunk可以不是weak head normal form，
但是如果thunk被求值，其結(jié)果一定是weak head normal form。
因此，在這個(gè)例子中，調(diào)用myHead infiniteNumbers之前，
infiniteNumbers是未求值的，
即使是，它所對(duì)應(yīng)的createInfiniteNumbers 1不是一個(gè)weak head normal form。
2.4 seq
為了對(duì)求值進(jìn)行控制，ghc內(nèi)置了seq函數(shù)。
ghci> :t seq
ghci> seq :: a -> b -> b
它首先將第一個(gè)參數(shù)求值為WHNF，然后返回第二個(gè)參數(shù)。
例如：
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提供的功能，用于顯示表達(dá)式的結(jié)果，但不會(huì)對(duì)它求值。
3. 參考
形式系統(tǒng)
Lambda-Calculus and Combinators
Beginning Haskell
Parallel and Concurrent Programming in Haskell
:sprint for polymorphic values
GHCi :sprint has odd/unhelpful behavior for values defined within the REPL
