%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% topology, ultrafilter, simple games, and matorid
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 16-8, 19-20 Oct 2009; revised 7 Jan 2010
% ufilter.pl
% By Kenryo Indo

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Group (set theoretical) operations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% project_id/4: projection for social choice set/ coalition  
% cited: 16 Oct 2009 (scsr/4 in spcf09.pl)

project_id(0,[],[],[]).
project_id(J,[_|Y],[0|B],C):- project_id(J,Y,B,C).
project_id(K,[X|Y],[1|B],[X|C]):- project_id(J,Y,B,C), length(Y,I), K is J+ 2^I.

agents([1,2,3]).
agent(I):- agents(N), member(I,N).

group(Pid,P,C):- var(C),agents(N), project_id(Pid,N,P,C).
group(Pid,P,C):- \+ var(C),group(Pid,P,D),same_members(C,D).

all_groups(L):- findall(I,group(I,_,_),L).

is_complement_of( A, B):-
   group(A,P,_),project_reverse(P,Q),group(B,Q,_).

project_reverse([],[]).
project_reverse([X|B],[Y|C]):-
   project_reverse(B,C),
   digit_reverse(X,Y).
digit_reverse(1,0).
digit_reverse(0,1).


/*

?- group(I,K,P),writeln(I;K;P),fail.
0;[0, 0, 0];[]
1;[0, 0, 1];[3]
2;[0, 1, 0];[2]
3;[0, 1, 1];[2, 3]
4;[1, 0, 0];[1]
5;[1, 0, 1];[1, 3]
6;[1, 1, 0];[1, 2]
7;[1, 1, 1];[1, 2, 3]
false.

?- group(A,_,B),is_complement_of(C,A),group(C,_,D),writeln(A:B-C:D),fail.
0:[]-7:[1, 2, 3]
1:[3]-6:[1, 2]
2:[2]-5:[1, 3]
3:[2, 3]-4:[1]
4:[1]-3:[2, 3]
5:[1, 3]-2:[2]
6:[1, 2]-1:[3]
7:[1, 2, 3]-0:[]

*/



same_members(X,Y):-
   subtract(X,Y, []), subtract(Y,X, []).

is_a_union_of_groups(X,[Y,Z],T):-
   member(Y, T), group(Y,_,C),
   member(Z, T), group(Z,_,D),
   union(C,D,W), same_members(W,V), group(X,_,V).

is_an_intersection_of_groups(X,[Y,Z],T):-
   member(Y, T), group(Y,_,C),
   member(Z, T), group(Z,_,D),
   intersection(C,D,W), same_members(W,V), group(X,_,V).

intersection_in_list([M], M).
intersection_in_list([C|L], M1):-
   intersection_in_list(L, M),
   intersection(M, C, M1).

has_a_supergroup(X,Y,T):-
   group(X,_,C),
   member(Y,T), group(Y,_,D), D\=[],
   subset(C,D).

has_a_subgroup(X,Y,T):-
   group(X,_,C),
   member(Y,T), group(Y,_,D), D\=[],
   subset(D,C).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Topology
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

topology(Tid, T):-
   all_groups(L),
   reverse(L,R),
   topology_id(Tid,R,_,T),
   Tid \= 0.

topology_id(0,[],[],[]).
topology_id(J,[X|Y],[0|B],C):-
   topology_id(J,Y,B,C),
   \+ topology_axiom(add_if, X,C).
topology_id(K,[X|Y],[1|B],[X|C]):-
   topology_id(J,Y,B,C),
   \+ topology_axiom(remove_if, X,C),
   length(Y,I), K is J+ 2^I.

topology_axiom(add_if, X,_):- group(X,_,[]).
topology_axiom(add_if, X,_):- agents(N), group(X,_,N).
topology_axiom(remove_if, X,T):- has_an_empty_intersection(X,_,T).
topology_axiom(add_if, X,T):- is_a_union_of_groups(X,_,T).

has_an_empty_intersection(X,S,T):-
   group(X,_,C),C \= [], 
   is_a_collection_of_groups(S,L, T),
   subtract(L,[[]],U),
   intersection_in_list([C|U],[]).

is_a_collection_of_groups(S,L, T):-
   project_id(_,T,_,S),
   findall( C,(member(I,S),group(I,_,C)),L).



/*

?- all_groups(L),is_a_collection_of_groups(S,O,L),intersection_in_list(O,M),M\=[].
L = [0, 1, 2, 3, 4, 5, 6, 7],
S = [7],
O = [[1, 2, 3]],
M = [1, 2, 3] ;
L = [0, 1, 2, 3, 4, 5, 6, 7],
S = [6],
O = [[1, 2]],
M = [1, 2] ;
L = [0, 1, 2, 3, 4, 5, 6, 7],
S = [6, 7],
O = [[1, 2], [1, 2, 3]],
M = [1, 2] .

*/



/*
?- topology(I,Y),writeln(I;Y),fail.
129;[7, 0]
131;[7, 1, 0]
133;[7, 2, 0]
137;[7, 3, 0]
139;[7, 3, 1, 0]
141;[7, 3, 2, 0]
145;[7, 4, 0]
161;[7, 5, 0]
163;[7, 5, 1, 0]
169;[7, 5, 3, 0]
171;[7, 5, 3, 1, 0]
177;[7, 5, 4, 0]
193;[7, 6, 0]
197;[7, 6, 2, 0]
201;[7, 6, 3, 0]
205;[7, 6, 3, 2, 0]
209;[7, 6, 4, 0]
225;[7, 6, 5, 0]
241;[7, 6, 5, 4, 0]
false.

?- topology(I,Y),is_a_collection_of_groups(Y,O,Y),writeln(I;O),fail.
129;[[1, 2, 3], []]
131;[[1, 2, 3], [3], []]
133;[[1, 2, 3], [2], []]
137;[[1, 2, 3], [2, 3], []]
139;[[1, 2, 3], [2, 3], [3], []]
141;[[1, 2, 3], [2, 3], [2], []]
145;[[1, 2, 3], [1], []]
161;[[1, 2, 3], [1, 3], []]
163;[[1, 2, 3], [1, 3], [3], []]
169;[[1, 2, 3], [1, 3], [2, 3], []]
171;[[1, 2, 3], [1, 3], [2, 3], [3], []]
177;[[1, 2, 3], [1, 3], [1], []]
193;[[1, 2, 3], [1, 2], []]
197;[[1, 2, 3], [1, 2], [2], []]
201;[[1, 2, 3], [1, 2], [2, 3], []]
205;[[1, 2, 3], [1, 2], [2, 3], [2], []]
209;[[1, 2, 3], [1, 2], [1], []]
225;[[1, 2, 3], [1, 2], [1, 3], []]
241;[[1, 2, 3], [1, 2], [1, 3], [1], []]
false.

*/

% terminology of topology

points(N):- agents(N).
point(I):- agent(I).

is_open( X, C, Tid):- topology(Tid,T), member(X, T), group(X, _,C).
is_closed( X, C, T):- is_open( Y, _, T), is_complement_of(X, Y), group(X,_,C).
is_clopen( X, C, T):- is_open(X, C, T), is_closed( X, C, T).

/*

 ?- I=131,topology(I,Y),member(X,Y),group(X,_,Z),writeln(Y;X;Z),fail.
[7, 1, 0];7;[1, 2, 3]
[7, 1, 0];1;[3]
[7, 1, 0];0;[]
false.

 ?- is_open(X,B,131),B\=[].
X = 7,
B = [1, 2, 3] ;
X = 1,
B = [3] ;
false.

 ?- is_closed(X,B,131).
X = 0,
B = [] ;
X = 6,
B = [1, 2] ;
X = 7,
B = [1, 2, 3] ;
false.

?- is_clopen(X,B,131).
X = 7,
B = [1, 2, 3] ;
X = 0,
B = [] ;

*/



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% filter, ultrafilter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

ufilter(Fid, T):-
  filter(Fid, T),
  \+ (filter(_, S), S\=T, subset(T, S)).

filter(Fid, T):-
   all_groups(L),
   filter_id(Fid,L,_,T,_),
   Fid \= 0.

filter_id(0,[],[],[],[]).
filter_id(J,[X|Y],[0|B],C,[X|D]):-
   filter_id(J,Y,B,C,D),
   \+ filter_axiom(add_if, X,C,D).
filter_id(K,[X|Y],[1|B],[X|C],D):-
   filter_id(J,Y,B,C,D),
   \+ filter_axiom(remove_if, X,C,D),
   length(Y,I), K is J + 2 ^ I.

filter_axiom(remove_if, X,_,_):- group(X,_,[]).
filter_axiom(add_if, X,_,_):- agents(N), group(X,_,N).
filter_axiom(add_if, X,C,_):- has_a_subgroup(X,_,C).
filter_axiom(remove_if, X,_,D):- has_a_supergroup(X,_,D).
%filter_axiom(add_if, X,C,_):- is_an_intersection_of_groups(X,_,C).
%filter_axiom(remove_if, X,_,D):- has_an_intersection_that_has_been_excluded(X,_,D).
filter_axiom(add_if, X,_,D):- complement_has_been_excluded(X,_,D).
filter_axiom(remove_if, X,C,_):- complement_has_been_included(X,_,C).

has_an_intersection_that_has_been_excluded(X,Y,T):- 
   is_an_intersection_of_groups(Y,[X,_],[X|T]), \+ member(Y,T).

complement_has_been_excluded(X,Y,T):-
   is_complement_of(X,Y), member(Y,T).

complement_has_been_included(X,Y,T):-
   is_complement_of(X,Y), member(Y,T).

/*

?- filter(I,Y),writeln(I;Y),fail.
15;[4, 5, 6, 7]
23;[3, 5, 6, 7]
51;[2, 3, 6, 7]
85;[1, 3, 5, 7]
false.

 ?- ufilter(I,Y),writeln(I;Y),fail.
15;[4, 5, 6, 7]
23;[3, 5, 6, 7]
51;[2, 3, 6, 7]
85;[1, 3, 5, 7]
false.

?- ufilter(I,Y),is_a_collection_of_groups(Y,O,Y),writeln(I;O),fail.
15;[[1], [1, 3], [1, 2], [1, 2, 3]]
23;[[2, 3], [1, 3], [1, 2], [1, 2, 3]]
51;[[2], [2, 3], [1, 2], [1, 2, 3]]
85;[[3], [2, 3], [1, 3], [1, 2, 3]]
false.

*/


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% simple games
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

sgame(Wid, W):-
   all_groups(L),
   reverse(L,R),
   sgame_id(Wid,R,_,W,_),
   Wid \= 0.

sgame_id(0,[],[],[],[]).
sgame_id(J,[X|Y],[0|B],C,[X|D]):-
   sgame_id(J,Y,B,C,D),
   \+ sgame_axiom(add_if, X,C,D).
sgame_id(K,[X|Y],[1|B],[X|C],D):-
   sgame_id(J,Y,B,C,D),
   \+ sgame_axiom(remove_if, X,C,D),
   length(Y,I), K is J+ 2^I.

sgame_axiom(remove_if, X,_,_):- group(X,_,[]).
sgame_axiom(add_if, X,_,_):- agents(N), group(X,_,N).
sgame_axiom(add_if, X,W,_):- has_a_subgroup(X,_,W).
sgame_axiom(remove_if, X,_,L):- has_a_supergroup(X,_,L).

% axioms for strong simple game
sgame_axiom(add_if, X,_,L):- complement_has_been_excluded(X,_,L).
sgame_axiom(remove_if, X,W,_):- complement_has_been_included(X,_,W).


/*

 ?- sgame(I,Y),writeln(I;Y),fail.
170;[7, 5, 3, 1]
204;[7, 6, 3, 2]
232;[7, 6, 5, 3]
240;[7, 6, 5, 4]
false.

118 ?- sgame(I,Y),is_a_collection_of_groups(Y,O,Y),writeln(I;O),fail.
170;[[1, 2, 3], [1, 3], [2, 3], [3]]
204;[[1, 2, 3], [1, 2], [2, 3], [2]]
232;[[1, 2, 3], [1, 2], [1, 3], [2, 3]]
240;[[1, 2, 3], [1, 2], [1, 3], [1]]
false.

% a comparison (using sgnn06.pl)

?- gen_win(W,[proper:yes,strong:yes,monotonic:yes]),nl,write(W),inspectall_win(S),write(S),fail.

[[1, 2, 3], [1, 2], [1, 3], [1]][yes, yes, yes, no([1]), no(1), yes]
[[1, 2, 3], [1, 2], [1, 3], [2, 3]][yes, yes, yes, yes, yes, yes]
[[1, 2, 3], [1, 2], [2, 3], [2]][yes, yes, yes, no([2]), no(2), yes]
[[1, 2, 3], [1, 3], [2, 3], [3]][yes, yes, yes, no([3]), no(3), yes]
false.

*/

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Matroid
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 19-20 Oct 2009 under construction

matroid(Mid, T):-
   all_groups(L),
   reverse(L,R),
   matroid_id(Mid,R,_,T),
   Mid \= 0.

matroid_id(0,[],[],[]).
matroid_id(J,[X|Y],[0|B],C):-
   matroid_id(J,Y,B,C),
   \+ matroid_axiom(add_if, X,C).
matroid_id(K,[X|Y],[1|B],[X|C]):-
   matroid_id(J,Y,B,C),
   \+ matroid_axiom(remove_if, X,C),
   length(Y,I), K is J+ 2^I.

matroid_axiom(add_if, X,_):- group(X,_,[]).
matroid_axiom(add_if, X,T):- has_hereditary_property_1(X,_,T). 
matroid_axiom(remove_if, X,T):- has_hereditary_property_2(X,_,T). 
matroid_axiom(remove_if, X,T):- has_augmentation_property(X,_,T). 

subgroup(X,Y,D):- group(X,_,A), group(Y,_,B), subset(A,B),subtract(B,A,D).

has_hereditary_property_1(X,Y,T):-
 % This is a subgroup which should be selected (However, it does not occur in this construction of group list.) 
   member(Y, T), subgroup(X,Y,_).

has_hereditary_property_2(X,Y,T):-  % There is no unselected foregone subgroup when this group selected.
   subgroup(Y,X,_), Y @< X, \+ member(Y, T).

has_augmentation_property(X,(Y,Z),T):-
   subgroup(Y,X,D),member(Y,T),member(W,D),group(X,_,C),
   subgroup(Z,X,[W|C]), \+ member(Z,T). 

/*

?- matroid(I,Y),writeln(I;Y),fail.
1;[0]
3;[1, 0]
5;[2, 0]
7;[2, 1, 0]
15;[3, 2, 1, 0]
17;[4, 0]
19;[4, 1, 0]
21;[4, 2, 0]
23;[4, 2, 1, 0]
31;[4, 3, 2, 1, 0]
51;[5, 4, 1, 0]
55;[5, 4, 2, 1, 0]
63;[5, 4, 3, 2, 1, 0]
85;[6, 4, 2, 0]
87;[6, 4, 2, 1, 0]
95;[6, 4, 3, 2, 1, 0]
119;[6, 5, 4, 2, 1, 0]
127;[6, 5, 4, 3, 2, 1, 0]
255;[7, 6, 5, 4, 3, 2, 1, 0]
false.

?- matroid(I,Y),is_a_collection_of_groups(Y,O,Y),writeln(I;O),fail.
1;[[]]
3;[[3], []]
5;[[2], []]
7;[[2], [3], []]
15;[[2, 3], [2], [3], []]
17;[[1], []]
19;[[1], [3], []]
21;[[1], [2], []]
23;[[1], [2], [3], []]
31;[[1], [2, 3], [2], [3], []]
51;[[1, 3], [1], [3], []]
55;[[1, 3], [1], [2], [3], []]
63;[[1, 3], [1], [2, 3], [2], [3], []]
85;[[1, 2], [1], [2], []]
87;[[1, 2], [1], [2], [3], []]
95;[[1, 2], [1], [2, 3], [2], [3], []]
119;[[1, 2], [1, 3], [1], [2], [3], []]
127;[[1, 2], [1, 3], [1], [2, 3], [2], [3], []]
255;[[1, 2, 3], [1, 2], [1, 3], [1], [2, 3], [2], [3], []]
false.

*/

% end