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

Question

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

\n\n

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

\n\n

Z与负范式公式统一。

\n\n

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

\n\n

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

\n\n

?- rewrite(e(4, 7), e(4, 7)).\ntrue.\n

\n\n

我尝试rewrite(A, A).用受保护的版本替换：

\n\n

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

\n\n

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

\n\n

?- rewrite(4, Z).\nZ = 4.\n\n?- rewrite(c(4, 7), Z).\nfalse.\n

\n\n

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

\n\n

\xe2\x9c\xb1 程序全文供参考：

\n\n

% so the primitive connectives are\n% l <-- necessity\n% m <-- possibility\n% c <-- implication\n% f <-- falsehood\n% t <-- truth\n% k <-- conjunction\n% a <-- alternative\n% n <-- negation\n% e <-- biconditional\n\nwff_shallowly(WFF) :-\n  WFF = l(_);\n  WFF = m(_);\n  WFF = c(_, _);\n  WFF = f;\n  WFF = t;\n  WFF = k(_, _);\n  WFF = a(_, _);\n  WFF = n(_);\n  WFF = e(_, _).\n\n% falsehood is primitive\nrewrite(f, f).\n\n% truth is primitive\nrewrite(t, t).\n\n% positive connectives\nrewrite(a(A, B), a(C, D)) :- rewrite(A, C), rewrite(B, D).\nrewrite(k(A, B), k(C, D)) :- rewrite(A, C), rewrite(B, D).\nrewrite(l(A), l(C)) :- rewrite(A, C).\nrewrite(m(A), m(C)) :- rewrite(A, C).\n\n% implication\nrewrite(c(A, B), a(NC, D)) :-\n  rewrite(n(A), NC), rewrite(B, D).\n\n% biconditional\nrewrite(e(A, B), a(k(C, D), k(NC, ND))) :-\n  rewrite(A, C),\n  rewrite(n(A), NC),\n  rewrite(B, D),\n  rewrite(n(B), ND).\n\n% negated falsehood is truth\nrewrite(n(f), t).\n\n% negated truth is falsehood\nrewrite(n(t), f).\n\n% double negation elimination\nrewrite(n(n(A)), C) :- rewrite(A, C).\n\n% negated alternation\nrewrite(n(a(A, B)), k(NC, ND)) :-\n  rewrite(n(A), NC), rewrite(n(B), ND).\n\n% negated conjunction\nrewrite(n(k(A, B)), a(NC, ND)) :-\n  rewrite(n(A), NC), rewrite(n(B), ND).\n\n% negated biconditional\nrewrite(n(e(A, B)), a(k(C, ND), k(NC, D))) :-\n  rewrite(A, C),\n  rewrite(n(A), NC),\n  rewrite(B, D),\n  rewrite(n(B), ND).\n\n% negated necessity\nrewrite(n(l(A)), m(NC)) :- rewrite(n(A), NC).\n\n% negated possibility\nrewrite(n(m(A)), l(NC)) :- rewrite(n(A), NC).\n\n% catch all, rewrite to self\nrewrite(A, A) :- \\+ wff_shallowly(A).\n

\n

Answer 1

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

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

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

我添加了以下子句来说明模态变量的含义，而不是“捕获所有”子句：

%（否定）变量

重写（n（v（V）），n（v（V）））。
重写(v(V), v(V))。

现在我们得到：

?- 重写(e(v(4), v(7)), Z)。
Z = a(k(v(4), v(7)), k(n(v(4)), n(v(7))))。

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

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

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