Page 34 - 《软件学报》2026年第2期

冯维直 等: 带递归定义的 SMT 公式求解技术综述 513

如果两个项是可合一的 (unifiable), 则它们存在一个唯一的 mgu, 写作 mgu(s,t).
A 上的一个二元关系 (binary relation) A×A 的一个子集. 常见的二元关系如非自反关系
在集合 R 是笛卡尔积
,
(irreflexive relation): 满足 a R b 蕴含对任意 a, b ∈ A a , b; 传递关系 (transitive relation): 满足对任意 a, b, c ∈ A,
R 是良基 R
a R b 且 b R c 可推出 a R c. 称集合 A 上的一个关系 (well-founded), 当 A 的所有非空子集都至少有一个
关系下的最小元.
1.3 代数数据类型理论
代数数据类型理论 (下面简称为 ADT 理论) 是函数式编程与类型论中的重要概念, 在有些文献中也被称为归
纳数据类型或递归数据类型 (inductive or recursive datatype) . ADT 理论的公式通常用来编码程序中需要使用递
[4]
归定义来描述的数据结构, 例如列表 ( list) 和二叉树 ( tree), 以及该数据结构相关的运算. 形式化定义代数数据类
d
d
型的符号集 Σ 为类型 (sort) 的序列 σ ,...,σ 和构造子 (constructor) 的序列 f 1 ,..., f m . 通常将 n 元构造子写作
1 k
d
d
f i : σ 1 ×...×σ n → σ 0 , 其中 σ 0 ,...,σ n ∈ {σ ,...,σ }, 将 0 元构造子称作常数 (constant) 或基础构造子 (base constructor).
1
k
d d f i : σ . 另外定义选择子 (selector) j f i -项的第
d
若 f i 返回类型 σ , 例如 f i : σ 1 ×...×σ n → σ , 则写作 f , 表示提取一个
j j j i
j 个参数; 定义测试子 (tester) is (f i ) , 用于决定一个项是否是 f i -项 (在有些文献中也称为 destructor). 代数数据类型理
ϕ 的语法定义为如下规则.
论中项 t 和公式
t ::= x variable
| f i (¯ t) constructor
j
| f (t) selector
i
ϕ (t) tester
::= is f i
| t = t equality
| ϕ∧ϕ | ϕ∨ϕ | ¬ϕ |... Boolean operator
例 1: 在 ADT N 如下:
理论中递归定义自然数
nat := O|s(x) : nat.
α 的列表 ( list(α)) 为:
定义类型
list := nil|cons(x : α,y : list),
p p(s(x)) = x. 则可以定义自然数中的一些基础项, 例如
s
则 nat 中 O 为基础构造子, 为一元构造子, 定义选择子 , 0
定义为 O, 1 定义为 s(O), 2 定义为 s(s(O)) 等. 另外由选择子定义有 p(s(s(O))) 等于 1. list 中 nil 为基础构造子, cons
x
为二元构造子, 其两个参数分别为类型为 α 的 和类型为 list 的 y . 在有些文献或表示习惯中也写成中缀表
2
1
x y
达式::, 即 cons(x,y) 等同于 :: . 定义选择子函数 cons 和 cons (通常写为 head 和 tail), 有 head(cons(x,y)) = x,
tail(cons(x,y)) = y.
若 α 为 nat 类型, 我们可定义一些自然数的列表, 如空列表 nil, 只有 1 个元素 0 的列表 l 0 为 cons(O,nil), 由 1、
,
0 组成的列表 l 1 为 cons(s(O), cons(O,nil)) 等. 且 (l 1 ) = s(O) tail(l 1 ) = cons(O,nil).
例 CList 类型:
2: 我们考虑一个代数数据类型理论中可满足赋值的例子, 如下定义 color 和

color := red|green|blue
 .


CList := nil|cons(h : Color,t : CList)
于是这里类型 color 构造子为 red、 green、 blue, 它们都是基础构造子, 也称为常数或 0 元构造子. CList 构造
子为 nil 和 cons, 其中 nil 为基础构造子, cons 为二元构造子 cons : Color×CList → CList. 定义 head 和 tail 为选择
子: head(cons(h,t)) = h tail(cons(h,t)) = t. 若给定类型为 CList 的变量 x 和类型为 Color 的变量 y, 我们可以构建一
,
个 ADT 公式为:
is cons (x)∧¬(y = blue)∧(head(x) = red ∨ x = cons(y,nil)) (1)
其中, is cons (x) 为 tester, 它为 true 当且仅当 x 是具有 cons 构造子的项. 求解公式 (1), 可以找到一组可满足的赋值
{x 7→ cons(red,nil),y 7→ green}. 具体的 ADT 理论公式求解算法将在第 2.2 节中进行介绍.