function - 在Lisp中替换元素

我口齿不清有这个问题。
我需要操纵存在的变量，引入SkuleMe化规则。
例如，我需要构建一个函数
(exist ?x (p ?x))中的(p sk00042)。
sk00042是一个变量。请注意，当涉及通用变量时，此函数会变得有点困难。
例如，给定表达式(forall ?y (exist ?x (p ?x ?y))的函数将其转换为(forall ?y (p (sf666 ?y) ?y)。
这个想法是，存在变量告诉我有一些满足公式的东西。如果这个存在量词是外部的，那么这个量词不依赖于任何事物，并且在上面的第一个例子中的变量?x应该用这个函数生成的常量skoo42替换：
(defun skolem-variable () (gentemp "SV-"))。
如果更难（第二）的情况发生，并且存在一个通用量词“OUT”的存在，那么存在的东西取决于普遍量化的变量，这意味着函数必须处理这种依赖性，并且通用变量在常数中被合并，例如在示例中：
(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变量替换变量。如果外部是一个FALLL，然后存在，函数就做了我上面解释过的。

最佳答案

我只是略过了Skelm范式的维基百科文章，但是如果我得到了正确的结果，每个存在性就变成了一个Skelem函数调用，它被绑定的普遍性作为参数（或者如果没有通用性在一个范围内是一个Skelm常量）。一种简单的方法是在递归地遍历表达式树时拥有一堆绑定的通用表达式：

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

关于function - 在Lisp中替换元素，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/14799832/