代数数据类型
一个代数数据类型，由值的一些集合，以及这些集合之间的一些函数构成。
这些函数都是一阶函数，不能以其他函数作为参数。
泛代数
泛代数（universal algebra）也称为等式逻辑（equational logic），
是用于研究代数数据类型的一个数学框架。
在泛代数中，代数数据类型的语法由代数项（algebraic term）描述，公理语义用项之间的等式集（a set of equations）描述，
而指称语义对应于一个代数，操作语义通过给等式设定方向来表示。
代数数据类型的语法
代数项和签名
一个代数项（algebraic term）由符号和类型来定义，
这些信息放在一起称为代数项的签名（signature）。
构成代数项的基本类型称为sort。
一个签名，由以下几个部分构成，
（1）以sort为元素构成的集合
（2）sort上函数符号的集合
其中，，称为类型化的函数符号，
每个函数符号的类型是唯一的。
例如，自然数表达式的签名是，
其中，只包含一个sort，
给出以下几个函数符号，
，，，。
习惯上为了节省空间，通常把签名写成一个表格形式，
变量的指派
一个指派（sort assignment），是如下一个有限集合，用来指定变量的类型，
不能为同一个变量指派不同的sort。
合法代数项的集合
基于签名和指派，可以定义一个sort为的代数项的集合，
它满足以下几个条件，
（1）如果则
（2）如果且，
，则
代数数据类型的指称语义
代数
代数是一种数学结构，它为代数项提供了含义或指称语义。
一个代数，包含了一个或多个集合，称为载体（carrier），
以及一些特征元素，和载体上的一些一阶函数，
例如，代数
具有载体，它是自然数集，
具有特征元素，，
以及函数，。
其中，特征元素可以看成零元函数。
带有多个载体的例子是代数
其中是自然数集，是布尔值集，
是自然数，是加法函数。
代数项的解释
我们说是与所有合法代数项对应的代数，
指的是如下对应关系成立，
（1）每一个sort，，恰好对应一个载体
（2）每一个函数符号，恰好对应一个函数
习惯上把写成。
含变量代数项的解释
代数的环境，是把变量映射到的各载体中元素的一个映射。
需要环境的原因是，对于含变量的项，叙述的含义必须先给指定一个确定的值。
如果对于每个，都有，就说环境满足指派。
假定代数的一个环境满足指派，
则可以把环境下的任何项的含义定义如下，
（1）
（2）
若代数在上下文中是明确的，通常省略而直接写，
若中没有变量，则不依赖于，可以写为。
语法和语义的关系
可靠性与完备性
代数数据类型的公理语义是由代数项之间的等式集给出的，签名和等式集合称代数规范（algebraic specification）。
一个代数规范，或者可以使用等式证明系统推导出代数项之间的其他等式，或者可以检验代数项对应的代数是否满足这些等式的要求。
代数项对应的代数并不是唯一的。
从一个代数规范推导得到的等式，在该规范对应的任何代数中都成立，就称该代数证明系统是可靠的（sound）。
一个代数规范对应的任何代数中都成立的等式，在该规范中都可证，就称该代数证明系统是完备的（complete）。
等式的可满足性
等式（equation）是一个公式，其中，。
如果环境满足指派，且，
就说代数在环境下满足，记为
对于含变量的项，我们更感兴趣的是一个等式是否在变量所有可能的取值情况下都成立，
而不是在一个特别的环境中成立。
如果对于满足的任何一个环境都有，
就可以说，代数满足等式，记为
可满足性也可以扩展到等式集和代数集，
设是一个等式集，如果满足所有等式，就说满足。
类似的，若是一类代数，且对每个都有，则
若任何一个代数都满足代数项之间的等式，就说该等式是永真的（valid），写为。
例如，就是永真的。
若满足签名上的所有等式，就说代数是平凡的（trivial）。
语义蕴含（semantic implication）
若满足等式集的每一个代数都满足等式，
则称签名上的等式集在语义上蕴含等式，记为，
有了签名和等式集，我们定义代数规范，
则满足代数规范的，在所有代数中都成立的等式，就是那些由等式集语义蕴含的等式。
语义理论
如果等式集在语义蕴含下封闭（closed），则把它称为一个理论（theory）。
更准确的说，如果，则，那么等式集就称为一个语义理论（semantic theory）。
一个代数的理论，就是在中成立的所有等式的集合。
可以证明一个代数的理论是一个语义理论。
形式证明
一个证明系统的推导规则如下，，
使得从前件（antecedent）的任何实例出发，通过使用该证明系统的公理和其他规则，
可以推导出后件（consequent）的相应实例。
例如：
若证明了一条规则是可推导的，则能够把它当做系统的一条证明规则来使用。
如果某条规则没有前件，则称它是证明系统的一条公理（axiom）。
我们说等式是可证的（provable），记为
如果从到存在一个等式序列，
使得每个等式或者是公理（axiom），或者是中的等式，
或者是从序列中之前出现的一个或多个等式经一步推导得到的结果。
语法理论
若在可证性下等式集是封闭的，则称是一个语法理论（syntactic theory）。
换句话说，如果，则，那么等式集就称为一个语法理论。
的语法理论就是从可证的所有等式的集合。
等式证明系统的性质
可靠性（soundness）：若，则
演绎完备性（deductive completeness）：若，则
结语
《Foundations for Programming Languages》是一本好书，
可是中文的翻译《程序设计语言理论基础》简直是晦涩难懂，
把sort翻译为『类子』，把signature翻译为『基调』，容易让人误以为和同调代数有什么联系。
原版书拿到后，看起来轻松了不少，这里只是对第三章部分内容做了个小结，以便卸下包袱轻装上阵。