2

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

例如，我需要构建一个函数，它会 (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-"))。

如果发生更难的（第二种）情况并且存在一个通用量词“超出”存在性量词，那么存在的事物依赖于普遍量化的变量，这意味着函数必须处理这种依赖性并且通用变量被合并到常数，如示例中所示：

(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-variable 替换变量。skolem-function如果外部是一个 forall 并且存在，则该函数执行我上面解释的操作。

4

1 回答 1

2

我刚刚浏览了关于 skolem 范式的 Wikipedia 文章，但是如果我做对了，每个存在都将成为一个 skolem 函数调用，其中绑定的普遍性作为参数（或者如果没有普遍性在范围内，则为 skolem 常数）。一种简单的方法是在递归地遍历表达式树时拥有一堆绑定的universal：

(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)))))))
于 2013-02-10T19:13:26.893 回答