2

λProlog features hypothetical reasoning. By using the operator (=>)/2 we can temporarily assert some clause. Can this be used to realize adversarial search in λProlog?

Was thinking about Tic-Tac-Toe game. Instead of starting with cell/3 facts that are populated to blank, we could also simply start with no cell/3 facts at all.

And then each player makes a move by adding cell/3 facts. Any corresponding implementations around? I guess they would be adaptations of this code here.

After two moves the database could look like this:

cell(2, 2, x).
cell(1, 1, o).
  • Isn't the advantage of λProlog's hereditary Harrop formulas that you can express (and prove) implications? The expressivity (and even the performance) of having facts (current state, extensional database) in the Prolog database or stashed in a term should be the same; a term can be unpacked into the Prolog database and a term can be constructed from whatever is in the Prolog database before actual proving begins. – David Tonhofer Jan 24 '21 at 09:46
  • With terms you could use arg/3. In database you might need to model things slightly different. So you cannot say its the same. Also in a database solution you don't construct a term before proving begins, you dynamically modify the database while proving. –  Jan 24 '21 at 15:36

1 Answers1

2

It turns out, that for the game search, we only need a special case of hypothetical reasoning which can be implemented in pure Prolog. Lets use the operator (-:)/2 for hypothetical reasoning, then we have this inference rule:

   Γ, F |- G
 -------------
  Γ |- F -: G

So verbally to solve the subgoal F -: G, the fact F is added the the database Γ and then the subgoal G is tried. What is challenging that for every success of G the fact F must disappear again from the database, because what is proved is without F in the database.

The special case we consider is that G is deterministic. That is G either succeeds once or fails. We currently do not assume exceptions or F non-ground as well. Under these assumption hypothetical reasoning can be implemented as follows:

:- op(1200, xfx, -:).

(F -: G) :-
   assertz(F),
   G, !,
   retract(F).
(F -: _) :-
   retract(F), fail.

Its now possible to rewrite the move/3 predicate from here into a predicate move/2 that offers a new fact F. The main adversial search routine then reads as follows, where we have also changed the win/2 and tie/2 predicate accordingly into win/1 and tie/1 to check the dynamic facts cell/3:

best(P, F) :-
   move(P, F),
   (F -: 
     (  win(P) -> true
     ;  other(P, Q),
        \+ tie(Q),
        \+ best(Q, _))).

Here are some results. The first mover has no winning strategy:

?- best(x, F).
false.

If the board is [[x, -, o], [x, -, -], [o, -, -]] the player x has winning strategy:

?- (cell(1,1,x) -: (cell(3,1,o) -: (cell(1,2,x) -: (cell(1,3,o) -: best(x, F))))).
F = cell(2, 2, x).

How performant is assertz/retract compared to a Prolog term game state? ca. 3 times slower:

?- time(best(x, F)).
% 478,598 inferences, 0.094 CPU in 0.094 seconds (100% CPU, 5105045 Lips)
false.

Open source:

Special Case of Hypothetical Reasoning
https://gist.github.com/jburse/279b6280ab4311de456e458a7386c1da#file-hypo-pl

Prolog code for the tic-tac-toe game
Min-max search via negation
Game board via Prolog facts
https://gist.github.com/jburse/279b6280ab4311de456e458a7386c1da#file-tictac2-pl