More compact definition

问题:

Given word/1,

word(W) :-
   abs(ABs),
   ABs = W.

abs([]).
abs([AB|ABs]) :-
   abs(ABs),
   ab(AB).

ab(a).
ab(b).

?- word(W).
   W = []
;  W = [a]
;  W = [b]
;  W = [a,a]
;  W = [b,a]
;  W = [a,b]
;  W = [b,b]
;  W = [a,a,a]
;  W = [b,a,a]
;  W = [a,b,a]
;  W = [b,b,a]
;  W = [a,a,b]
;  W = [b,a,b]
;  W = [a,b,b]
;  W = [b,b,b]
;  W = [a,a,a,a]
...

how does a more compact definition of word/1 look like, otherwise identical w.r.t. termination and the set of solutions, fairness, with the following constraints:

1. No use of built-ins like (=)/2.

2. No use of control constructs like (',')/2 or (;)/2, or call/1.

3. Uses one fact, one recursive rule, and one rule for word/1.

Maybe simpler is to ask for the terms F1 ... F4 in:

word(W) :-
   p(F1).

p(F2).
p(F3) :-
   p(F4).

For the record: The property exploited here is closely related to the undecidability of termination of a single binary clause. Praise goes to:

Philippe Devienne, Patrick Lebègue, Jean-Christophe Routier, and Jörg Würtz. One binary horn clause is enough STACS '94.

回答1:

The solution I have come up with is:

word(W) :-
        p([[]|Ls], Ls, W).

p([W|_], _, W).
p([W0|Ws], [[a|W0],[b|W0]|Ls], W) :-
        p(Ws, Ls, W).

Sample query and answer:

?- word(W).
W = [] ;
W = [a] ;
W = [b] ;
W = [a, a] ;
W = [b, a] ;
W = [a, b] ;
W = [b, b] ;
W = [a, a, a] ;
W = [b, a, a] ;
W = [a, b, a] ;
W = [b, b, a] ;
W = [a, a, b] ;
W = [b, a, b] ;
W = [a, b, b] ;
W = [b, b, b] ;
W = [a, a, a, a] ;
W = [b, a, a, a] ;
etc.

I am using a difference list to incrementally materialize the solutions I want the toplevel to report.

回答2:

Okay so not an answer yet.

The closest I had was :

s_s1([],[a]).
s_s1([b|T],[a|T]).
s_s1([a|T],[b|T2]):-
 s_s1(T,T2).

word([]).
word(W2):-
 word(W),
 s_s1(W,W2).

Which does not either meet the criteria or give the right solutions!

So next I thought we could try and use prolog to find the answer.. The structure is given so we need to search for the args..

%First define the first 16 correct solutions.. 
correct_sols(X):-
X=[
     [],
     [a],
     [b],
     [a,a],
     [b,a],
     [a,b],
     [b,b],
     [a,a,a],
     [b,a,a],
     [a,b,a],
     [b,b,a],
     [a,a,b],
     [b,a,b],
     [a,b,b],
     [b,b,b],
     [a,a,a,a]
].

%Then a mi
provable(true, _) :- !.
provable((G1,G2), Defs) :- !,
    provable(G1, Defs),
    provable(G2, Defs).
provable(BI, _) :-
    predicate_property(BI, built_in),
    !,
    call(BI).
provable(Goal, Defs) :-
    member(Def, Defs),
    copy_term(Def, Goal-Body),
    provable(Body, Defs).

%From 4 Vars find 16 solutions to word(X)
vars_16sols(Vars,List):-
    Vars =[Args,Args0,Args1,Argsx],
    findnsols(16,X,provable(word(X),[
                            a(Args)-true,
                            a(Args0)-a(Args1),
                            word(X)-a(Argsx)]
                       ),List).
%Evaluate the score, for the solutions found how many match correct
evaluate_score(Solutions,Score):-
   correct_sols(C),
   maplist(correct_test_tf,C,Solutions,TrueFalse),
   findall(_,member(true,TrueFalse),Matches),
   length(Matches,Score).

%The main search, give a form for the starting 4 arguments, if they 
match all 16 correct stop.
startingargs_solution(Start,Sol):-
   vars_16sols(Start,SolsStart),
   evaluate_score(SolsStart,Score),
   Score =16,
   SolsStart=Sol.
%Othewise refine args, and try again.
startingargs_solution(Start,Sol):-
   vars_16sols(Start,SolsStart),
   evaluate_score(SolsStart,Score),
   Score <16,
   start_refined(Start,Refined),
   startingargs_solution(Refined,Sol).

We would still need to define :

1. correct_test_tf/3
2. start_refined/2 with some constraints, such as the size of the terms for args(needs to be reasonable to be a 'compact definition', and what things need to be included, i.e. at least a and b somewhere and probably [].

Clearly not finished and not sure if it will be possible to do this but thought I would post an answer to see what people have to say.. The search is naive at the moment!

This is only testing the first 16 solutions but maybe that is adequate to get a correct answer..

Also maybe this is harder then solving the question on its own!

回答3:

My closest yet.

unfold20([], []).
unfold20([H|T], [[a|H], [b|H]|L]) :-
   unfold20(T, L).

member20(X, [X|_]).
member20(X, [_|Tail]) :-
  member20(X, Tail).

swap20(R,R) :-
    write('swap20 R: '),write(R),nl.

swap20(In,L) :-
    write('swap20 In: '),write(In),nl,
    unfold20(In,L),
    swap20(L,_),
    write('swap20 L: '),write(L),nl.

word20(W) :-
    swap20([[]],L),
    write('word20 L: '),write(L),nl,
    member20(W,L),
    write('word20 W: '),write(W),nl.

?- word20(X).
swap20 R: [[]]
word20 L: [[]]
word20 W: []
X = [] ;
swap20 In: [[]]
swap20 R: [[a],[b]]
swap20 L: [[a],[b]]
word20 L: [[a],[b]]
word20 W: [a]
X = [a] ;
word20 W: [b]
X = [b] ;
swap20 In: [[a],[b]]
swap20 R: [[a,a],[b,a],[a,b],[b,b]]
swap20 L: [[a,a],[b,a],[a,b],[b,b]]
swap20 L: [[a],[b]]
word20 L: [[a],[b]]
word20 W: [a]
X = [a] ;
word20 W: [b]
X = [b] ;
swap20 In: [[a,a],[b,a],[a,b],[b,b]]
swap20 R: [[a,a,a],[b,a,a],[a,b,a],[b,b,a],[a,a,b],[b,a,b],[a,b,b],[b,b,b]]
swap20 L: [[a,a,a],[b,a,a],[a,b,a],[b,b,a],[a,a,b],[b,a,b],[a,b,b],[b,b,b]]
swap20 L: [[a,a],[b,a],[a,b],[b,b]]
swap20 L: [[a],[b]]
word20 L: [[a],[b]]
word20 W: [a]
X = [a] ;
word20 W: [b]
X = [b] ;
swap20 In: [[a,a,a],[b,a,a],[a,b,a],[b,b,a],[a,a,b],[b,a,b],[a,b,b],[b,b,b]]
swap20 R: [[a,a,a,a],[b,a,a,a],[a,b,a,a],[b,b,a,a],[a,a,b,a],[b,a,b,a],[a,b,b,a],[b,b,b,a],[a,a,a,b],[b,a,a,b],[a,b,a,b],[b,b,a,b],[a,a,b,b],[b,a,b,b],[a,b,b,b],[b,b,b,b]]
swap20 L: [[a,a,a,a],[b,a,a,a],[a,b,a,a],[b,b,a,a],[a,a,b,a],[b,a,b,a],[a,b,b,a],[b,b,b,a],[a,a,a,b],[b,a,a,b],[a,b,a,b],[b,b,a,b],[a,a,b,b],[b,a,b,b],[a,b,b,b],[b,b,b,b]]
swap20 L: [[a,a,a],[b,a,a],[a,b,a],[b,b,a],[a,a,b],[b,a,b],[a,b,b],[b,b,b]]
swap20 L: [[a,a],[b,a],[a,b],[b,b]]
swap20 L: [[a],[b]]
word20 L: [[a],[b]]
word20 W: [a]
X = [a]

If you look you will see that there is no use of ; which I am sure is a problem some people are having. Also all of the rules are simple enough that they should be able to be folded into the requirements by using additional arguments. e.g. unfold(A,B) would become unfold(A,B,C,D) or a variation.

The problem with this version is that I get the correct answers as the evaluation progresses, it is just getting them back to the top level.

e.g.

swap20 L: [[a,a,a],[b,a,a],[a,b,a],[b,b,a],[a,a,b],[b,a,b],[a,b,b],[b,b,b]]
swap20 L: [[a,a],[b,a],[a,b],[b,b]]
swap20 L: [[a],[b]]

I will keep working on this before the dead line, but if someone is able to use what I have here, hats off to them, I just ask that you give credit if any part of this helped you get the answer.

The unfold predicate is based on this SO answer. Credit to salva

member is an old friend. Notice that it starts with [[]] and not [].

swap I created this predicate. I have swap working for different variation yet the variation fails for a different reason.

Supplement

Debugger output of mat's answer

I looked at Mat's answer more closely with a debugger because it might hold the answer to a similar problem where I can generate the answers but not return them independently to Top.

Mat's answer copied here for reference.

p([W|_], _, W).

p([W0|Ws], [[a|W0],[b|W0]|Ls], W) :-
    p(Ws, Ls, W).

word(W) :-
    p([[]|Ls], Ls, W).

The part of interest is far to the right as comments. I would suggest that you copy from here and past into a app that allows you to see all of the line without wrapping or hidden.

The column on the left was created with SWI-Prolog running the query with trace and the comments on the right were created by running the query with gtrace and hand copying the values and noting the level for indentation.

?- word(W).
   Call: (8) word(_822) ? creep                                                                                                                                      % word(W) :-
   Call: (9) p([[]|_1010], _1010, _822) ? creep                                                                                                                      %   p([[]|Ls], Ls, W).
   Exit: (9) p([[]|_1010], _1010, []) ? creep                                                                                                                        %   p([W|_], _, W).                             % W = []
   Exit: (8) word([]) ? creep                                                                                                                                        % p([[]|Ls], Ls, W).                            % W = []
W = [] ;                                                                                                                                                                                                                       
   Redo: (9) p([[]|_1010], _1010, _822) ? creep                                                                                                                      %   p([W0|Ws], [[a|W0],[b|W0]|Ls], W) :-        %              W0 = []    Ws = [[a],[b]|Ls]
   Call: (10) p([[a], [b]|_1028], _1028, _822) ? creep                                                                                                               %     p(Ws, Ls, W).                             %              W0 = []    Ws = [[a],[b]|Ls]
   Exit: (10) p([[a], [b]|_1028], _1028, [a]) ? creep                                                                                                                %     p([W|_], _, W).                           % W = [a]    
   Exit: (9) p([[], [a], [b]|_1028], [[a], [b]|_1028], [a]) ? creep                                                                                                  %   p(Ws, Ls, W).                               % W = [a]      W0 = []    Ws = [[a],[b]|Ls]
   Exit: (8) word([a]) ? creep                                                                                                                                       % p([[]|Ls], Ls, W).                            % W = [a]                                                                               Ls = [[a],[b]|_2312]
W = [a] ;                                                                                                                                                                                                                                                                                             
   Redo: (10) p([[a], [b]|_1028], _1028, _822) ? creep                                                                                                               %     p([W0|Ws], [[a|W0],[b|W0]|Ls], W) :-      %              W0 = [a]   Ws = [    [b],[a,a],[b,a]|Ls]                          
   Call: (11) p([[b], [a, a], [b, a]|_1052], _1052, _822) ? creep                                                                                                    %       p(Ws, Ls, W).                           %              W0 = [a]   Ws = [    [b],[a,a],[b,a]|Ls]                          
   Exit: (11) p([[b], [a, a], [b, a]|_1052], _1052, [b]) ? creep                                                                                                     %       p([W|_], _, W).                         % W = [b]                                                                    
   Exit: (10) p([[a], [b], [a, a], [b, a]|_1052], [[a, a], [b, a]|_1052], [b]) ? creep                                                                               %     p(Ws, Ls, W).                             % W = [b]      W0 = [a]   Ws = [    [b],[a,a],[b,a]|Ls]                         
   Exit: (9) p([[], [a], [b], [a, a], [b, a]|_1052], [[a], [b], [a, a], [b, a]|_1052], [b]) ? creep                                                                  %   p(Ws, Ls, W).                               % W = [b]      W0 = []    Ws = [[a],[b],[a,a],[b,a]|_2324]                              Ls = [        [a,a],[b,a]|_2324] 
   Exit: (8) word([b]) ? creep                                                                                                                                       % p([[]|Ls], Ls, W).                            % W = [b]                                                                               Ls = [[a],[b],[a,a],[b,a]|_2324]                            
W = [b] .                                                                                                                                                                                                                                                                                            
   Redo: (11) p([[b], [a, a], [b, a]|_1052], _1052, _822) ? creep                                                                                                    %       p([W0|Ws], [[a|W0],[b|W0]|Ls], W) :-    %              W0 = [b]   Ws = [        [a,a],[b,a],[a,b],[b,b]|Ls]                  
   Call: (12) p([[a, a], [b, a], [a, b], [b, b]|_1076], _1076, _822) ? creep                                                                                         %         p(Ws, Ls, W).                         %              W0 = [b]   Ws = [        [a,a],[b,a],[a,b],[b,b]|Ls]                  
   Exit: (12) p([[a, a], [b, a], [a, b], [b, b]|_1076], _1076, [a, a]) ? creep                                                                                       %         p([W|_], _, W).                       % W = [a,a]                                                                   
   Exit: (11) p([[b], [a, a], [b, a], [a, b], [b, b]|_1076], [[a, b], [b, b]|_1076], [a, a]) ? creep                                                                 %       p(Ws, Ls, W).                           % W = [a,a]    W0 = [b]   Ws = [        [a,a],[b,a],[a,b],[b,b]|Ls]                  
   Exit: (10) p([[a], [b], [a, a], [b, a], [a, b], [b, b]|_1076], [[a, a], [b, a], [a, b], [b, b]|_1076], [a, a]) ? creep                                            %     p(Ws, Ls, W).                             % W = [a,a]    W0 = [a]   Ws = [    [b],[a,a],[b,a],[a,b],[b,b]|_2348]                  Ls = [                    [a,b],[b,b]|_2348]
   Exit: (9) p([[], [a], [b], [a, a], [b, a], [a, b], [b|...]|_1076], [[a], [b], [a, a], [b, a], [a, b], [b, b]|_1076], [a, a]) ? creep                              %   p(Ws, Ls, W).                               % W = [a,a]    W0 = []    Ws = [[a],[b],[a,a],[b,a],[a,b],[b,b]|_2348]                  Ls = [        [a,a],[b,a],[a,b],[b,b]|_2348] 
   Exit: (8) word([a, a]) ? creep                                                                                                                                    % p([[]|Ls], Ls, W).                            % W = [a,a]                                                                             Ls = [[a],[b],[a,a],[b,a],[a,b],[b,b]|_2348]
W = [a, a] ;                                                                                                                                                               
   Redo: (12) p([[a, a], [b, a], [a, b], [b, b]|_1076], _1076, _822) ? creep                                                                                                                         
   Call: (13) p([[b, a], [a, b], [b, b], [a, a, a], [b, a, a]|_1100], _1100, _822) ? creep                                                                           %         p([W0|Ws], [[a|W0],[b|W0]|Ls], W) :-  %              W0 = [a,a] Ws = [              [b,a],[a,b],[b,b],[a,a,a],[b,a,a]|Ls]                                              
   Exit: (13) p([[b, a], [a, b], [b, b], [a, a, a], [b, a, a]|_1100], _1100, [b, a]) ? creep                                                                         %           p(Ws, Ls, W).                       %              W0 = [a,a] Ws = [              [b,a],[a,b],[b,b],[a,a,a],[b,a,a]|Ls]                                                  
   Exit: (12) p([[a, a], [b, a], [a, b], [b, b], [a, a, a], [b, a|...]|_1100], [[a, a, a], [b, a, a]|_1100], [b, a]) ? creep                                         %           p([W|_], _, W).                     % W = [b,a]                                                                                                                                    
   Exit: (11) p([[b], [a, a], [b, a], [a, b], [b, b], [a, a|...], [b|...]|_1100], [[a, b], [b, b], [a, a, a], [b, a, a]|_1100], [b, a]) ? creep                      %         p(Ws, Ls, W).                         % W = [b,a]    W0 = [a,a] Ws = [              [b,a],[a,b],[b,b],[a,a,a],[b,a,a]|Ls]                                                                                                                                
   Exit: (10) p([[a], [b], [a, a], [b, a], [a, b], [b, b], [a|...], [...|...]|...], [[a, a], [b, a], [a, b], [b, b], [a, a, a], [b, a|...]|_1100], [b, a]) ? creep   %       p(Ws, Ls, W).                           % W = [b,a]    W0 = [b]   Ws = [        [a,a],[b,a],[a,b],[b,b],[a,a,a],[b,a,a]|_2372]  Ls = [                                [a,a,a],[b,a,a]|_2372]                                                                                                                                                         
   Exit: (9) p([[], [a], [b], [a, a], [b, a], [a, b], [b|...], [...|...]|...], [[a], [b], [a, a], [b, a], [a, b], [b, b], [a|...], [...|...]|...], [b, a]) ? creep   %     p(Ws, Ls, W).                             % W = [b,a]    W0 = [a]   Ws = [    [b],[a,a],[b,a],[a,b],[b,b],[a,a,a],[b,a,a]|_2372]  Ls = [                    [a,b],[b,b],[a,a,a],[b,a,a]|_2372]                                                                                                                                                           
   Exit: (8) word([b, a]) ? creep                                                                                                                                    %   p(Ws, Ls, W).                               % W = [b,a]    W0 = []    Ws = [[a],[b],[a,a],[b,a],[a,b],[b,b],[a,a,a],[b,a,a]|_2372]  Ls = [        [a,a],[b,a],[a,b],[b,b],[a,a,a],[b,a,a]|_2372]     
W = [b, a] ;                                                                                                                                                         % p([[]|Ls], Ls, W).                            % W = [b,a]                                                                             Ls = [[a],[b],[a,a],[b,a],[a,b],[b,b],[a,a,a],[b,a,a]|_2372] 

回答4:

Normally I would post these as a single answer, but @false asked me to keep them separate.

If you read my comments and answers you will see that I was aware that I had to pass the result from one iteration back into the next iteration. What gave me insight into that was using a cross-product predicate which I found in

"The Craft of Prolog" by Richard A. O'Keefe pg. 243

If you are serious about learning Prolog, the book is a must have.

To quote the Preface

There are a lot of introductory Prolog books around. This is not one of them. Think of it as "second steps in Prolog". If you have already read one of the introductory books, if you have taken an introductory course on Prolog, if you have written ore or two Prolog programs, and if you are wondering why it is still hard to write good Prolog programs, this book is meant to help you. The purpose of the book is to show you how you can write Prolog programs that work, that don't take an unreasonable amount of time, and that are clean enough to show to your friends.

Here is a slight variation that I used for one variation that did not work.

combine(X,Y,[X,Y]).

product(P,Xs,Ys,PXYs) :-
    product1(Xs,Ys,PXYs,P).

product1([],_,[],_).

product1([X|Xs],Ys,PXYs0,P) :-
    product1(Ys,X,P,PXYs0,PXYs1),
    product1(Xs,Ys,PXYs1,P).

product1([],_,_) --> [].

product1([Y|Ys],X,P) -->
    {
        call(P,X,Y,PXY)
    },
    [PXY],
    product1(Ys,X,P).

?- product(combine,[a,b],[a,b],R).
R = [[a, a], [a, b], [b, a], [b, b]].

回答5:

So to clarify, the intended solution is an instance of the following schema?

fact(Args).

recursive_rule(Args0) :-
    recursive_rule(Args1).

word(W) :-
    recursive_rule(Args).

Where each occurrence of an Args variable stands for zero or more terms and presumably (but not necessarily) fact and recursive_rule are actually the same functor?

回答6:

With Guy coder's suggestions this is closer?

unfold([], []).
unfold([H|T], [[a|H], [b|H]|L]) :-
 unfold(T, L).

ab([], [[]]).   
ab([_|N1],L):-
 ab(N1, L1),
 unfold(L1, L).

word(X):-
 length(List,_),
 ab(List,Values),
 member(X,Values).

回答7:

Not a solution, but an insight toward a solution.

This started with using DCG

abs4 --> [].
abs4 --> abs4, ([a] | [b]).

?- phrase(abs4,X).
X = [] ;
X = [a] ;
X = [b] ;
X = [a, a] ;
X = [a, b] ;
X = [b, a] ;
X = [b, b] ;
X = [a, a, a] ;
X = [a, a, b] ;
X = [a, b, a] ;
X = [a, b, b] ;
X = [b, a, a] ;
X = [b, a, b] ;
X = [b, b, a] ;
X = [b, b, b] ;
X = [a, a, a, a] ;
X = [a, a, a, b] ;

then looking at the listing

?- listing(abs4).
abs4(A, A).
abs4(A, C) :-
        abs4(A, B),
        (   B=[a|C]
        ;   B=[b|C]
        ).

and using member to remove the ;.

word5(W) :-
    abs5(W,[]).
abs5(A, A).
abs5(A, C) :-
    abs5(A, [D|C]),
    member5(D,[a,b]).
member5(X, [X|_]).
member5(X, [_|Tail]) :-
  member5(X, Tail).

?- word5(X).
X = [] ;
X = [a] ;
X = [b] ;
X = [a, a] ;
X = [a, b] ;
X = [b, a] ;
X = [b, b] ;
X = [a, a, a] ;
X = [a, a, b] ;
X = [a, b, a] ;
X = [a, b, b] ;
X = [b, a, a]