1

我必须构建一个函数来确定我是否有以这种方式构建的格式良好的公式的合取：

cong ::= '(' and wff wff ...')'

假设我有确定公式是否为 wff 的代码。该函数必须首先检查列表的第一个元素是否是'and ，然后递归地检查其余的子列表是否是 wff。请注意，这 p也是一个 wff，因此它不一定是子列表。

例子 ：(and (or a b v) (and a b d) m n)

这是我尝试过的对我不起作用的方法：

(defun cong (fbf)
    (and (eq (first fbf) 'and )
        (reduce (lambda (x y) (and x y))
            (mapcar #'wff (rest fbf)))))
4

1 回答 1

1

假设一个有效的wff谓词，您的代码将起作用。例如，numberp用作谓词：

(defun cong (fbf)
  (and (eq (first fbf) 'and)
       (reduce (lambda (x y) (and x y))
               (mapcar #'numberp (rest fbf)))))

工作正常：

CL-USER> (cong '(and 1 2 3 4 5))
T
CL-USER> (cong '(and 1 2 3 4 foo))
NIL
CL-USER> (cong '(1 2 3 4))
NIL

请注意，这可以更容易地完成：

(defun cong (fbf)
  (and (eq (first fbf) 'and)
       (every #'wff (cdr fbf))))

另外，请注意，在 CL 中，按照惯例，谓词通常应以p.

因此，鉴于您的上述评论，您的问题是wff谓词，它似乎不适用于原子。既然你提到了psatisfies wff，那个谓词是完全错误的，但是如果你必须使用它（假设这是某种家庭作业），只需检查手头的元素是否是一个缺点：

(defun cong (fbf)
  (and (eq (first fbf) 'and)
       (every #'wff (remove-if-not #'consp (cdr fbf)))))

这假设每个原子都满足wff。因此，它们不会改变连词的结果并且可以被删除。否则，您必须编写另一个谓词来检查原子是否满足wff，或者，这是正确的做法，wff首先要修复。

另外，请注意，这些都没有真正涉及递归，因为您只是在询问如何将谓词应用于列表并将结果结合起来。

于 2013-02-12T15:56:29.300 回答