prolog 捕获仅在没有其他子句时才处于事件状态的所有子句

Question

我有一个谓词，将模态逻辑公式与其负范式联系起来。除了模态运算符、合取和析取之外的所有连接词都被消除，并且否定被尽可能地插入表达式的叶子中。

rewrite/2 ✱ 谓词有一个包罗万象的子句 rewrite(A, A).这是文本上的最后。有了这个包罗万象的子句，就可以提取否定范式的公式。在此示例中，e是一个双条件连接词，如 Łukasiewicz 表示法，并且 4和7是模态逻辑中的变量(因此也是 Prolog 常量)。

Z与负范式公式统一。

?- rewrite(e(4, 7), Z).
Z = a(k(4, 7), k(n(4), n(7)))

但是，rewrite(<some constant>, <some constant>)总是成功，但我希望它不要成功。包罗万象的子句确实应该是包罗万象的，而不是如果另一个子句适用则可能会触发的东西。

?- rewrite(e(4, 7), e(4, 7)).
true.

我尝试替换 rewrite(A, A).使用 protected 版本:

wff_shallowly(WFF) :-
  WFF = l(_);
  WFF = m(_);
  WFF = c(_, _);
  WFF = f;
  WFF = t;
  WFF = k(_, _);
  WFF = a(_, _);
  WFF = n(_);
  WFF = e(_, _).

rewrite(A, A) :- \+ wff_shallowly(A).

我认为这会阻止包罗万象的子句适用当且仅当 A 不是由具有特殊含义的原子/构造函数开头。但是，进行更改后，rewrite如果递归调用总是失败。

?- rewrite(4, Z).
Z = 4.

?- rewrite(c(4, 7), Z).
false.

设置 catch all 子句的正确方法是什么。

✱节目全文供引用:

% so the primitive connectives are
% l <-- necessity
% m <-- possibility
% c <-- implication
% f <-- falsehood
% t <-- truth
% k <-- conjunction
% a <-- alternative
% n <-- negation
% e <-- biconditional

wff_shallowly(WFF) :-
  WFF = l(_);
  WFF = m(_);
  WFF = c(_, _);
  WFF = f;
  WFF = t;
  WFF = k(_, _);
  WFF = a(_, _);
  WFF = n(_);
  WFF = e(_, _).

% falsehood is primitive
rewrite(f, f).

% truth is primitive
rewrite(t, t).

% positive connectives
rewrite(a(A, B), a(C, D)) :- rewrite(A, C), rewrite(B, D).
rewrite(k(A, B), k(C, D)) :- rewrite(A, C), rewrite(B, D).
rewrite(l(A), l(C)) :- rewrite(A, C).
rewrite(m(A), m(C)) :- rewrite(A, C).

% implication
rewrite(c(A, B), a(NC, D)) :-
  rewrite(n(A), NC), rewrite(B, D).

% biconditional
rewrite(e(A, B), a(k(C, D), k(NC, ND))) :-
  rewrite(A, C),
  rewrite(n(A), NC),
  rewrite(B, D),
  rewrite(n(B), ND).

% negated falsehood is truth
rewrite(n(f), t).

% negated truth is falsehood
rewrite(n(t), f).

% double negation elimination
rewrite(n(n(A)), C) :- rewrite(A, C).

% negated alternation
rewrite(n(a(A, B)), k(NC, ND)) :-
  rewrite(n(A), NC), rewrite(n(B), ND).

% negated conjunction
rewrite(n(k(A, B)), a(NC, ND)) :-
  rewrite(n(A), NC), rewrite(n(B), ND).

% negated biconditional
rewrite(n(e(A, B)), a(k(C, ND), k(NC, D))) :-
  rewrite(A, C),
  rewrite(n(A), NC),
  rewrite(B, D),
  rewrite(n(B), ND).

% negated necessity
rewrite(n(l(A)), m(NC)) :- rewrite(n(A), NC).

% negated possibility
rewrite(n(m(A)), l(NC)) :- rewrite(n(A), NC).

% catch all, rewrite to self
rewrite(A, A) :- \+ wff_shallowly(A).

Answer 1

如果您使用干净的数据表示方式，这些问题都会消失。

在这种情况下，这意味着您应该完全类似于如何通过不同的仿函数系统地表示所有其他实体，也使用专用仿函数来表示(模态)变量.

例如，让我们使用仿函数v/1来表示变量。这意味着我们使用 v(1)、v(7) 等来表示模态变量 1、7 等。

我添加了以下子句来说明模态变量的含义，而不是“catch all”子句:

% (negated) variablerewrite(n(v(V)), n(v(V))).rewrite(v(V), v(V)).

现在我们得到:

?- rewrite(e(v(4), v(7)), Z).Z = a(k(v(4), v(7)), k(n(v(4)), n(v(7)))).

请注意，我们当然必须在查询中使用 v/1 包装器，并在答案中获取包装器。与不存在包装器相比，这稍微难以读取和写入。然而，它使得对此类公式的推理变得更加容易，因此我强烈建议使用它。

在此类公式和您当前使用的默认表示形式之间进行转换是一个简单的练习。它被称为“defaulty”正是因为它需要一个default(“catch all”)情况，而且还因为它被认为有缺陷。最好尽快摆脱此类表示，然后围绕干净的表示编写主要逻辑。

干净的表示有利于通用性，也有利于效率:Prolog 系统的参数索引现在可以通过第一个参数的主仿函数轻松区分所有子句，这提高了该参数被完全实例化的重要用例(例如，在您发布的示例中)。