域论模型
类型化lambda演算，有两个常用模型。
其一，域论模型。其二，递归函数论模型。
在众多域论模型中，
主要关心的是一种具有完全偏序（complete partial order）结构的域，简称CPO。
研究它的主要原因是，它是带有不动点算子的模型，
而且它还提供了一种解释递归类型表达式的方法。
域论方法是递归函数论模型的基础。
递归
加入递归之后，对表达式进行归约就可能会无限的进行下去，
因此将出现没有范式（normal form）的表达式。
于是，把每个表达式指称为一个数值，这种想法就可能有问题了。
下面我们引入不动点算子（fixed-point operator），用来它定义递归。
它表示，但是中f的值，是等式的解。
而中可能会包含。
的类型根据等式也是。
我们将看到，是与不动点算子的语法糖（syntactic sugar）。
首先，我们先用定义阶乘函数，来计算。
其中是下列等式的解。
不动点算子
从数学的角度来看，并不是所有形如的等式都有解，
如果有多个解，也不知道选择哪个解。
我们先假设每个这样的等式都有解，为此我们增加一个不动点算子来得到这个解。
一般的，如果是某一类型到自身的函数。
那么的一个不动点，是使得的值。
经过观察我们发现，阶乘函数是以下函数的的不动点，即满足。
其中，，
我们定义，，是对应于每个类型的不动点算子。
满足的如下等式公理，
可知，对任意的，是的不动点，即，
我们就可以用和表示了。
归约
我们以阶乘函数为例，来说明带有不动点算子的表达式是如何归约的。
为了行文方便，我们省略的下标，直接记为。
定义阶乘函数，其中，
我们来计算。
无法终止的运算
由于递归允许我们写出没有范式的表达式，
所以我们相应的必须给这样的表达式赋予含义。
例如，
尽管该表达式的类型是，但是我们无法把它简化为一个数值。
所以该表达式的含义就不是一个自然数了。
一方面，认为该表达式的类型是是合理的，它是类型规则的推导结论。
另一方面，如果我们说该表达式的值是『未定义的』，
那么的语义就变成了部分函数（partial function）。
我们不如给自然数集附加一个值，
用来表示类型上无法终止的运算（nonterminating computation）。
这给了我们一个把部分函数看成完全函数（total function）的方法。
CPO
偏序
一个偏序（partial order）是一个集合，以及集合上的一个关系（relation），
这个关系具有自反性，反对称性，和传递性。
若对于任意有，则称具有自反性（reflexive）。
若且有，则称具有反对称性（anti-symmetric）。
若且有，则称具有传递性（transitive）。
上界与最小上界
如果是一个偏序，则子集的上界（upper bound），
是中的一个元素，使得对于任意的有。
最小上界（least upper bound）是那个任何其它上界的元素。
有向集
如果是一个偏序，称子集是有向的（directed），
如果的每一个有限子集在中都有上界。
有向集（directed set）的一个性质是，所有有向集都非空。
完全偏序
完全偏序（complete partial order）简称CPO，它是一个偏序，
且每一个有向子集都有最小上界，我们把这个最小上界记为。
可证，任何一个有限的偏序，都是完全偏序。
一个不是CPO的例子是自然数集，自然数集本身是有向的，但没有最小上界。
如果我们加入一个比其他自然数都大的元素，我们就得到了一个CPO。
CPO的提升
有奇点的CPO
如果是一个有最小元（least element）的偏序，
则称为是有奇点（pointed）的，我们用表示的最小元。
提升集
对于任意的集合，我们构建一个CPO，，
其中，当且仅当或。
我们称为的提升集（lifted set）。
用这个方法，我们可以提升任何一个CPO，，
得到，
其中与中的任何元素都不等，新的序关系当且仅当或。
可证，如果是一个CPO，则是一个有奇点的CPO。
连续函数
单调函数
设和是CPO，
是集合到的一个函数，我们说是单调的（monotonic），
如果就有。
连续函数
一个单调函数是连续的（continuous），如果对于任意有向子集，有。
提升函数
我们定义对应的提升函数（lifted function）为。
其中，如果，则，否则。
函数集构成CPO
假设和是CPO，
对于连续函数，我们称，如果对于任意，都有。
于是，所有这些连续函数构成了一个CPO，记为。
最小不动点
我们称是的最小不动点（least fixed point），
如果且对于任意的，我们有。
如果是一个有奇点的CPO，且是连续的，则有最小不动点，
，
且是连续的。
例如，设是有奇点的CPO，则恒等函数的最小不动点是。
结语
初等数学中，某些函数是没有不动点的。
那么在什么情况下，形如的表达式有解呢？
定义了递归之后，对类型化lambda演算的模型产生了什么影响呢？
这是一直以来我心中是一个问题。
诚然，类型化lambda演算有不同的解释方式，但以上域论模型通俗易懂，
也算是告一段落吧，以后的路还长着呢。