在逻辑学与数学中，一个形式系统由两部分组成，一个形式语言加上一套推理规则。
一个形式系统也许是纯粹抽象地制定出来的，只是为了研究其自身。也可能是为了描述真实现象或客观事实而设计的。
λ演算用于研究函数定义、函数应用和递归，它是一些形式系统的总称，配备不同的推理规则集，就会得到不同的演算系统。
λ演算由Alonzo Church和Stephen Cole Kleene在20世纪三十年代引入，Church在1936年证明了，两个λ表达式是否等价的问题，是不可判定的。这是第一个被证明的不可判定问题，甚至早于停机问题。
λ演算对函数式编程有巨大的影响。
采用BNF，λ项的文法可以描述如下，
M ::= x | MM | λx.M注：为行文简便，这里省略了(和)。
它表明，合法的表达式，要么是一个变量：x，要么是一个函数调用（application）：MM，要么是一个函数抽象（lambda abstraction）：λx.M。
例如：这些表达式是合法的，x，(λx.x)5，λx.y。
α转换是一种推理规则，它基于以下事实，函数的形参只是占位符，替换形参和函数体中相应的符号，所产生的新表达式与原表达式等价。
例如，经过α转换之后，
λxy.x(xy) ≡ λuv.u(uv)易见，α转换是一个等价关系（自反的，对称的，传递的）。
函数调用表达式，可以化简，结果为函数体中的形参替换成实参后的表达式。例如，(λx.x(xy))N可以一步β归约为N(Ny)，(λx.(λy.yx)z)v可以两步β归约为zv，而(λx.xx)(λx.xx)可以无限制的进行β归约。
通常我们把一步或者多步β归约，简称为β归约。如果某一λ项不可再进行β归约，就称该项为β范式（β-normal form）。
如果某一λ项可以β归约为两个不同的项，那么，这两项必定可以再β归约为同一项，这种性质称为汇聚性（confluence）。
大多数编程语言采用的策略是严格求值（strict evaluation），即，求值子表达式总是在复合表达式之前进行，或者说，在进入函数体之前，实参需要先求值。例如：
head [3+2, 7*5] => head [5, 35] => 5如果采用了这种求值策略，列表的长度就必须是有限的，调用函数head之前，必须先确定列表中的每一个元素。
Haskell的实现ghc，并没有采用这种求值策略，它希望求值一个表达式越晚越好。在这个例子中，ghc并不会先确定列表元素的值，而是直接调用head，得到一个尚未被求值的列表元素3+2。
而后，因为我们要在屏幕上显示结果，所以迫使3+2必须被求值，显示为5，这种求值方式，被称为惰性求值（lazy）。
现在我们来计算myHead infiniteNumbers。
『希望求值一个表达式越晚越好』并不是一件简单的事情，因为即使infiniteNumbers不事先求值，在带入myHead之后，还是不得不求值它，仍然会导致createInfiniteNumbers无限递归。
其实，ghc在求值表达式时，并不会一次性的求值到底，而是每次只将一个表达式求值到它的WHNF（weak head normal form），即，求值到最外层的值构造器或者λ抽象为止。
值构造器以及λ抽象内部，就不会被求值了，未被求值的部分用占位符来表示，称为thunk。ghc会记录多个相同thunk的不同引用，使得这些相同thunk只会被求值一次。
我们来看上式的求值过程：（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。
为了对求值进行控制，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提供的功能，用于显示表达式的结果，但不会对它求值。
形式系统Lambda-Calculus and CombinatorsBeginning HaskellParallel 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
相关资源：python入门教程(PDF版)