0

我需要尝试展示一个找到列表最小值的函数，我觉得我快要得到它但实际上无法得到它。

导师给了我们这个功能：

(defun minlist (l)
  (if (<= (len l) 1)
    (first l)
    (if (<= (first l) (minlist (rest l)))
      (first l)
      (minlist (rest l)))))

然后说

;;; TODO: Write a little theory that verifies that the minlist of a list is 
;;; less than or equal to any element of the list
;;; Hint: Use this declaration to generate a non-empty list
;;;  (n :value (random-between 1 10)
;;;   l :value (random-natural-list-of-length n))

然后我做了：

(defproperty-program minlist-<=-member (n)
    (if ((n :value (random-between 1 10) 
          l :value (random-natural-list-of-length n)))
          (<= (min-list l) (first l))
          (nil)))

Proof Pad 中的哪个给了我一个错误，我无法弄清楚我做错了什么。

错误是：

硬 ACL2 错误：缺少 N 的 :value 参数

TOP-LEVEL 中的 ACL2 错误：尝试对表单进行宏扩展

(EXPAND-VARS (N)
             (IF ((N :VALUE (RANDOM-BETWEEN 1 10)
                     L
                     :VALUE (RANDOM-NATURAL-LIST-OF-LENGTH N)))
                 (<= (MIN-LIST L) (FIRST L))
                 (NIL))),

宏体的评估导致以下错误：

评估中止。要调试，请参见 :DOC print-gv，参见 :DOC 跟踪，并参见 :DOC wet。

4

1 回答 1

1

如果这篇文章来得太晚了，我很抱歉。

因此，我看到您拥有的 defproperty 存在一些“结构”问题，一个是您调用 min-list (<= (MIN-LIST L)，但定义的函数是 minlist 没有破折号。此外，该部分 (n :value (random-between 1 10) l :value (random-natural-list-of-length n))

构造要使用的列表，并且根本不应该在 if 语句中。它应该在它之上。此外，该语句声明了 n 值，并且您不需要 (n) 您拥有的值。在这些更改之后，您最终得到

   (defproperty-program minlist-<=-member
(n :value (random-between 1 10) 
          l :value (random-natural-list-of-length n))
    (if (<= (minlist l) (first l))
          (nil)))

但这会使您的 if 语句没有足够的参数。此外，您拥有的语句 '(<= (minlist l) (first l))' 仅检查列表的第一个元素是否小于或等于 minlist 元素。这并不能证明它比可能存在的其他元素小。

我希望这有帮助。

于 2019-03-07T22:15:54.280 回答