是否可以证明这个定义的函数是 z3 的对合? [英] Is it possible to prove this defined function is an involution in z3?

问题描述

我试图了解如何定义断言，以证明已定义函数的某些数学特性.如 this post SMT 求解器不太适合用于证明数学质量的归纳法.

I'm trying to understand how to define an assertion in such a way that it proves certain mathematical qualities of an already defined function. As discussed in this post SMT solvers are not well-suited for induction, which is often needed to prove a mathematical quality.

在我的例子中，我有一个 identity function f(x) = x 的递归函数定义(只是一个简单的例子):

In my case, I have a recursive function definition for the identity function f(x) = x (just as a simple example):

(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 不会终止:

The same post suggests that such characteristics cannot be proven out-of-the-box. However, I am interested to know how general mathematical properties are proven in z3. I tried with all-quantifiers to prove the involution of the function but z3 does not terminate:

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

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

My Question: What assertion can we use to prove that such a recursive function is an involution with z3?

推荐答案

在这里你真的无能为力.理想情况下，策略是分别定义和证明基本情况和归纳步骤，然后(在元级别)论证该属性对所有字符串都为真.

There isn't really much you can do here. Ideally, the strategy would be to define and prove the base case and the inductive-step separately, and then argue (at the meta-level) that the property is true for all strings.

对于基本情况，事情很简单.我会定义:

For the base-case things are easy enough. I'd define:

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

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

然后:

(assert (not base_case))

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

If you do this, z3 will happily say unsat, i.e., base case is true. For the induction step, I'd define:

(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 作为子引擎的证明工具.

Alas, you'll find that z3 will choke on this query, i.e., won't terminate. Assuming for a second it did, you'd then conclude (at the meta-level) that identity is indeed an involution. But this has to be done at one-level above z3; either by a human, or some other proof tool that uses z3 as a sub-engine.

那么，自然的问题是要问让 z3 证明 inductive_step 的希望是什么?它绝对不会开箱即用.但也许您可以使用模式来哄它这样做，请参阅 https://rise4fun.com/z3/tutorialcontent/guide#h28 了解详情.但是，请注意，即使您可以通过非常巧妙的模式实例化来获得此证明，该证明也会非常脆弱:即使对您的定理或 z3 的实际实现进行微小更改也会影响结果，因为您将受无数启发式方法的支配.

So, the natural question is to ask what are the hopes for getting z3 to prove the inductive_step? It will definitely not do it out-of-the-box. But perhaps you can use patterns to coax it into doing so, see https://rise4fun.com/z3/tutorialcontent/guide#h28 for details. Be warned, however, that even if you can get this proof go with very clever pattern instantiations, the proof will be so very brittle: Even minor changes to your theorem or the actual implementation of z3 can affect the result, as you'll be at the mercy of a myriad of heuristics.

长话短说:如果您的目标是证明递归函数的属性，那么您使用了错误的工具.使用ACL2、HOL、Isabelle等； 有目的地设计和构建来处理这些定理.SMT 求解器不适合这里的要求.

Long story short: You're using the wrong tool if your goal is to prove properties of recursive functions. Use ACL2, HOL, Isabelle, etc.; which are purposefully designed and built to deal with such theorems. An SMT solver just doesn't fit the bill here.

这篇关于是否可以证明这个定义的函数是 z3 的对合?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！