表示受限域的唯一性

Question

给定一些函数：

define foo(x,y) (x > y) end.
define bar(x) (foo x x) end.
define baz(x,y) (foo x y) end.

我对函数获取/返回的确切值不感兴趣，但是我想知道输入的符号如何影响输出。

为了模拟大于函数，我使用原子zero_int，它被解释为0，pos_int，它被解释为所有大于0的整数，neg_int被解释为所有小于@987654327的整数@。

%% pos_int greater then ...
%% i.e forall n,m : (n > 0) & (m = 0) => n is_greater_than m
gt(pos_int,zero_int,true).
gt(pos_int,neg_int,true).
gt(pos_int, pos_int, X) :- boolean(X). % return either true or false.
%% zero greater than ...
gt(zero_int, pos_int, false).
gt(zero_int,zero_int,false).
gt(zero_int, neg_int, true).
%% neg int greater than...
gt(neg_int, pos_int, false).
gt(neg_int, zero_int, false).
gt(neg_int, neg_int, X) :- boolean(X).

boolean/1 谓词用于在有选择点时返回true 或false。即比较n > m，其中n > 0 和m > 0 可能为真或假。由于我们不知道n 和m 的实际（整数）值，因此假设这两种情况都是正确的。

%% define booleans
boolean(true).
boolean(false).

现在我按以下方式对函数进行编码：

foo(X,Y,Return) :- gt(X,Y,Return).
bar(X,Return) :- foo(X,X,Return).
baz(X,Y,Return) :- foo(X,Y,Return).

测试foo（和baz）我们得到了预期的结果：

?- foo(X,Y,Return).
X = pos_int,
Y = zero_int,
Return = true ;
X = pos_int,
Y = neg_int,
Return = true ;
X = Y, Y = pos_int,
Return = true ;
X = Y, Y = pos_int,
Return = false ;
X = zero_int,
Y = pos_int,
Return = false ;
...

我的问题是，因为 bar 调用 gt 时只有一个值 - 我希望它始终返回 false，因为它永远不会像 n > n 那样返回

?- bar(X,Return).
X = pos_int,
Return = true ;
X = pos_int,
Return = false ;
X = zero_int,
Return = false ;
X = neg_int,
Return = true ;
X = neg_int,
Return = false.

我对如何编码很感兴趣。我已经探索过使用成对的变量作为输入，以允许可以比较的 labels。

Answer 1

你可以试试

boolean(true).
boolean(false).

gt2((_, pos_int), (_, zero_int), (_,true)).
gt2((_, pos_int), (_, neg_int),  (_,true)).
gt2((L1, pos_int), (L2, pos_int), (_,X)) :- not(L1 == L2), boolean(X).
%% zero greater than ...
gt2((_, zero_int), (_, pos_int),  (_,false)).
gt2((_, zero_int), (_, zero_int), (_,false)).
gt2((_, zero_int), (_, neg_int),  (_,true)).
%% neg int greater than...
gt2((_, neg_int), (_, pos_int), (_,false)).
gt2((_, neg_int), (_, zero_int), (_,false)).
gt2((L1, neg_int), (L2, neg_int), (_,X)) :- not(L1 == L2), boolean(X).

gt2((L,pos_int),(L,pos_int),(_,false)).
gt2((L,neg_int),(L,neg_int),(_,false)).

foo(X,Y,Return) :- gt2(X,Y,Return).
bar(X,Return) :- foo(X,X,Return).
baz(X,Y,Return) :- foo(X,Y,Return).

这使用了 labels 的思想，它允许我们对输入进行标记，这样我们就可以对相等性进行编码。基本上，如果标签匹配，则输入严格相等。 （即给定两个正整数集合内的输入，如果它们具有相同的标签，那么它们是相同的整数。 这将给出结果：

?- bar(X,R).
X =  (_31408, zero_int),
R =  (_31414, false) ;
X =  (_31408, pos_int),
R =  (_31414, false) ;
X =  (_31408, neg_int),
R =  (_31414, false).

?- foo(X,Y,R).
X =  (_31852, pos_int),
Y =  (_31858, zero_int),
R =  (_31864, true) ;
X =  (_31852, pos_int),
Y =  (_31858, neg_int),
R =  (_31864, true) ;
X =  (_31852, pos_int),
Y =  (_31858, pos_int),
R =  (_31864, true) ;
X =  (_31852, pos_int),
Y =  (_31858, pos_int),
R =  (_31864, false) ;
X =  (_31852, zero_int),
Y =  (_31858, pos_int),
R =  (_31864, false) ;
X =  (_31852, zero_int),
Y =  (_31858, zero_int),
R =  (_31864, false) ;
X =  (_31852, zero_int),
Y =  (_31858, neg_int),
R =  (_31864, true) ;
X =  (_31852, neg_int),
Y =  (_31858, pos_int),
R =  (_31864, false) ;
X =  (_31852, neg_int),
Y =  (_31858, zero_int),
R =  (_31864, false) ;
X =  (_31852, neg_int),
Y =  (_31858, neg_int),
R =  (_31864, true) ;
X =  (_31852, neg_int),
Y =  (_31858, neg_int),
R =  (_31864, false) ;
X = Y, Y =  (_31852, pos_int),
R =  (_31864, false) ;
X = Y, Y =  (_31852, neg_int),
R =  (_31864, false).

注意foo 会在 标签 相同时生成额外的输入。