时间戳

首页 > 解决方案 > 是否有可能证明这个定义的函数是 z3 中的对合？

z3 - 是否有可能证明这个定义的函数是 z3 中的对合？

问题描述

我试图了解如何定义断言，以证明已定义函数的某些数学特性。正如这篇文章中所讨论的， SMT 求解器并不适合归纳，这通常是证明数学质量所必需的。

在我的例子中，我有一个用于标识函数 f(x) = x的递归函数定义（作为一个简单的例子）：

(define-fun-rec identity-rec ((l String)) String
   (ite (= 0 (str.len l))
      ""
      (str.++ (str.at l 0) (identity-rec (str.substr l 1 (seq.len l))))))



(define-fun identity ((l String)) String
   (ite (= 0 (str.len l))
      ""
      (identity-rec l)))

同一篇文章表明，这些特征不能被证明是开箱即用的。但是，我很想知道如何在z3. 我尝试使用全量词来证明函数的对合z3，但没有终止：

(assert
(forall ((a String))
    (=
        a
        (indentity (identity a))
    )
)

我的问题： 我们可以用什么断言来证明这样的递归函数是与 的对合z3？

标签： z3smt

解决方案

你可以在这里做的真的不多。理想情况下，策略是分别定义和证明基本情况和归纳步骤，然后（在元级别）论证该属性对于所有字符串都是正确的。

对于基本情况，事情很容易。我会定义：

(define-fun check-inv ((x String)) Bool (= (identity (identity x)) x))

(define-fun base_case () Bool (check-inv ""))

接着：

(assert (not base_case))

如果你这样做，z3 会很高兴地说unsat，即基本情况为真。对于归纳步​​骤，我会定义：

(define-fun inductive_step () Bool
   (forall ((x String) (c String))
        (implies (and (= 1 (str.len c)) (check-inv x))
                 (check-inv (str.++ c x)))))

并希望证明：

(assert (not inductive_step))

唉，你会发现 z3 会在这个查询上阻塞，即不会终止。假设它确实这样做了，那么您会得出结论（在元级别上）这identity确实是一个内卷。但这必须在 z3 之上的一级完成；由人类或其他使用 z3 作为子引擎的证明工具。

所以，很自然的问题是问让 z3 证明 的希望是什么inductive_step？它绝对不会开箱即用。但也许您可以使用模式来哄它这样做，有关详细信息，请参阅https://rise4fun.com/z3/tutorialcontent/guide#h28。但是请注意，即使您可以通过非常聪明的模式实例化来获得此证明，证明也将非常脆弱：即使对您的定理或 z3 的实际实现进行微小更改也会影响结果，因为您将受无数启发式的摆布。

长话短说：如果您的目标是证明递归函数的属性，那么您使用的是错误的工具。使用ACL2、HOL、Isabelle等；它们是专门为处理此类定理而设计和构建的。SMT 求解器不符合这里的要求。

推荐阅读