替换lisp中的元素

Question

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

例如，我需要构建一个在(p sk00042)中转换(exist ?x (p ?x))的函数。

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，后面跟着and exist，这个函数会做我上面解释过的事情。

Answer 1

我刚刚浏览了维基百科上关于skolem范式的文章，但如果我没有弄错，每个存在词都会变成一个skolem函数调用，并将绑定的共性作为参数(如果作用域中没有共性，则为一个skolem常量)。一种简单的方法是在递归遍历表达式树时拥有一个绑定的通用堆栈：

(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)))))))