z3中的最大递归界限

Question

我在下面编写了一个基准来生成两个列表的叉积。 z3 是否有某种最大递归界限？出于某种原因，它可以推理大小为 1 而不是大小为 2 的列表。或者我在形式化的某个地方有错误？

(declare-datatypes ((MyList 1)) ((par (T) ((cons (head T) (tail (MyList T))) (nil)))))
(declare-datatypes (T2) ((Pair (pair (first T2) (second T2)))))

; list functions for lists of ints
(define-fun prepend ( (val (Pair Int)) (l (MyList (Pair Int))) ) (MyList (Pair Int)) (cons val l))

(declare-fun get ( (MyList Int) Int ) Int)
(assert (forall ( (h Int) (t (MyList Int)) (i Int) )
                (ite (<= i 0)
                     (= (get (cons h t) i) h)
                     (= (get (cons h t) i) (get t (- i 1))))))

(declare-fun list_length ( (MyList Int) ) Int)
(assert (= (list_length (as nil (MyList Int))) 0))
(assert (forall ( (val Int) (l (MyList Int)) )
                (= (list_length (cons val l)) (+ 1 (list_length l)))))

(declare-fun tail ( (MyList Int) Int ) (MyList Int))
(assert (forall ( (start Int) (h Int) (t (MyList Int)) )
                (ite (<= start 0)
                     (= (tail (cons h t) start) (cons h t))
                     (= (tail (cons h t) start) (tail t (- start 1))))))
(assert (forall ( (start Int) )
                (= (tail (as nil (MyList Int)) start) (as nil (MyList Int)))))


; same list functions but for lists of int pairs -- 
; would be great if there is a way to avoid redefining all these again :(
(declare-fun list_get_pair ( (MyList (Pair Int)) Int ) (Pair Int))
(assert (forall ( (h (Pair Int)) (t (MyList (Pair Int))) (i Int) )
                (ite (<= i 0)
                     (= (list_get_pair (cons h t) i) h)
                     (= (list_get_pair (cons h t) i) (list_get_pair t (- i 1))))))

(declare-fun list_length_pair ( (MyList (Pair Int)) ) Int)
(assert (= (list_length_pair (as nil (MyList (Pair Int)))) 0))
(assert (forall ( (val (Pair Int)) (l (MyList (Pair Int))) )
                (= (list_length_pair (cons val l)) (+ 1 (list_length_pair l)))))

(declare-fun tail_pair ( (MyList (Pair Int)) Int ) (MyList (Pair Int)))
(assert (forall ( (start Int) (h (Pair Int)) (t (MyList (Pair Int))) )
                (ite (<= start 0)
                     (= (tail_pair (cons h t) start) (cons h t))
                     (= (tail_pair (cons h t) start) (tail_pair t (- start 1))))))
(assert (forall ( (start Int) )
                (= (tail_pair (as nil (MyList (Pair Int))) start) (as nil (MyList (Pair Int))))))

(declare-fun concat ( (MyList (Pair Int)) (MyList (Pair Int)) ) (MyList (Pair Int)))
(assert (forall ((xs (MyList (Pair Int))) (ys (MyList (Pair Int))))
            (ite (= (as nil (MyList (Pair Int))) xs)
                 (= (concat xs ys) ys)
                 (= (concat xs ys) (prepend (list_get_pair xs 0) (concat (tail_pair xs 1) ys))))))                 

(assert (forall ((xs (MyList (Pair Int))) (ys (MyList (Pair Int))))
            (=> (= (as nil (MyList (Pair Int))) ys)
                (= (concat xs ys) xs))))

; two functions defined using recursive construct                
(define-funs-rec
(
(cross_helper ((i Int) (ys (MyList Int))) (MyList (Pair Int)))
(cross ((xs (MyList Int)) (ys (MyList Int))) (MyList (Pair Int)))
)
(
; cross_helper - given e and [a, b, c] return [(e,a), (e,b), (e,c)]
(ite (= ys (as nil (MyList Int))) (as nil (MyList (Pair Int)))
     (prepend (pair i (get ys 0)) (cross_helper i (tail ys 1))))


; cross - given [a, b] and [c, d] return [(a,c), (a,d), (b,c) (b,d)]
(ite (= xs (as nil (MyList Int))) (as nil (MyList (Pair Int)))
     (concat (cross_helper (get xs 0) ys) (cross (tail xs 1) ys)))
))


(declare-const in1 (MyList Int)) (declare-const in2 (MyList Int))
(declare-const i Int) (declare-const j Int)
(declare-const in11 Int) (declare-const in12 Int) 
(declare-const in21 Int) (declare-const in22 Int)


; this works
; cross([in11], [in21, in22]) = ([in11, in21], [in11, in22])
(push)
(assert (= in1 (cons in11 (as nil (MyList Int)))))
(assert (= in2 (cons in21 (cons in22 (as nil (MyList Int))))))

(assert (not (= (cross in1 in2) (cons (pair in11 in21) (cons (pair in11 in22)                               
                                                            (as nil (MyList (Pair Int))))))))
(check-sat) (pop)

; but this doesn't work
; cross([in11, in12], [in21, in22]) = ([in11, in21], [in11, in22], [in12, in21], [in12, in22])
(push)
(assert (= in1 (cons in11 (cons in22 (as nil (MyList Int))))))
(assert (= in2 (cons in21 (cons in22 (as nil (MyList Int))))))

(assert (not (= (cross in1 in2) (cons (pair in11 in21) (cons (pair in11 in22)
                               (cons (pair in12 in21) (cons (pair in12 in22)
                                                            (as nil (MyList (Pair Int))))))))))
(check-sat) (pop)

Answer 1

在 SMT 求解器的上下文中谈论“最大递归界限”确实是不正确的。我可以看出您倾向于这样称呼它；正如您所希望的那样，它会尽可能多地展开定义。但这根本不是 SMT 求解器的工作原理。

一般来说，当你有一个递归函数时，它会引发一组量化的公理。 （您可以在http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 63 页找到翻译。）因此，您可能将其视为“函数”实际上是编写一堆量化公理的简写。

请注意，您也有自己的量化公理，所有这些约束结合在一起，求解器开始工作。不幸的是，这使得逻辑半可判定。意味着没有决策程序。 （决策过程总是终止并正确回答。）理论上，这意味着如果它最终存在，它总是可以找到一个“证明”，但如果某些事情不正确，它可能会无限循环。但是，在实践中，这通常意味着它会在两种情况下循环足够长的时间，以至于您的耐心或计算机的内存将首先耗尽。

存在处理量词的算法（例如宏查找和电子匹配）。但这些都必然是不完整的，而且在我的经验中相当脆弱。您还可以尝试通过提供量词实例化模式来帮助 z3，请参见此处：https://rise4fun.com/z3/tutorialcontent/guide#h28。但该技术既不容易使用，也无法在实践中扩展。

长话短说，SMT 求解器不适合使用量词进行推理。递归定义意味着量化。它们的功能既有理论上的限制，也有关于可用性、性能和诚实的投资回报的实际考虑：如果你想推理递归函数和递归数据类型，SMT 求解器可以说是不正确的工具。相反，使用 HOL、Isabelle、Coq、Agda、Lean 等定理证明器；等，它们旨在与此类结构一起使用。 （这些工具中的大多数可以自动代表您调用 SMT 求解器以实现简化目标；因此您可以两全其美。）

我希望这个解释是清楚的。经验法则是递归函数的推理需要归纳，而归纳证明需要发明必要的不变量。 SMT 求解器无法为您提供所需的不变量，即使您愿意提供它们，它们也不允许您指定这些不变量是什么。但是定理证明器可以帮助您陈述和证明这些不变量；并且应该是此类问题的首选。