等式逻辑与未解释函数

等式逻辑

等式逻辑(equality logic)可以认为是命题逻辑, 这种命题逻辑的原子都是等式, 等式两边是变量或者一边是变量一边是常数. 等式逻辑的文法如下: \[ \begin{aligned} formula&:formula\land formula\ |\ \neg formula\ |\ (formula)\ |\ atom\\ atom&:term\ =\ term\\ term&:identifier\ |\ constant \end{aligned} \] 举个例子, 公式 \((y=z\lor (\neg(x=z)\land x=2))\) 是良形式的等式逻辑公式, 变量 \(x,y,z\in \mathbb{R}\). 一组可满足的赋值为 \(\{x\mapsto2,y\mapsto2,z\mapsto0\}\).

针对等式逻辑的可满足性问题是属于 NPC 的, 即确定性图灵机可以在较大的时间复杂度类别中求解它, 并且可以在多项式时间内验证其解的问题. 实际上等式逻辑和命题逻辑都是 NPC 问题, 这意味着二者可以对同一个判定问题进行建模. 那么为什么还要引入等式逻辑呢? 主要有两个原因,

1. 方便建模 对于某些特定问题, 用等式逻辑进行建模要更加自然和方便, 反之亦然.
2. 高效 输入等式逻辑公式中的高阶结构可以潜在地用于使判定过程更快地工作. 如果直接在命题逻辑中对问题进行建模, 则一些信息可能会丢失.

通常来说, 等式逻辑公式中是有布尔变量的. 但是, 我们并不应该把他们集成到理论的定义中, 这是为了保证算法描述尽可能简单. 布尔变量能够通过在输入的公式中用两个新变量的等式关系替换掉. 但是, 这并不是十分高效的解决办法. 后文将说明如何直接处理这些布尔变量.

未解释函数

等式逻辑在与未解释函数(uninterpreted functions)结合的时候会变得非常有用. 简单来说, 未解释函数的作用就是用来抽象, 泛化或者定理化. 不像其他函数符号, 未解释函数不应被解释为公式模型的一部分, 也就是说, 在公式中, 未解释函数单单是一个未释义的函数. 比如说如下公式, \(F\) 和 \(G\) 是未解释的, 二元运算符"+"就为常用的加法功能: \[ F(x)=F(G(y))\lor x+1=y. \] 带有未解释函数的等式逻辑的文法定义如下: \[ \begin{aligned} formula &: formula \land formula\ |\ \neg formula\ |\ (formula)\ |\ atom\\ atom &: term = term\ |\ predicate-symbol\ (list\ of\ terms)\\ term &: identifier\ |\ function-symbol\ (list\ of\ terms)\\ \end{aligned} \] ### 未解释函数的使用

用未解释函数去替换公式中原本的函数时常用的技术, 使得公式更容易推理(比如, 证明其有效性). 看如下推理规则: \[ \models\varphi^{UF}\Longrightarrow\ \models\varphi.\tag{1} \] 其中 \(\models\varphi^{UF}\) 代表公式 \(\varphi\) 中一些或者全部函数被未解释函数替换后形成的公式. 未解释函数被广泛应用于微积分和其他数学分支, 但是在推理和验证领域, 主要应用于简化证明过程. 在某些情况下, 未解释函数能够让我们在忽略一些后者全部函数语义的时候对系统进行推理, 假设这些函数对于证明并不是必要的. 忽略函数的语义是指, 一个解释并不需要为了满足公式而去满足这些原子. 它唯一需要满足的是一个公理, 该公理表明未解释的函数与任何函数一样都是一致的, 即给定相同的输入, 它将返回相同的输出. 这是函数一致性(functional consistency)的要求. 所谓函数一致性(功能一致性), 就是相同函数的实例接受相等的参数, 那么返回值也是相等的. 有很多实例, 无论对于函数的解释如何, 公式总是有效的. 在这些例子中, 未解释函数极大地简化了证明过程, 尤其是在借助自动定理证明工具进行机械证明地时候.

假设我们有检查 EUF 公式的方法. 基于这个假设, 使用未解释函数的基本框架如下:

1. 符号 \(\varphi\) 代表带有未解释函数的公式. 假设检查公式 \(\varphi\) 的有效性的计算复杂度非常高, 甚至无法计算.
2. 对公式 \(\varphi\) 中的每一个函数都用一个与之对应的未解释的函数进行赋值, 并记新公式为 \(\varphi^{UF}\).
3. 检查公式 \(\varphi^{UF}\) 的有效性. 如果它是有效的, 那么返回" \(\varphi\ 是有效的\)". 否则, 返回"无法判定".

步骤2的执行会付出一些代价, 因为会丢失信息. 就像上文提到的, 它会导致验证过程的不完备, 即使原公式是属于可判定的逻辑. 由此, 当一个对于输入公式的判定过程的计算太过复杂的时候, 可以设计 一个程序将公式中函数的解释版本替换成未解释版本.

例子: 证明程序的等价性

考虑如下两个在功能上一致的 C 程序(a)和(b), 目的是证明它们对于每一个可能的输入"in"都返回相同的值.

int func(int in){
    int i, out_a;
    out_a = in;
    for(i = 0; i < 2; i++){
        out_a = out_a * in;
    }
    return out_a;
}

(a)

int func_new(int in){
    int out_b;
    out_b = (in * in) * in;
    return out_b;
}

(b)

通常来说, 证明两个程序等价是不可判定的, 换句话说, 没有一个既可靠又完备的方法证明这样的等价性. 但是在当前的例子中, 等价性是可判定的. 关于这些程序的一个关键是它们只有有限循环，因此可以计算它们的输入/输出关系。 从这两个程序推导这些关系可以如下进行:

1. 移除变量声明和 return 语句.
2. 展开 for 循环.
3. 用新的辅助变量替换每个赋值语句中的左侧变量.
4. 无论在何处读取变量(在表达式中引用), 都应使用辅助变量替换该变量, 该辅助变量会在赋值的最后位置替换该变量.
5. 将所有程序语句合取起来.

上述操作的结果变为两个公式 \(\varphi_a\) 和 \(\varphi_b\) , 如下所示: \[ \begin{aligned} out0\_a&=in0_a\ &\land\\ out1\_a&=out0\_a*in0_a\ &\land\\ out2\_a&=out1\_a*in0_a\\ \\ &\hspace{10mm}(\varphi_a) \end{aligned} \] \[ \begin{aligned} out0\_b&=(in0_b*in0_b)*in0_b\\ \\ &\hspace{10mm}(\varphi_b) \end{aligned} \] 所以证明程序(a)和(b)等价性的问题就转化为, 证明如下公式的有效性: \[ in0_a=in0_b\land\varphi_a\land\varphi_b\Longrightarrow out2_a=out0_b. \] 未解释函数可以帮助证明程序(a)和(b)的等价性. 在这种情况下, 这样做的动机是计算上的, 确定乘以例如64位变量的公式非常困难. 用未解释函数替换乘法符号可以解决该问题. \[ \begin{aligned} out0\_a&=in0\_a&\land\\ out1\_a&=G(out0\_a,in0\_a)&\land\\ out2\_a&=G(out1\_a,in0\_a)\\ \\ &(\varphi^{UF}_a) \end{aligned} \]

\[ \begin{aligned} out0\_b&=G(G(in0\_b,in0\_b),in0\_b)\\ \\ &\hspace{3mm}(\varphi^{UF}_b) \end{aligned} \]

如上所示, \(\varphi^{UF}_a\) 和 \(\varphi^{UF}_b\) 是在对公式 \((\varphi_a)\) 和 \((\varphi_b)\) 用未解释函数 \(G\) 进行替换之后的公式. 所以现在, 我们可以尝试验证 \[ \varphi^{UF}_a\land\varphi^{UF}_b\Longrightarrow\ out2\_a=out0\_b. \]

通过同余闭包判定等式和未解释函数的合取式

现在说明一个用于解决等式逻辑和未解释函数合取式的方法. 从变量和未解释函数的等式和不等式的合取式 \(\varphi^{UF}\) 开始, 基于计算等效类的算法有两个阶段. 下面所示算法版本假设未解释函数只接收一个参数. 见算法1所示. \[ \begin{aligned} &\mathbf{Algorithme\ 1:\ }{\rm CONGRUENCE\mbox{-}CLOSURE}\\ &\mathbf{Input:\ }{\rm A\ conjunction\ }\varphi^{UF}\ {\rm of\ equality\ predicates\ over\ variables\ and\ uninterpreted\ functions}\\ &\mathbf{Output:\ }{\rm ''Satisfiable''\ if\ }\varphi^{UF}\ {\rm is\ satisfiable,\ and\ ''Unsatisfiable''\ otherwise}\\ \\ &1.\hspace{2mm}{\rm Build\ congruence\mbox{-}closed\ equivalence\ classes.}\\ &\hspace{6mm}{\rm (a)\ \ Initially,\ put\ two\ terms\ }t_1,t_2\ {\rm (either\ variables\ or\ uninterpreted\mbox{-}function\ instances)\ in\ their\ }\\ &\hspace{15mm}{\rm own\ equivalence\ class\ if\ }(t_1=t_2)\ {\rm is\ a\ predicate\ in\ }\varphi^{UF}.\ {\rm All\ other\ variables\ form\ singleton\ }\\ &\hspace{15mm}{\rm equivalence\ classes.}\\ &\hspace{6mm}{\rm (b)\ Given\ two\ equivalence\ classes\ with\ a\ shared\ term,\ merge\ them.\ Repeate\ until\ there\ are\ no\ }\\ &\hspace{15mm}{\rm more\ classes\ to\ be\ merged.}\\ &\hspace{6mm}{\rm (c)\ Compute\ the\ }congruence\ closure:{\rm given\ two\ terms\ }t_i,t_j\ {\rm that\ are\ in\ the\ same\ class\ and\ that\ }\\ &\hspace{15mm}F(t_i)\ {\rm and\ }F(t_j){\rm\ are\ terms\ in\ }\varphi^{UF}\ {\rm for\ some\ uninterpreted\ function\ }F,\ {\rm merge\ the\ classes\ of\ }\\ &\hspace{15mm}F(t_i)\ {\rm and\ }F(t_j).\ {\rm Repeat\ util\ there\ are\ no\ more\ such\ instances.}\\ &2.\hspace{2mm}{\rm If\ there\ exists\ a\ disequality\ }t_1\ne t_j\ {\rm in\ }\varphi^{UF}\ {\rm such\ that\ }t_i {\rm and\ }t_j\ {\rm are\ in\ the\ same\ equivalence\ class,\ }\\ &\hspace{6mm}{\rm returen\ ''Unsatisfiable''.\ Otherwise\ return\ ''Satisfiable''.} \end{aligned} \] 算法说明:

该算法的输入是变量和未解释函数的等式谓词的合取公式 \(\varphi^{UF}\); 输出是, 返回可满足如果公式 \(\varphi^{UF}\) 是可满足, 否则返回不可满足.

1. 建立同余闭包等价类

   1. 初始化, 将两个项(变量或者未解释函数的实例)置入它们自己的等式集合中如果 \((t_1=t_2)\) 是公式 \(\varphi^{UF}\) 中的断言. 所有其他变量构成单例等价类.

   2. 给定两个具有相同项的等价类, 将它们合并. 重复直到不再有要合并的类.

   3. 计算同余闭包: 给定两个在同一个类中的项 \(t_i,t_j\), 并且 \(F(t_i)\) 和 \(F(t_j)\) 是公式中 \(\varphi^{UF}\) 某些未解释函数的项, 合并 \(F(t_i)\) 和 \(F(t_j)\). 重复直到没有此类实例.

2. 如果在公式 \(\varphi^{UF}\) 中存在不等式 \(t_i\ne t_j\), 而且 \(t_i\) 和 \(t_j\) 是在同一个等价类中, 那么返回不可满足. 否则返回可满足.

比如, 考虑如下合取式 \[ \varphi^{UF} := x_1=x_2\land x_2=x_3\land x_4=x_5\land x_5\ne x_1\land F(x_1)\ne F(x_3). \] 在初始步骤中, 等价类为 \[ \{x_1, x_2\},\{x_2, x_3\},\{x_4,x_5\},\{F(x_1)\},\{F(x_3)\}. \] 步骤 1.b 合并前两个类: \[ \{x_1,x_2,x_3\},\{x_4,x_5\},\{F(x_1)\}, \{F(x_3)\}. \] 下一步骤合并包含 \(F(x_1)\) 和 \(F(x_3)\) 的类, 因为 \(x_1\) 和 \(x_3\) 在同一个类中: \[ \{x_1,x_2,x_3\},\{x_4,x_5\},\{F(x_1),F(x_3)\}. \] 在步骤 2 中, 可见 \(F(x_1)\ne F(x_3)\) 是公式 \(\varphi^{UF}\) 的断言, 但是 \(F(x_1)\) 和 \(F(x_3)\) 是在同一个类中. 因此, 公式 \(\varphi^{UF}\) 不可满足.