function - 替换 lisp 中的元素

Question

我在 Common Lisp 中遇到这个问题。 我需要操纵存在变量，引入 skolemization 规则。

例如，我需要构建一个函数，该函数将 (exist ?x (p ?x))在(p sk00042) .

sk00042是一个变量。请注意，当涉及通用变量时，此函数会变得有点困难。

例如，给定表达式 (forall ?y (exist ?x (p ?x ?y)) 的函数将其变成(forall ?y (p (sf666 ?y) ?y) 。 这个想法是，存在变量告诉我有一些东西满足公式。如果这个存在量词是outer，那么这个量词不依赖于任何东西并且变量?x上面第一个示例中的内容应替换为常量 skoo42这是由这个函数生成的: (defun skolem-variable () (gentemp "SV-")) .

如果发生更困难的(第二种)情况，并且存在一个存在性量词“之外”的全称量词，那么存在的东西取决于全称量化的变量，这意味着该函数必须处理这种依赖性和全称变量合并到常量中，如示例所示:

(forall ?y (exist ?x (p ?x ?y)) ---->(forall ?y (p (sf666 ?y) ?y) 为此还具有以下功能:

(defun skolem-function* (&rest args) (cons (gentemp "SF-") args))
(defun skolem-function (args) (apply #'skolem-function* args))

这里有一些例子可以让您更熟悉这个想法:

(skolemize '(forall ?y (exist ?x (p ?x ?y))))
;=> (forall ?y (P (SF-1 ?Y) ?Y))
(skolemize '(exist ?y (forall ?x (p ?x ?y))))
;=> (for all ?x (P ?X SV-2)
(skolemize '(exist ?y (and (p ?x) (f ?y))))
;=> (AND (P ?X) (F SV-4))
(skolemize '(forall ?x (exist ?y (and (p ?x) (f ?y)))))
;=> (forall ?x (AND (P ?X) (F (SF-5 ?X)))

我需要构建给定的函数(使用上面的skolem-variable和skolem-function) 表达式控制外部是否存在，然后用 skolem-variable 替换该变量。如果外部是一个 forall 后跟并存在，则该函数将执行我上面解释的操作。

Answer 1

我刚刚浏览了关于 skolem 范式的维基百科文章，但如果我理解正确，每个存在式都会变成一个 skolem 函数调用，以绑定(bind)的通用项作为参数(如果范围内没有通用项，则为 skolem 常量)。一种简单的方法是在递归地遍历表达式树时拥有一堆绑定(bind)通用项:

(defun skolemize (form &optional (universals nil))
  (cond ((null form) nil)                                  ; subtree done
        ((consp (car form))                                ; walk branches
         (cons (skolemize (car form) universals)
               (skolemize (cdr form) universals)))
        ((eq (car form) 'forall)                           ; universal binding
         (list 'forall
               (cadr form)
               (skolemize (caddr form)                     ; skolemize body
                          (cons (cadr form) universals)))) ; new var on the stack
        ((eq (car form) 'exist)                            ; existential binding
         (subst (if universals                             ; substitute variables
                    (cons (gentemp "SF-") universals)      ; with skolem function
                    (gentemp "SV-"))                       ; with skolem constant
                (cadr form)
                (skolemize (caddr form) universals)))
        (t (cons (car form) (skolemize (cdr form) universals)))))

请注意，这只是为了让您开始 - 我既没有深入研究这个主题，也没有真正针对性能或优雅进行测试或优化。此外，它还会接受格式错误的输入，例如(skolemize '(forall (foo bar)))。

你的例子:

CL-USER> (skolemize '(exist ?x (p ?x)))
(P SV-16)
CL-USER> (skolemize '(forall ?y (exist ?x (p ?x ?y))))
(FORALL ?Y (P (SF-17 ?Y) ?Y))
CL-USER> (skolemize '(exist ?y (forall ?x (p ?x ?y))))
(FORALL ?X (P ?X SV-18))
CL-USER> (skolemize '(exist ?y (and (p ?x) (f ?y))))
(AND (P ?X) (F SV-19))
CL-USER> (skolemize '(forall ?x (exist ?y (and (p ?x) (f ?y)))))
(FORALL ?X (AND (P ?X) (F (SF-20 ?X))))

测试更复杂的表达式:

CL-USER> (skolemize '(exist ?a
                      (forall ?b
                       (exist ?c
                        (forall ?d
                         (exist ?e (and (or (and (f ?a) (g ?b))
                                            (and (f ?c) (g ?d)))
                                        (or (and (f ?c) (g ?e))
                                            (and (f ?d) (g ?e))))))))))
(FORALL ?B
  (FORALL ?D (AND (OR (AND (F SV-15) (G ?B))
                      (AND (F (SF-16 ?B)) (G ?D)))
                  (OR (AND (F (SF-16 ?B)) (G (SF-17 ?D ?B)))
                      (AND (F ?D) (G (SF-17 ?D ?B)))))))