2

受早期问题的启发，我尝试实现一些可以枚举布尔表达式的可能性的东西。但是，我在选择变量时遇到了麻烦。这是我的预期结果：

?- eval(X^Y, R).
R = 0^0;
R = 0^1;
R = 1^0;
R = 1^1;
no.

这是我的代码：

:- op(200, yfx, ^).

split(V, R) :- var(V), R = 0.
split(V, R) :- var(V), R = 1.
split(X ^ Y, XP ^ YP) :- split(X, XP), split(Y, YP).

即使对于这个简单的案例，这也不能满足我的要求：

?- split(Y, R).
R = 0 ;
R = 1 ;
Y = _G269^_G270,
R = 0^0 ;
Y = _G269^_G270,
R = 0^1 ;
Y = _G269^ (_G275^_G276),
R = 0^ (0^0) ;
Y = _G269^ (_G275^_G276),
R = 0^ (0^1) ;
Y = _G269^ (_G275^ (_G281^_G282)),
R = 0^ (0^ (0^0)) .

所以，我可以看到问题出在哪里，即在通过split(Y, YP)Prolog 的过程中已经用尽了前两个子句，所以它再次结束，基本上split(X^Y, ...)统一了 myY和。X'^Y'我只是不确定我需要做什么来关闭这条路径，除非我一开始就有结构^/2。

我也希望它可以与嵌套结构一起使用，所以我不能仅仅消除分支的递归处理。

编辑：没有运营商

如果op/3困扰您，请考虑以下公式：

eval(and(X,Y), R).
R = and(0,0);
R = and(0,1);
R = and(1,0);
R = and(1,1);
no.

这将是这种情况下的代码：

split(V, R) :- var(V), R = 0.
split(V, R) :- var(V), R = 1.
split(and(X,Y), and(XP,YP)) :- split(X, XP), split(Y, YP).

请记住，我仍然希望它可以与诸如此类的递归公式一起使用and(and(X,Y),and(Y,Z))。

4

3 回答 3

6

主要问题：默认表示

这种情况下的核心问题是您用来表示布尔表达式的默认表示。

“默认”是指您无法通过模式匹配清楚地区分情况：在您的情况下，变量V可能表示

  • 命题常数之一0和 1,或
  • 形式的复合表达式A^B。

由于这个缺点，您无法在程序中清晰地表达“变量X仅代表两个命题常数之一”形式的约束。

出路：干净的代表

一个声明性的出路是使用一个干净的表示 来代替。

例如，假设我们任意使用v/1来区分仅表示命题常数的变量，那么我们有：

  • v(X)表示命题变量X
  • A^B表示复合表达式。

显然，由于主要函子和元数不同（v/1vs. (^)/2），我们可以仅通过模式匹配来区分这些情况。

使用这种新的表示形式，您的代码段将变为：

分裂（v（V），V）：- V = 0。
分裂（v（V），V）：- V = 1。
拆分（X^Y，XP ^ YP）：-
        分裂（X，XP），
        分裂（Y，YP）。

示例查询：

?- 分裂(v(X)^v(Y), R)。
X = Y，Y = 0，
R = 0^0 ;
X = 0,
Y = 1,
R = 0^1 ;
X = 1,
Y = 0,
R = 1^0 ;
X = Y，Y = 1，
R = 1^1。

请注意，这仍然适用于所有方向，在最一般的情况下也是如此：

?-拆分（Expr，R）。
Expr = v(0),
R = 0 ;
Expr = v(1),
R = 1;
表达式 = v(0)^v(0),
R = 0^0 ;
表达式 = v(0)^v(1),
R = 0^1 ;
等等

根据经验，一旦你不得不var/1在代码中使用额外的逻辑谓词，就几乎没有希望保持其逻辑纯度和单调性。旨在使用干净的表示来保留这些属性。

有时，使用默认表示是不可避免的，例如，因为您想让用户更容易输入。在这种情况下，目标是在开始实际推理之前快速将它们转换为干净的。

于 2017-01-12T20:43:03.970 回答
3

在某个时间点，我编写了一个非常小的程序，似乎或多或少是您正在寻找的。我真的希望我没有完全误解你的问题。您可以查看此 SWISH 程序以了解整个程序。有一些区别，例如使用fandt代替 0 和 1，或使用andandor代替^and v。但是，基本思想与您的相同（我认为）。

如果我删除一些不必要的东西进行演示，那么这将是程序：

:- op(100, fy, ?).
:- op(500, yfx, and).
:- op(500, yfx, or).

table(F, T) :-
        term_variables(F, Vs),
        bagof(R-Vs, bl(F, R), T).

bl(?X, R) :-
        v(X, R).
bl(X and Y, R) :-
        bl(X, R0),
        and_bl(R0, Y, R).
bl(X or Y, R) :-
        bl(X, R0),
        or_bl(R0, Y, R).

v(f, f).
v(t, t).

and_bl(f, _, f).
and_bl(t, Y, R) :- bl(Y, R).

or_bl(f, Y, R) :- bl(Y, R).
or_bl(t, _, t).

这里的要点是我有一个纯关系 my v/2，它简单地说明trueis 的值和 is的true值。然后，我使用相互递归的定义来实际评估布尔表达式，最终在.falsefalsev/2

我决定自己“标记”布尔变量，因此X您必须编写?X. 如果我没记错的话，当时我意识到我需要一种方法来明确说明表达式中是否有布尔变量，或者整个表达式是否仍然“未知”。换句话说， this: ?Xis either tor fand this: Exprcan be ?X, or not ?X, or ?X and ?Y, or ?X or ?Y, or not (?X and ?Y), 等等。

用标记变量?X是避免“默认表示”是@mat解释的。重要的是，如果没有显式标记，我看不到将布尔变量与布尔表达式区分开来的方法。

以下是如何使用它：

?- bl(?t and ?X, R).
X = R, R = f ;
X = R, R = t.

?- bl(?t or ?X, R).
R = t.

?- bl(?A or (?B and ?C), R).
A = B, B = R, R = f ;
A = C, C = R, R = f,
B = t ;
A = f,
B = C, C = R, R = t ;
A = R, R = t.

?- table(?A or (?B and ?A), R).
R = [f-[f, f], f-[f, t], t-[t, _7734]].
于 2017-01-12T20:47:34.190 回答
3

已经有两个很好的答案，一个是纯的，另一个是使用term_variables/2. 我还是想讲一个细节：

所以，我可以看到问题出在哪里，即在通过split(Y, YP)Prolog 的过程中已经用尽了前两个子句，所以它再次结束，基本上split(X^Y, ...)统一了 myY和。X'^Y'我只是不确定我需要做什么来关闭这条路径，除非我一开始就有结构^/2。

如果您不想X^Y在第一个参数是变量的情况下执行头部统一，请将统一从头部中拉出来。没有什么能强迫你把这个词放在X^Y那里！如果前两个条款不适用，您要做的是仅考虑您的最后一个条款。前两个子句由 保护var/1，因此您可以用 保护最后一个子句nonvar/1：

split(V, R) :- var(V), R = 0.
split(V, R) :- var(V), R = 1.
split(Term, SplitTerm) :-
    nonvar(Term),
    Term = X ^ Y,
    split(X, XP),
    split(Y, YP),
    SplitTerm = XP ^ YP.

有了这个，您的示例按预期工作：

?- split(Y, R).
R = 0 ;
R = 1 ;
false.

?- split(X^Y, R).
R = 0^0 ;
R = 0^1 ;
R = 1^0 ;
R = 1^1 ;
false.

编辑：正如 mat 在评论中指出的那样，使用类似的测试var/1会给你带来各种各样的麻烦。

一个问题是，您必须仔细检查各种级别的实例化：mat 的示例查询split(1, R)失败，上面的代码（它应该成功R = 1）。这是因为1落入nonvar案件但不与 统一_^_。如果我们要这样做，我们不仅要区分varandnonvar情况，还要区分var,ground和nonvar-but-not- ground。这有点混乱。

另一个问题是查询split(V, R), V = 1，它在声明上等同于上面的查询，但成功了两次，包括解决方案R = V。这是因为split/2（故意）的这种定义避免在其论点之间引入共享。我们是否想要共享取决于规范。

我不会尝试通过实例化测试给出一个完全健壮的解决方案，因为我的观点不是这是最好的方法。

于 2017-01-12T20:59:26.460 回答