diff --git "a/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" "b/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" index 63c2be9..a79aa63 100644 --- "a/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" +++ "b/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" @@ -693,7 +693,7 @@ #definition[蕴含/等价][ - 设 $calA, calB$ 是公式，称 $calA$ 蕴含 $calB$，记作 $calA models calB$，如果所有 $calA$ 的模型也是 $calB$ 的模型。 - 若 $calA, calB$ 互相蕴含，则称之为逻辑等价，记作 $calA eq.triple calB$ - ] + ] == 斯科伦式 #definition[][ 若公式 $exists x_i calB$ 出现在 $calA$ 中，且属于 $forall x_(i 1) ... x_(i t)$ 的辖域，则可删除 $exists x_i$ ，且以函项 $h_i^r (x_(i 1), ..., x_(i t))$ 替换 $x_i$，其中 $h_i^r (x_(i 1), ..., x_(i t))$ 称为斯科伦函项，替换后的公式称为斯科伦式。 @@ -742,7 +742,7 @@ $ tack calA => models calA $ - ] + ] #corollary[一致性][ K 是一致的，也即不存在公式 $calA$ 使得 $tack calA$ 且 $tack not1 calA$ ] @@ -878,10 +878,129 @@ + $tack forall x_i calA -> exists x_i calA$ ] ] -$ - ((alpha -> beta) -> alpha) -> alpha\ - ((alpha -> beta) -> alpha) -> (not1 alpha -> not1 (alpha -> beta))\ - not1 (alpha -> beta) -> alpha\ - (not1 alpha -> not1 (alpha -> beta)) -> (not1 alpha -> alpha) -$ - + == 等价 + #definition[可证等价][ + 若 $calA, calB$ 是公式，称 $calA$ 和 $calB$ 是可证等价的，如果 $tack calA <-> calB$ + ] + #proposition[][ + 可证等价是自反的、对称的、传递的 + ] + #proposition[][ + 若 $calA, calB$ 可证等价，则它们逻辑等价（@logic-equiv） + ] + #proof[ + 就是 @first-order-soundness + ] + #remark[][ + 逻辑等价也可以证明论地定义为： + $ + calA tack calB "iff" calB tack calA + $ + 使用之后我们会证明的一阶逻辑完备性，它和之前模型论的完备性是等价的。然而注意到，它与 + $ + tack calA <-> calB + $ + 并不相同，既然一阶逻辑的演绎定理需要一些额外的条件。 + ] + #proposition[变元换名][ + 假设 $x_j$ 不在 $calA$ 中（自由或约束）出现，则： + $ + tack forall x_i calA <-> forall x_j calA(x_i \/ x_j) + $ + ] + #definition[全称闭式][ + 设 $calA$ 中所有自由变元为 $x_1, x_2, ..., x_n$，则称： + $ + forall x_1 forall x_2 ... forall x_n calA + $ + 为 $calA$ 的全称闭式，将其记作 $calA'$。容易证明，逻辑闭式与 $calA$ 逻辑等价，但并不一定可证等价。 + ] + #theorem[替换定理][ + 设 $calA, calB$ 是公式，设 $calB_0$ 是用 $calB$ 替换 $calA_0$ 中的一次或多次替换 $calA$ 的出现的公式，则： + $ + tack (calA <-> calB)' -> (calA_0 <-> calB_0) + $ + ] + #proof[ + 往证： + $ + (calA <-> calB)' tack calA_0 <-> calB_0 + $ + 对 $calA_0$ 做结构归纳： + - $calA_0 = calA$ 显然 + - $calA_0$ 不含 $calA$ 作为子公式：显然 + - $calA_0 = calA_1 -> calA_2$，归纳假设给出： + $ + (calA <-> calB)' tack calA_1 <-> calB_1\ + (calA <-> calB)' tack calA_2 <-> calB_2 + $ + HS 容易给出 $(calA <-> calB)' tack calB_1 -> calB_2$ + - $calA_0 = not1 calA_1$，归纳假设给出： + $ + (calA <-> calB)' tack calA_1 <-> calB_1 + $ + 重言式 $(calA_1 <-> calB_1) <-> (not1 calB_1 <-> not1 calA_1)$ 给出： + $ + (calA <-> calB)' tack not1 calB_1 <-> not1 calA_1 = (calB_0 <-> calA_0) + $ + - $calA_0 = forall x_i calA_1$，归纳假设给出： + $ + (calA <-> calB)' tack calA_1 <-> calB_1 + $ + 同时注意到： + $ + calA_1 <-> calB_1 tack forall x_i (calA_1 <-> calB_1) tack forall x_i calA_1 <-> forall x_i calB_1 + $ + 这里对 $x_i$ 使用了 GEN 规则，但是既然 $(calA <-> calB)'$ 是全称闭式，因此不会破坏演绎定理的条件。 + ] + #corollary[][ + - 若 $tack calA <-> calB$，则 $tack calA_0 <-> calB_0$ + - 若 $tack calA <-> calB$，且 $tack calA_0$，则 $tack calB_0$ + ] + == 前束范式和子句范式 + #proposition[][ + - $tack not1 (forall x_i) calA <-> (exists x_i) not1 calA$ + - $tack not1 (exists x_i) calA <-> (forall x_i) not1 calA$ + 此外，若 $x_i$ 不在 $calA$ 中自由出现，则： + - $tack forall x_i (calA -> calB) <-> (calA -> forall x_i calB)$ + - $tack exists x_i (calA -> calB) <-> (calA -> exists x_i calB)$ + - $tack (exists x_i calB -> calA) <-> (not1 forall x_i not1 calB -> calA) <-> (not1 calA -> forall x_i not1 calB) <-> forall x_i (calB -> calA)$ + - $tack (forall x_i calB -> calA) <-> (not1 calA -> exists x_i not1 calB) <-> exists x_i (calB -> calA)$ + ] + #definition[前束范式][ + 称形如： + $ + Q_1 x_1 ... Q_n x_n calA + $ + 的公式为前束范式，其中 $Q_i$ 是量词，$x_i$ 是变元，$calA$ 是无量词公式。如果所有的存在量词都在全称量词的左边，则称之为斯科伦前束范式。此外，$calA$ 往往被化成命题逻辑的合取范式或析取范式。 + ] + #theorem[][ + 任意公式 $calA$ 都存在前束范式 $calB$ 与其可证等价 + ] + #proof[ + 由换名规则，不妨设 $calA$ 中自由变元和约束变元不存在重名。考虑 $calA$ 为： + - 原子公式：显然 + - $not1 calC$: 归纳假设给出 $calC$ 的前束范式 $Q_1 x_1 ... Q_n x_n calC'$，而： + $ + not1 Q_1 x_1 ... Q_n x_n calC' <-> Q_1^* x_1 ... Q_n^* x_n not1 calC' + $ + 其中 $Q_i^*$ 是 $Q_i$ 的对偶，成立性来自于 @prop-quantifier + - $calB -> calC$: + 归纳假设给出： + $ + tack calB <-> Q_1 x_1 ... Q_n x_n calB'\ + tack calC <-> P_1 y_1 ... P_n y_n calC' + $ + 无妨设 $x_i != x_j, x_1 != y_j$，则由替换定理的推论，有： + $ + tack (Q_1 x_1 ... Q_n x_n calB' -> P_1 y_1 ... P_n y_n calC') <-> calA + $ + ] + #definition[$Pi, Sigma$][ + 称前束范式为 $Pi_n$ 范式，如果它以全称量词开始，且量词交替 $n - 1$ 次。称前束范式为 $Sigma_n$ 范式，如果它以存在量词开始，且量词交替 $n - 1$ 次。该概念在涉及一阶逻辑的计算中很有用。 + ] + #theorem[弱等价性定理][ + 设 $K^s$ 是把 $K$ 的每个公理换成斯科林式而得，则： + - 若 $calB$ 是 $K$ 的公式且 $tack_(K^s) calB$，则 $tack_K calB$ + - $K$ 是一致的当且仅当 $K^s$ 是一致的 + ] diff --git "a/\350\256\272\346\226\207/scallop.typ" "b/\350\256\272\346\226\207/scallop.typ" index 7149b4c..5e87dec 100644 --- "a/\350\256\272\346\226\207/scallop.typ" +++ "b/\350\256\272\346\226\207/scallop.typ" @@ -53,24 +53,26 @@ $ P(x_i) = tP_i / norm(tP)_1 $ -== 概率的传播 - 设 $f: X -> Y$ 是函数，显然 $f(cal(X))$ 应该是一个概率空间。其上的概率非常典范的定义为： - $ - P(y) = sum_(x in Inv(f) (y)) P(x) - $ - 其中 $Inv(f) (y) = {x in X | f(x) = y}$ ，若 $f$ 已经给定，则它是非常容易计算的。上式右侧无非是一些求和，因此可以继承可微性。 -== 二元函数 - 设 $f: X times Y -> Z$ 是二元函数，则 $Z$ 上的概率定义为： - $ - P(z) = sum_((x, y) in Inv(f) (z)) P(x, y) - $ - 公式并没有问题，然而 $P(x, y)$ 的计算并不显然。注意到它不是简单的 $P(x) P(y)$，既然我们很可能不能假设 $cal(X), cal(Y)$ 独立。 +// == 概率的传播 +// 设 $f: X -> Y$ 是函数，显然 $f(cal(X))$ 应该是一个概率空间。其上的概率非常典范的定义为： +// $ +// P(y) = sum_(x in Inv(f) (y)) P(x) +// $ +// 其中 $Inv(f) (y) = {x in X | f(x) = y}$ ，若 $f$ 已经给定，则它是非常容易计算的。上式右侧无非是一些求和，因此可以继承可微性。 +// == 二元函数 +// 设 $f: X times Y -> Z$ 是二元函数，则 $Z$ 上的概率定义为： +// $ +// P(z) = sum_((x, y) in Inv(f) (z)) P(x, y) +// $ +// 公式并没有问题，然而 $P(x, y)$ 的计算并不显然。注意到它不是简单的 $P(x) P(y)$，既然我们很可能不能假设 $cal(X), cal(Y)$ 独立。 - 很明显，我们需要更细致地考察命题的构建过程。事实上，如果我们暂时不考虑变元，那么命题无非是： - - 原子命题 - - 逻辑与 - - 逻辑或 - 而我们可以假设，原子命题之间的概率分布是独立的，接下来无非是拆解成原子命题。 +// 很明显，我们只能更细致地考察命题的构建过程，自底向上的计算概率分布。事实上，如果我们暂时不考虑变元，那么命题无非是： +// - 原子命题 +// - 逻辑与 +// - 逻辑或 +// 而我们可以假设，原子命题之间的概率分布是独立的，接下来无非是拆解成原子命题。 +// == 带标签的概率传播 + // == Sentential Decision Diagram // // 考虑以下的程序： // // ```rust @@ -100,7 +102,18 @@ == 证明的构建 Scallop 实际上不去建立命题的真值的概率分布，而是建立命题的证明的概率分布。对于任何一个命题 $X$，我们可以把它视作一个类型，其中的值是所有 $X$ 的证明#footnote[原论文实际上没有使用“类型”而是简单的使用集合语言。不过这里也只是换一个术语，应该比集合套集合清晰一些]。自然的，原子命题只有一个证明，而： $ - A and B := A tensorProduct B, A or B := A directSum B + A tensorProduct B := A and B = A times B, A directSum B := A or B = A + B $ - 当然，不难验证 $tensorProduct, directSum$ 运算在命题空间上构成半环结构，称为 proof semiring#footnote[原文没有使用这套“命题等同于命题的所有证明”的语言，导致了非常拗口的“命题的所有证明构成的集合上的半环”]。可以想象，Datalog 程序的计算将给出任意一个命题所有证明树，沿着证明树计算最终命题的概率的问题称为 Weighted Model Counting（带权的模型计数），当然这个问题看起来就比 SAT 更难，所以我们需要更有实践性的方案。 - + 当然，不难验证 $tensorProduct, directSum$ 运算在命题空间上构成半环结构，称为 proof semiring。可以想象，Datalog 程序无非是由原子命题和 $tensorProduct, directSum$ 构成的表达式，因此我们可以得到析取范式： + $ + P = directSum_j (tensorProduct_i A_(i j)) + $ + 其中 $A_(i j)$ 是一些原子命题，根据 $A_(i j)$ 的概率计算 $P$ 的概率的问题称为 WMC（Weighted Model Counting）问题。当然这个计算过程听起来复杂度就是指数级的，因此需要一些近似算法。 +== top-k + 上面的思路无非是用逻辑演算构造一个分类问题，而分类问题中我们可以期望概率分布是相当不平衡的，大部分概率集中在少数几个类别上。因此，我们可以只考虑那些概率比较大的证明。具体来说，在上一页的公式中，我们可以只考虑 $P$ 中概率最大的 $k$ 个证明，这样就得到了 top-k 算法。换言之，重新定义： + $ + A tensorProduct B := "Top"_k (A and B) , A directSum B := "Top"_k (A or B) + $ + 可以证明这样定义的运算仍然构成半环，因此可以在其上高效地计算 WMC +== 梯度传播 + 可以想象梯度的计算和概率的计算应该是一体的。因此为了能够计算梯度，只需要在计算概率的同时再加一个梯度的记录即可，论文中将其称为 _gradient semiring augmented WMC procedure_