/************************************************************
  common admissible domain, closedness under decisiveness 
  implicature, and decomposability: proving Kalai-Muller theorem
  program: dcdi06.pl
  language: prolog
  date: 2006.12.22-23,25-26,31 & 2007.1.5-6.
  creator: Kenryo INDO
************************************************************/
% load the social choice analyzer if oof/2 does not exist.
:- (\+ clause(oof(_,_),_)->[spcf06];true).

init_me:-init_me(4).
init_me(K):- L=[gprf06,cswf06,spcf06,dcdi06],
   nth1(J,L,P),J=retract(O);true),assert(r_j_admission(J,L)).
init_r_admission:- domain_type(T:_),all_r(L,T),update_r_admission(L).
init_r_j_admission(J):- j(J), r_admission(L),
   forall(clause(r_j_admission(J,_),_),update_r_j_admission(J,L)).

r_admit(Q):-
   domain_type(T:_),r_admission(L),R=..[T,Q],R,member(Q,L).

% override r/1 (to update domain with r_admit and affect rr/1,3).
r_admit_domain:- abolish(r/1),forall(r_admit(Q),assert(r(Q))). 

% override chdom/1 to initialize r_admission/1.
chdom(A->A):- \+ var(A),domain_type(A).
chdom(A->B):- domain_type(A),r_type(B),B\=A,
   update_domain(B),init_r_admission.

:- init_r_admission.

% override rr/2 (to affect rr/1,3).
rr([],[]).
rr([Q|R],[J|N]):- rr(R,N),r_j_admitted(J,Q).
r_j_admitted(J,Q):- j(J),clause(r_j_admission(J,L),_),r(Q,_,_),oof(Q,L).
r_j_admitted(J,Q):- j(J),\+ clause(r_j_admission(J,_),_), r(Q).

% generating common admissible domain 
% specified with type T and length N

restricted_domain(L,T,N):- all_r(A,T),
   (var(L)->select_n(L,A,N);(subset(L,A),length(L,N))),
   L\=[],update_r_admission(L).

select_n([],[],0).
select_n([R|Q],[R|S],A):-select_n(Q,S,B), A is B + 1.
select_n(Q,[_|S],B):-select_n(Q,S,B).

% omission for current domain (added: 31 Dec2006)
restricted_domain(L):-
   domain_type(T:_),restricted_domain(L,T,_).

display_domain(L):- (var(L)->r_admission(L);true),forall(oof(R,L),(id_r(_:S,R,_),write(S))).

% a experiment of existence of the strategy-proof scf.

/*
?- show_scf_hl(l),
stopwatch((restricted_domain(L,l,N),\+ \+ (scf(F,sp),cs_scf(F),
show_scf_l0(F,l),tab(2),display_domain(L)),fail;true),Time).

pref:j=1:ACITZNACITZNACITZNACITZNACITZNACITZN
pref:j=2:AAAAAACCCCCCIIIIIITTTTTTZZZZZZNNNNNN
best:j=1:abbaccabbaccabbaccabbaccabbaccabbacc
best:j=2:aaaaaabbbbbbbbbbbbaaaaaacccccccccccc
scf:     abbaccabbaccabbaccabbaccabbaccabbacc  ACITZN
scf:     abbaa-bbbbb-bbbbb-abbaa-abbac-------  ACITZ
scf:     aaaa-aabba-babba-baaaa-a------abba-c  ACITN
scf:     abb-ccabb-ccabb-cc------abb-ccabb-cc  ACIZN
scf:     abb-a-bbb-b-bbb-b-------abb-c-------  ACIZ
scf:     aaa--aabb--babb--b------------abb--c  ACIN
scf:     aa-aaaab-aab------aa-aaaaa-accab-acc  ACTZN
scf:     aa-aa-ab-aa-------aa-aa-aa-ac-------  ACTZ
scf:     aa-a-aab-a-b------aa-a-a------ab-a-c  ACTN
scf:     aa--aaab--ab------------aa--ccab--cc  ACZN
scf:     aa--a-ab--a-------------aa--c-------  ACZ
scf:     aa---aab---b------------------ab---c  ACN
scf:     a-bacc------a-bacca-bacca-bacca-bacc  AITZN
scf:     a-baa-------b-bbb-a-baa-a-bac-------  AITZ
scf:     a-aa-a------a-ba-ba-aa-a------a-ba-c  AITN
scf:     a-aa--------b-bc--a-aa--------------  AIT
scf:     a-b-cc------a-b-cc------a-b-cca-b-cc  AIZN
scf:     a-b-a-------b-b-b-------a-b-c-------  AIZ
scf:     a-a--a------a-b--b------------a-b--c  AIN
scf:     a--a-b------------a--a-c------a--a-c  ATN
scf:     a---ab------------------a---cca---cc  AZN
scf:     a----b------------------------a----c  AN
scf:     -------bbacc-bbacc-bbacc-bbacc-bbacc  CITZN
scf:     -------bbbb--bbbb--bbaa--bbac-------  CITZ
scf:     -------bba-b-bba-b-aaa-a-------bba-c  CITN
scf:     -------bba---bbc---aaa--------------  CIT
scf:     -------bb-a--bb-c--------bb-c-------  CIZ
scf:     -------b-aab-------a-aaa-a-acc-b-acc  CTZN
scf:     -------b-aa--------a-aa--a-ac-------  CTZ
scf:     -------b-a-b-------a-a-a-------b-a-c  CTN
scf:     -------b--ab-------------a--cc-b--cc  CZN
scf:     -------b--a--------------a--c-------  CZ
scf:     --------------bacc--bacc--bacc--bacc  ITZN
scf:     --------------bbb---baa---bac-------  ITZ
scf:     --------------ba-b--aa-a--------ba-c  ITN
scf:     --------------bc----aa--------------  IT
% time elapsed (sec): 3.531

No
?- show_scf_hl(l),stopwatch((restricted_domain(L,l,N),
\+ \+ (scf(F,sp),cs_scf(F),\+ dictatorial_scf(_,F),
show_scf_l0(F,l),tab(2),display_domain(L)),fail;true),Time).

pref:j=1:ACITZNACITZNACITZNACITZNACITZNACITZN
pref:j=2:AAAAAACCCCCCIIIIIITTTTTTZZZZZZNNNNNN
best:j=1:abbaccabbaccabbaccabbaccabbaccabbacc
best:j=2:aaaaaabbbbbbbbbbbbaaaaaacccccccccccc
scf:     abbaa-bbbbb-bbbbb-abbaa-abbac-------  ACITZ
scf:     aaaa-aabba-babba-baaaa-a------abba-c  ACITN
scf:     abb-abbbb-bbbbb-bb------abb-ccbbb-cc  ACIZN
scf:     abb-a-bbb-b-bbb-b-------abb-c-------  ACIZ
scf:     aaa--aabb--babb--b------------abb--c  ACIN
scf:     aa-aaaab-aab------aa-aaaaa-accab-acc  ACTZN
scf:     aa-aa-ab-aa-------aa-aa-aa-ac-------  ACTZ
scf:     aa-a-aab-a-b------aa-a-a------ab-a-c  ACTN
scf:     aa--aaab--ab------------aa--ccab--cc  ACZN
scf:     aa--a-ab--a-------------aa--c-------  ACZ
scf:     aa---aab---b------------------ab---c  ACN
scf:     a-aaaa------a-bacca-aaaaa-cacca-cacc  AITZN
scf:     a-baa-------b-bbb-a-baa-a-bac-------  AITZ
scf:     a-aa-a------a-ba-ba-aa-a------a-ba-c  AITN
scf:     a-aa--------b-bc--a-aa--------------  AIT
scf:     a-b-ab------b-b-bb------a-b-ccb-b-cc  AIZN
scf:     a-b-a-------b-b-b-------a-b-c-------  AIZ
scf:     a-a--a------a-b--b------------a-b--c  AIN
scf:     a--a-b------------a--a-c------a--a-c  ATN
scf:     a---ab------------------a---cca---cc  AZN
scf:     a----b------------------------a----c  AN
scf:     -------bbbbb-bbbbb-bbacc-bbccc-bbccc  CITZN
scf:     -------bbbb--bbbb--bbaa--bbac-------  CITZ
scf:     -------bba-b-bba-b-aaa-a-------bba-c  CITN
scf:     -------bba---bbc---aaa--------------  CIT
scf:     -------bb-a--bb-c--------bb-c-------  CIZ
scf:     -------b-aab-------a-aaa-a-acc-b-acc  CTZN
scf:     -------b-aa--------a-aa--a-ac-------  CTZ
scf:     -------b-a-b-------a-a-a-------b-a-c  CTN
scf:     -------b--ab-------------a--cc-b--cc  CZN
scf:     -------b--a--------------a--c-------  CZ
scf:     --------------bacc--aaaa--cacc--cacc  ITZN
scf:     --------------bbb---baa---bac-------  ITZ
scf:     --------------ba-b--aa-a--------ba-c  ITN
scf:     --------------bc----aa--------------  IT
% time elapsed (sec): 5.297

L = _G159
N = _G161
F = _G163
Time = 5.297 

?-
*/


%-------------------------------------------------
%  decomposability (Kalai and Muller, 1977)

% trivial/nontrivial ordered pair
dop_trivial((X,Y)):- dop((X,Y)),\+ (r(P),p((X,Y),P),r(Q),p((Y,X),Q)).
dop_ntr((X,Y)):- dop((X,Y)),\+ dop_trivial((X,Y)).

% closed under decisiveness implicature
cdi_pairs(D,Tb):- select_ntr(D,Tb),\+ not_cdi(_,_,D).
acyclic_cdi_pairs(D,Tb):- cdi_pairs(D,Tb),\+ circulate(_,D).
circulate((X,Y),B):- oof((X,Y),B),oof((Y,X),B).
circulate((X,Y),B):- oof((X,Y),B),oof((Y,Z),B),oof((Z,X),B).
select_ntr(D,Tb):- findall(B,dop(B),Tb), select_ntr(D,Tb,K),D\=Tb,K>0.
select_ntr([],[],0).
select_ntr([R|D],[R|S],K):- select_ntr(D,S,K),dop_trivial(R).
select_ntr([R|D],[R|S],M):- select_ntr(D,S,K),dop_ntr(R),M is K + 1.
select_ntr(D,[R|S],K):- select_ntr(D,S,K),dop_ntr(R).
not_cdi((V,C),(X,Y,Z),D):- dot((X,Y,Z)),
   dop_ntr((X,Y)),dop_ntr((X,Z)),not_cdi(V,(X,Y,Z),C,D).
not_cdi((1,A), (X,Y,Z),[(P,Q)],D):- rr([P,Q]),
   r((X,Y),P),r((Y,Z),P),r((Y,Z),Q),r((Z,X),Q),not_cdi_1(A, (X,Y,Z),D).
not_cdi((2,A), (X,Y,Z),[R], D):- r(R),
   r((X,Y),R),r((Y,Z),R),not_cdi_2(A, (X,Y,Z),D).
not_cdi_1(a,(X,Y,Z),D):- oof((X,Y),D),\+ oof((X,Z),D).
not_cdi_1(b,(X,Y,Z),D):- oof((Z,X),D),\+ oof((Y,X),D).
not_cdi_2(a,(X,Y,Z),D):- oof((X,Y),D),oof((Y,Z),D),\+ oof((X,Z),D).
not_cdi_2(b,(X,Y,Z),D):- oof((Z,X),D),oof((Y,X),D),oof((Z,Y),D).
not_cdi_2(c,(X,Y,Z),D):- oof((Z,X),D),\+ oof((Y,X),D),\+ oof((Z,Y),D).

% decomposability
decomposable_domain(L,T,N):- restricted_domain(L,T,N),\+ \+ cdi_pairs(_,_).
acyclic_decomposable_domain(L,T,N):- restricted_domain(L,T,N),\+ \+ acyclic_cdi_pairs(_,_).

%-----------
% demos

% the verification of Kalai-Muller Theorem 2 and Theorem 3.
% Assuming liner common admmisible domain,
% there exists a set of cdi-pairs(cdi-triple) i.e., decomposable domain 
% <-> there exists an arrovian swf on liner common admmisible domain ...[A]
% <-> there exists an exists an scf which satisfies SP + ND ...[B]

/*
proof:[A]

?- nl,restricted_domain(L,l,N),\+ cdi_pairs(_,_),
\+ \+ (swf(F,arrow(l)),\+ dictator(_,F)).

No
?- decomposable_domain(L,l,N),
\+ (swf(F,arrow(l)),\+ dictator(_,F)).

No
?-

% addeundum for proving [A]: two latin squares are both decomposable but 
% there are only Arrovian SWFs using the inadmissible rankings.  
?- decomposable_domain(L,l,N),
\+ (swf(F,arrow),\+ dictator(_,F)), nl,display_domain(L),write(:),write(L),fail.

AIZ:[[+, +, +], [-, -, +], [+, -, -]]
CTN:[[-, +, +], [+, +, -], [-, -, -]]

No
?-

proof:[B]

?- restricted_domain(L,l,N),\+ cdi_pairs(_,_),
\+ \+ (scf(F,sp),cs_scf(F),\+ dictatorial_scf(_,F)).

No
?- decomposable_domain(L,l,N),
\+ (scf(F,sp),\+ dictatorial_scf(_,F)).

No
?-
*/

% the verification of an extension of Kalai-Muller Theorem 2 and Theorem 3.
% Assuming liner common admmisible domain,
% there exists a noncircular set of cdi-pairs(cdi-triple)
% i.e., acyclically decomposable domain 
% <-> there exists an scf which satisfies SP + ND + SC unless it cannot choose best alternative...[B]
% <-> there exists an arrovian swf with SC condition ...[A]

/*
proof:[B]
?- restricted_domain(L,l,N),\+ acyclic_cdi_pairs(_,_),
\+ \+ (scf(F,sp),cs_scf(F),\+ dictatorial_scf(_,F)).

No
?- acyclic_decomposable_domain(L,l,N),
\+ (scf(F,sp),cs_scf(F),\+ dictatorial_scf(_,F)),
nl,display_domain(L),tab(1),
forall(oof(R,L),(best(A,R),write(A))),fail.

ACIT abba
ATZN aacc
CIZN bbcc

No
?- demo_r(l).

1:[+, +, +]:A
3:[-, +, +]:C
9:[-, -, +]:I
19:[+, +, -]:T
25:[+, -, -]:Z
27:[-, -, -]:N

Yes
?- 

*/

/*
proof:[A]
% acyclically decomposable domain -> ND swf 
?- acyclic_decomposable_domain(L,l,N),
\+ (swf(F,arrow(l)),\+ dictator(_,F)),nl,display_domain(L),fail.

No
?-

% NOT (ND swf -> acyclically decomposable domain)
?- nl,restricted_domain(L,l,N),\+ acyclic_cdi_pairs(_,_),
(\+ \+ (swf(F,arrow(l)),\+ dictator(_,F))),
display_domain(L),write(;),fail.

ACI;ACT;AC;AI;ATZ;AT;AZ;CIN;CI;CT;CN;IZN;IZ;IN;TZN;TZ;TN;ZN;

No
?-

% ND + CS swf -> acyclically decomposable domain
?- nl,restricted_domain(L,l,N),\+ acyclic_cdi_pairs(_,_),
(\+ \+ (swf(F,arrow(l)),\+ dictator(_,F),cs(F))).

No
?- 
*/

% addendum (admissible domain valued swf)

/*

?- nl,restricted_domain(L,l,N),\+ acyclic_cdi_pairs(_,_),
(\+ \+ (swf(F,arrow),\+ dictator(_,F),cs(F))).

No
?- acyclic_decomposable_domain(L,l,N),
display_domain(L),write(;),
\+ (swf(F,arrow),\+ dictator(_,F)),nl,display_domain(L),fail.

AIZ
CTN

No
?-

?- nl,restricted_domain(L,l,N),\+ acyclic_cdi_pairs(_,_),
\+ \+ (swf(F,arrow(l)),\+ dictator(_,F),display_swf_t2(F)),
nl,display_domain(domain:L).


swf:row  col |ACI ab|+-- ac|++- bc|+++
--------------------------------------------------
[+, +, +]=A  |AAA  +|+++  +|+++  +|+++
[-, +, +]=C  |ACC  -|+--  +|+++  +|+++
[-, -, +]=I  |ACI  -|+--  -|++-  +|+++
domain:ACI

L = [[+, +, +], [-, +, +], [-, -, +]]
N = 3
F = _G171 ;

swf:row  col |ACT ab|+-+ ac|+++ bc|++-
--------------------------------------------------
[+, +, +]=A  |AAA  +|+++  +|+++  +|+++
[-, +, +]=C  |AAC  -|+-+  +|+++  +|+++
[+, +, -]=T  |AAT  +|+++  +|+++  -|++-
domain:ACT

L = [[+, +, +], [-, +, +], [+, +, -]]
N = 3
F = _G171 ;

swf:row  col |AC ab|+- ac|++ bc|++
--------------------------------------------------
[+, +, +]=A  |AA  +|++  +|++  +|++
[-, +, +]=C  |AC  -|+-  +|++  +|++
domain:AC

L = [[+, +, +], [-, +, +]]
N = 2
F = _G171 

Yes
?- 

*/


%---- end 

return to front page.