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可被用于模式匹配，而1和createInfiniteNumbers (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
GHCi :sprint has odd/unhelpful behavior for values defined within the REPL
