4

I offered the following clpfd-based code for the recent question Segregating Lists in Prolog:

list_evens_odds([],[],[]).
list_evens_odds([X|Xs],[X|Es],Os) :-
   X mod 2 #= 0,
   list_evens_odds(Xs,Es,Os).
list_evens_odds([X|Xs],Es,[X|Os]) :-
   X mod 2 #= 1,
   list_evens_odds(Xs,Es,Os).

It is concise and pure, but can leave behind many unnecessary choice-points. Consider:

?- list_evens_odds([1,2,3,4,5,6,7],Es,Os).

Above query leaves behind a useless choice-point for every non-odd item in [1,2,3,4,5,6,7].

Alternative implementation

Using the reification technique demonstrated by @false in Prolog union for A U B U C can reduce the number of unnecessary choice-points. The implementation could change to:

list_evens_odds([],[],[]).
list_evens_odds([X|Xs],Es,Os) :-
   if_(#<=>(X mod 2 #= 0), (Es=[X|Es0],Os=   Os0),
                           (Es=   Es0, Os=[X|Os0])),
   list_evens_odds(Xs,Es0,Os0).

To directly interact with clpfd-reification the implementation of if_/3 could be adapted like this:

if_( C_1, Then_0, Else_0) :-
   call(C_1,Truth01),
   indomain(Truth01),
   ( Truth01 == 1 -> Then_0 ; Truth01 == 0, Else_0 ).

Of course, (=)/3 would also need to be adapted to this convention.

The bottom line

So I wonder: Is using 0 and 1 as truth-values instead of false and true a good idea?

Am I missing problems along that road? Help, please! Thank you in advance!

Community
  • 1
  • 1
repeat
  • 18,496
  • 4
  • 54
  • 166
  • 1
    quick fix `..., X mod 2 #= M, if_(M=0, ...`. Also, you might give this other `if_/3` another name, like `if0_/3` – false Apr 07 '15 at 14:25

3 Answers3

1

In SWI-Prolog, you can use zcompare/3:

:- use_module(library(clpfd)).

list_evens_odds([], [], []).
list_evens_odds([X|Xs], Es, Os) :-
      Mod #= X mod 2,
      zcompare(Ord, 0, Mod),
      ord_(Ord, X, Es0, Es, Os0, Os),
      list_evens_odds(Xs, Es0, Os0).

ord_(=, X, Es0, [X|Es0], Os, Os).
ord_(<, X, Es, Es, Os0, [X|Os0]).

Example query:

?- list_evens_odds([1,2,3,4,5,6,7], Es, Os).
Es = [2, 4, 6],
Os = [1, 3, 5, 7].
mat
  • 40,498
  • 3
  • 51
  • 78
  • This looks unnecessarily obscure. Why map {0,1} to {<,=} rather than using it directly in ord_/6? – jschimpf Apr 08 '15 at 15:07
  • This happened because I used your code as the starting point, which uses a reified value for branching. With `zcompare/3`, the reification is no longer needed, so I removed it. – mat Apr 08 '15 at 15:29
  • That's not what I meant, the reification was fine. It's the zcompare that's pointless. You can just use the reification boolean as the 1st argument of ord_/6. – jschimpf Apr 08 '15 at 23:53
  • There are several CLP(FD) systems that do not yet support reification. `zcompare/3` or a similar construct is easier to add to such systems and still provides a declarative solution for such branching in connection with a comparison, so I am using it instead to show how you can provide, without needing to handle many reified predicates, something similar to the `if_/3` construct of the original question within CLP(FD). – mat Apr 10 '15 at 06:56
  • mat: *"There are several CLP(FD) systems that do not yet support reification"* - Really? *"zcompare/3 or a similar construct is easier to add to such systems"* - How so? It is essentially a reified comparison, and no easier to implement. It is not necessary to reinvent the wheel. – jschimpf Apr 10 '15 at 13:40
  • That's incorrect, but not the place to discuss it here. – jschimpf Apr 11 '15 at 01:26
  • Yes, you can still find such systems easily, but I hope they add it in the near future of course. Please also see for example the source of `zcompare/3` in SWI-Prolog: Reification is not needed to implement it. I think this is an important feature, and I also think that getting reification of CLP(FD) constraints right is harder than one may realize at first. For example, you can still easily find cases in current systems (especially involving division by zero) that yield wrong results. – mat Apr 11 '15 at 10:18
  • I agree. I only want to show that getting reification right is far harder than implementing `zcompare/3`, not to show current deficiencies of any specific system, so I have generalized the comment. – mat Apr 11 '15 at 10:20
  • However, what I said was *"zcompare is essentially a reified comparison, and no easier to implement"*, nothing more nothing less. If you want to discuss it seriously, please email me. – jschimpf Apr 11 '15 at 14:45
  • There is a significant difference to full reification: `zcompare/3` does not support compound arithmetic *expressions* as its arguments, but only individual variables or integers. This is the reason why it is much easier to implement than full-fledged reification of arithmetic expressions. CLP(FD) expressions like `X/0`, which is what makes reification harder to implement than one may initially expect, cannot occur in `zcompare/3`. To implement `zcompare/3`, you essentially need only `freeze/2` and a propagator, much less code than for general reification. – mat Apr 11 '15 at 21:34
1

I have reconsidered my proposed "double-use" of if_/3 and I feel like I'm seeing better through it now.

The comments by @false and @lurker and the answer by @mat have had their fair share in aiding my understanding. Thank you!

The "insights" I have gained are by no means dramatic; still I'd like to share them with you:

  1. Adapting if_/3 like I did is do-able and may same some LOC's.
  2. However, it mixes up two concepts that are procedurally quite different from each other: By default, clpfd propagates and then delays. Reified term equality OTOH forces a choice right away.
  3. It is therefore cleaner to separate these two use cases. And of course, "Cleanliness is indeed next to Godliness"...
repeat
  • 18,496
  • 4
  • 54
  • 166
0

The straightforward solution (which works for any reifiable clp(fd) condition) would seem to be

:- use_module(library(clpfd)).

list_evens_odds([],[],[]).
list_evens_odds([X|Xs],Es,Os) :-
   B #<==> (X mod 2 #= 0),
   freeze(B, (B=1 -> Es=[X|Es0],Os=Os0 ; Es=Es0,Os=[X|Os0])),
   list_evens_odds(Xs,Es0,Os0).

Whether 0/1 or true/false are used as truth values doesn't really matter here. The reason the 0/1 convention is preferred in arithmetic solvers is simply that you can easily reuse the truth values in arithmetic constraints, e.g. add them up, etc.

jschimpf
  • 4,904
  • 11
  • 24