1

この方法で構築された整形式の論理積があるかどうかを判断する関数を構築する必要があります。

cong ::= '(' と wff 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述語であり、アトムでは機能しないようです。pthat satisfiesと述べたので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 に答える