Prolog定义正交条件

Question

我在Prolog魔法世界中很新，但它似乎非常有力地解决了我的问题。

我有两个基础[i0,j0,k0]和[i1,j1,k1]。然后在相同基的所有元素之间存在一个正交约束(i0与j0正交，j0与k0正交，k0与i0正交)。

我想找到一组新的正交约束，以便在第一个基和第二个基的元素之间添加一组新的正交约束，使两个基对齐/相等。然后，找到最小数量的约束可能会很有趣(当您考虑到这一点时，它似乎是3)。

我已经开始编写代码了(但是你可以给我一些技巧和技巧来获得更有效的代码)，但是当我需要表达我的问题的目标时，我就被困住了。

让我们定义ortho/1，这样列表中的所有元素都是互相正交的。然后我们就可以定义我们的两个基础：

ortho([i0,j0,k0]).
ortho([i1,j1,k1]).

然后，我添加以下规则从ortho([X,Y])谓词中推断出ortho([X,Y,Z])：

ortho(L) :- ortho(B), unique(L), unordered_subset(B,L).

这一点可以解释，因为我们需要找到一个现有的基础B，这样L是B的子列表，L的所有元素都是不同的。一些测试导致：

?- ortho([i0,j0]).
true.
?- ortho([k0,i0]).
true.
?- ortho([i0,i0]).
false.

下面是我在我的程序中使用的unique/1、subset/2和unordered_subset/2的实现(在StackOverflow上找到，不知道是否有更好的实现，但它似乎有效)。

% unique/1 detect list formed by unique elements
unique([]).
unique([X|Xs]) :- \+ memberchk(X, Xs), unique(Xs).

% subset/2 (set, subset) true if subset is a subset of set in the same order
subset([], []).
subset([E|Tail], [E|NTail]):-
    subset(Tail, NTail).
subset([_|Tail], NTail):-
    subset(Tail, NTail).

% unordered_subset/2 (set, subset) true if subset is a subset of set
unordered_subset(Set, SubSet):-
    length(Set, LSet),
    between(0,LSet, LSubSet),
    length(NSubSet, LSubSet),
    permutation(SubSet, NSubSet),
    subset(Set, NSubSet).

最后一个问题是看这两个基础是否相等。为此，我定义了equal/2和collin/2，以便：

% collin/2 check the collinearity of two vectors
collin(A,B) :-
    ortho([X,Y,A]), ortho([X,B]), ortho([Y,B]).

% equal/2 check basis equals
equal([],[]).
equal([H1|T1],[H2|T2]) :-
    collin(H1,H2),
    equal(T1,T2).

collin/2是基于两个向量A和B是共线的，如果存在X和Y，那么[X,Y,A]是基，X和Y都是与B正交的。equal/2是这样一个事实:如果取好的向量是共线的，那么两个基是相等的。(通过交换性，Prolog应该能够找到这个好的顺序)。

为了解决我的问题，我想找到一个长度为T的N对的列表，N尽可能低，这样对于T中的所有对P=X-Y，ortho(X,Y)都意味着equal([i0,j0,k0], [i1,j1,k1])。

你能帮我表达一下这条规则吗？(并最终获得更好的代码:)

Answer 1

您的unique/1只在列表已完全填充时才能工作--这违反了执行代码的“快速失败”原则。应该检查各个list元素是否实例化--这可以使用freeze来完成。

我看到的最正确的唯一定义是all_dif in https://stackoverflow.com/a/31724022/ (因为它在列表的尾部稍后被扩展时起作用)。

还可以在swi中使用此方法(性能折衷)：

% Very fast, due to memberchk written in C
% But requires that the list is populated in order
all_unique_memberchk_freeze([]).
all_unique_memberchk_freeze([H|T]) :-
    % Can only use the fast code if the list is closed
    is_list(T),
    !,
    all_unique_memberchk_freeze_(T, [H]).
all_unique_memberchk_freeze([H|T]) :-
    all_dif([H|T]).

all_unique_memberchk_freeze_([], _).
all_unique_memberchk_freeze_([H|T], SeenLst) :-
    freeze(H, \+ memberchk(H, SeenLst)),
    all_unique_memberchk_freeze_(T, [H|SeenLst]).