ProofPad中ACL2二叉搜索树验证函数实现问题求助

问题背景 #

课堂作业中使用Web版ACL2 IDE（ProofPad），需实现search-treep函数验证二叉搜索树有效性，已提供预设函数tree-max和tree-min：

预设函数代码 #

;;; BEGIN boilerplate code -- ignore :-)

(in-package "ACL2")

(include-book "testing" :dir :teachpacks)
(include-book "doublecheck" :dir :teachpacks)
(include-book "arithmetic-5/top" :dir :system)

;;; END boilerplate code

(defun tree-max (tree)
   (if (consp tree)
       (if (consp (third tree))
           (if (consp (fourth tree))
               (max-<< (first tree)
                    (max-<< (tree-max (third tree)) 
                            (tree-max (fourth tree))))
               (max-<< (first tree)
                       (tree-max (third tree))))
           (if (consp (fourth tree))
               (max-<< (first tree)
                       (tree-max (fourth tree)))
               (first tree)))
       'MIN-SYMBOL))

;;; This function finds the minimum key in a tree

(defun tree-min (tree)
   (if (consp tree)
       (if (consp (third tree))
           (if (consp (fourth tree))
               (min-<< (first tree)
                       (min-<< (tree-min (third tree)) 
                               (tree-min (fourth tree))))
               (min-<< (first tree)
                       (tree-min (third tree))))
           (if (consp (fourth tree))
               (min-<< (first tree)
                       (tree-min (fourth tree)))
               (first tree)))
       'MAX-SYMBOL)
   )

search-treep函数要求 #

需满足以下全部条件之一：

1. 树为NIL；或
2. 树是包含4个元素（key value left right）的列表，且：
   • key是有效符号
   • value是有理数
   • 左子树为NIL，或左子树的max << 当前key
   • 右子树为NIL，或当前key << 右子树的min
   • 左子树是有效搜索树
   • 右子树是有效搜索树

现有实现及问题 #

用户初步实现代码如下：

;;; TODO-5: Implement this function using the strategy above.

(defun search-treep (tree)
   (if (consp tree) ;;if list or tree is non-0
      (if (= (LEN '(tree)) 4)
      (if (symbolp (first tree)) ;;if the first item in list or "key" is a symbol
         (if(rationalp (second tree)) ;;if the second item for value is a number
            (if(AND ;;if both
            (OR (= (third tree) nil) (tree-max (third tree))) ;;The left tree is NIL, OR the max of                         
            (OR (= (fourth tree) nil) (tree-min(fourth tree)))) ;;The right tree is NIL, OR the key 
               (if (search-treep (third tree)) ;he left tree is a valid search tree
                 (if (search-treep (fourth tree)) t ;The right tree is a valid search tree
                 nil)
               nil)
            nil)
        nil)
     nil)
     nil)      
  nil))

运行测试用例时均返回nil，不符合预期：

(check-expect (search-treep '(x 1 nil (z 3 (y 2 nil nil) nil))) t) ; 预期返回t
(check-expect (search-treep '(y 1 (z 3 (x 2 nil nil) nil) nil)) nil) ; 预期返回nil

问题分析 #

现有代码存在多处逻辑错误：

• 长度判断错误：(LEN '(tree))是计算符号tree组成的单元素列表长度，结果永远为1，应改为(len tree)
• 空值判断错误：ACL2中判断空列表需用(null tree)而非(= tree nil)
• 关键比较逻辑缺失：仅判断了左子树存在最大值、右子树存在最小值，但未实现左子树max << 当前key和当前key << 右子树min的核心比较
• 嵌套逻辑冗余：多层if嵌套导致逻辑混乱，可通过AND合并条件简化结构

修正后的代码 #

(defun search-treep (tree)
  (or (null tree)
      (and (consp tree)
           (= (len tree) 4)
           (symbolp (first tree))
           (rationalp (second tree))
           (or (null (third tree))
               (and (search-treep (third tree))
                    (max-<< (tree-max (third tree)) (first tree))))
           (or (null (fourth tree))
               (and (search-treep (fourth tree))
                    (max-<< (first tree) (tree-min (fourth tree))))))))

代码说明 #

• 用or直接处理树为NIL的情况
• 用and合并所有非NIL树的验证条件：
  1. 树是列表且长度为4
  2. key是符号、value是有理数
  3. 左子树为空，或左子树有效且其最大值小于当前key
  4. 右子树为空，或右子树有效且当前key小于右子树最小值

测试验证 #

运行原测试用例可得到正确结果：

• (search-treep '(x 1 nil (z 3 (y 2 nil nil) nil))) 返回t
• (search-treep '(y 1 (z 3 (x 2 nil nil) nil) nil)) 返回nil

内容的提问来源于stack exchange，提问作者inherownlittleworld