回顾
上文我们介绍了哥德尔定理，它指出了形式化方法的局限性，
任何包含初等算术的形式理论，都是不完全的，
且自身的协调性无法在系统内部被证明。
为了理解这句话，上文中我们做出了严谨的定义，
仔细建立了语法和语义之间的联系。
实际上，语法（符号）层面的推导，属于公式的证明，
而语义（模型）层面的推导，属于逻辑结论的推理。
证明和推理之间的关系由系统的可靠性和完全性给出。
1. 简单类型化演算
在《你好，类型》系列文章中，
我们介绍了简单类型化演算（simply typed lambda calculus），
它是一个形式系统，采用公理化的方式定义。
当时我们看来，系统中的项，只是一堆符合推导规则的符号，
我们并不知道它到底代表什么含义。
例如，，只是一个符号串，
自然数集上的后继函数f(x)=x+1，能不能作为它的解释，我们是不清楚的，
只是猜想可能是。
不幸的是，后继函数并不足以作为的解释，
因为，集合上的后继函数是没有不动点的，而有不动点。
我们曾经在《递归函数》系列文章中给出过证明。
2. 代数
一般有两种通用的方法，来给出简单类型化演算的语义，
一种是Henkin模型，另一种是笛卡尔闭范畴。
范畴论我们可以稍后再介绍，这里先介绍Henkin模型，
不过在这之前，我们还得先了解一些代数相关的内容。
代数是一种数学结构，
一个代数，包含了一个或多个集合，称为载体（carrier），
以及一些特征元素，和载体上的一些一阶函数，
例如，代数
具有载体，它是自然数集，
具有特征元素，，
以及函数，。
其中，特征元素可以看成零元函数。
带有多个载体的例子是代数
其中是自然数集，是布尔值集，
是自然数，是加法函数。
3. 代数数据类型的签名（signature）
在简单类型化演算中，类型属于形式系统中的概念，
它并不代表类型中值的集合。
这种认识可能有助于澄清人们对编程语言中类型的误解。
例如，我们可以为初等算术系统赋予类型，
指定，，，，
分别为常元符号和，以及二元函数符号和的类型。
常元符号也可以看成是零元函数符号。
这里，我们称以下二元组，
为初等算术系统的类型签名。
其中，是系统中类型的集合，
是函数符号的集合。
一般的，一个类型签名（signature），由以下两部分构成，
（1）是以类型为元素构成的集合，
（2）是类型上函数符号的集合，
其中，。
并且，除了初等算术系统，某些系统中可能还会包含变量，
因此，为了完成类型化，我们还需为这些变量指定类型。
我们称有限集，
为变量的一个指派（assignment）。
其中，是类型。
有了签名和指派之后，
类型为的项的集合就可以这样定义了，
（1）如果则
（2）如果且，，
则
具有多种类型的项的集合可以记为，
其中为类型的集合。
4. 项的解释
代数，与类型化的项的集合之间，存在着解释关系。
如果满足以下两个条件，
（1）对于每一个类型，恰好存在代数中的一个载体与之对应，
（2）每一个函数符号，
恰好存在集合上的一个函数与之对应，
也可以写成。
我们就称就是所对应的代数。
为了解释含变量的类型化的项，我们需要定义环境的概念。
代数的环境，指的是把变量映射到的各载体中元素的一个映射，
对于含变量的项，为它指定了载体上的一个唯一确定的值。
如果对于指派而言，，都有，
我们就说环境满足指派。
假定代数的一个环境满足指派，
在这个环境中，我们就可以将任何项的含义定义如下，
（1）
（2）
5. 例子
上文我们介绍了初等算术系统的类型签名，
其中，，。
我们可以选择代数作为它的解释，
它的载体为自然数集，分别为自然数集上的零元和一元函数。
如果初等算术系统中的项包含变量，
我们就可以为代数指定环境。
例如，我们可以假定环境满足，
则在这个环境中，的语义就可以按下式确定了。
总结
本文介绍了一种称为代数的数学结构，
它可以用来解释带有类型签名的项。
可是，要想让这样的代数称为项的模型，还是不够的，
我们还必须保证每一个项的解释，都在模型中。
为此代数还要满足一些额外的条件。
下文我们再详细讨论这些条件。