alphaBeta.mlw 5.25 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22

theory TwoPlayerGame

  use import int.Int
  use import list.List


  (** type describing a position in the game. It must include every
     needed info, in particular in general it will include whose
     turn it is. *)
  type position

  (** type describing a move *)
  type move

  (** the initial_position of the game *)
  constant initial_position : position

  (** gives the list of legal moves in the given position *)
  function legal_moves position : list move

  (** [do_move p m] returns the position obtained by doing the move [m]
MARCHE Claude's avatar
MARCHE Claude committed
23
     on position [p].
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
  *)
  function do_move position move : position

  (** [position_value p] returns an evaluation of position [p], an
     integer [v] between [-infinity] and [+infinity] which is supposed
     to be as higher as the position is good FOR THE PLAYER WHO HAS
     THE TURN. [v] must be 0 for a position where nobody can win
     anymore (draw game). For a position where the player who has the
     turn wins, [v] must be between [winning_value] and [infinity],
     and if the other player wins, [v] must be between [-infinity] and
     [-winning_value].
  *)
  constant winning_value : int
  constant infinity : int
  function position_value position : int

MARCHE Claude's avatar
MARCHE Claude committed
40
  axiom position_value_bound :
41
    forall p:position. - infinity < position_value p < infinity
MARCHE Claude's avatar
MARCHE Claude committed
42

MARCHE Claude's avatar
MARCHE Claude committed
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
  (*

    [minmax p d] returns the min-max evaluation of position [p] at depth [d].
    As for [position_value], the value is for the player who has the turn.

  *)
  function minmax position int : int

  axiom minmax_depth_0 :
    forall p:position. minmax p 0 = position_value p

  type param = (position,int)
  function cost (p:param) (m:move) : int =
    match p with (p,n) -> minmax (do_move p m) n
    end

MARCHE Claude's avatar
MARCHE Claude committed
59
  clone import set.Min as MinMaxRec with
MARCHE Claude's avatar
MARCHE Claude committed
60 61 62 63 64 65 66 67
    type param = param,
    type elt = move,
    function cost = cost

  use list.Elements
  use set.Fset

  axiom minmax_depth_non_zero:
68 69
    forall p:position, n:int. n > 0 ->
     minmax p n =
MARCHE Claude's avatar
MARCHE Claude committed
70 71
        let moves = Elements.elements (legal_moves p) in
        if Fset.is_empty moves then position_value p else
72
          - MinMaxRec.min (p,n-1) moves
MARCHE Claude's avatar
MARCHE Claude committed
73 74 75 76 77 78 79 80

  use list.Mem

  goal Test:
    forall p:position, m:move.
      let moves = legal_moves p in
      Mem.mem m moves -> - (position_value (do_move p m)) <= minmax p 1

MARCHE Claude's avatar
MARCHE Claude committed
81 82 83

  lemma minmax_bound:
    forall p:position, d:int.
84 85 86 87 88 89
      d >= 0 -> - infinity < minmax p d < infinity

  lemma minmax_nomove :
    forall p:position, d:int.
      d >= 0 /\ legal_moves p = Nil ->
         minmax p d = position_value p
MARCHE Claude's avatar
MARCHE Claude committed
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
end


(*

   alpha-beta

*)

module AlphaBeta

  use import int.Int
  use import int.MinMax

  use TwoPlayerGame as G
  use import list.List
MARCHE Claude's avatar
MARCHE Claude committed
106 107
  use list.Elements
  use set.Fset
MARCHE Claude's avatar
MARCHE Claude committed
108

MARCHE Claude's avatar
MARCHE Claude committed
109
  let rec move_value_alpha_beta alpha beta pos depth move =
110 111 112
    requires { depth >= 1 }
    ensures  {
      let pos' = G.do_move pos move in
MARCHE Claude's avatar
MARCHE Claude committed
113
      let m = G.minmax pos' (depth-1) in
114 115
      if - beta < m < - alpha then result = - m
      else if m <= - beta then result >= beta
116 117 118 119
      else result <= alpha }
    let pos' = G.do_move pos move in
    let s = negabeta (-beta) (-alpha) pos' (depth-1)
    in -s
MARCHE Claude's avatar
MARCHE Claude committed
120 121

  with negabeta alpha beta pos depth =
122 123 124 125 126
    requires { depth >= 0 }
    ensures  {
      if alpha < G.minmax pos depth < beta then result = G.minmax pos depth else
      if G.minmax pos depth <= alpha then result <= alpha else
      result >= beta }
MARCHE Claude's avatar
MARCHE Claude committed
127
    if depth = 0 then G.position_value pos else
MARCHE Claude's avatar
MARCHE Claude committed
128 129 130
    let l = G.legal_moves pos in
    match l with
      | Nil -> G.position_value pos
MARCHE Claude's avatar
MARCHE Claude committed
131
      | Cons m l ->
MARCHE Claude's avatar
MARCHE Claude committed
132
	  let best =
MARCHE Claude's avatar
MARCHE Claude committed
133
	    move_value_alpha_beta alpha beta pos depth m
MARCHE Claude's avatar
MARCHE Claude committed
134 135
	  in
	  if best >= beta then best else
MARCHE Claude's avatar
MARCHE Claude committed
136
	    negabeta_rec (max best alpha) beta pos depth best l
MARCHE Claude's avatar
MARCHE Claude committed
137 138
    end

MARCHE Claude's avatar
MARCHE Claude committed
139
  with negabeta_rec alpha beta pos depth best l =
140 141 142 143 144 145 146 147
    requires { depth >= 1 }
    ensures {
      let moves = Elements.elements l in
      if Fset.is_empty moves then result = best else
      let m = G.MinMaxRec.min (pos,depth) moves in
      if alpha < m < beta then result = m
      else if m <= alpha then result <= alpha else
      result >= beta }
MARCHE Claude's avatar
MARCHE Claude committed
148 149 150 151
    match l with
      |	Nil -> best
      | Cons c l ->
	  let s =
MARCHE Claude's avatar
MARCHE Claude committed
152
            move_value_alpha_beta alpha beta pos depth c
MARCHE Claude's avatar
MARCHE Claude committed
153 154 155
          in
	  let new_best  = max s best in
	  if new_best >= beta then new_best else
MARCHE Claude's avatar
MARCHE Claude committed
156
   	    negabeta_rec (max new_best alpha) beta pos depth new_best l
MARCHE Claude's avatar
MARCHE Claude committed
157 158 159 160
    end

(* alpha-beta at a given depth *)

MARCHE Claude's avatar
MARCHE Claude committed
161
let alpha_beta pos depth =
162 163
  requires { depth >= 0 }
  ensures  { result = G.minmax pos depth }
MARCHE Claude's avatar
MARCHE Claude committed
164
  negabeta (-G.infinity) G.infinity pos depth
MARCHE Claude's avatar
MARCHE Claude committed
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181

(* iterative deepening *)

(*
  let best_move_alpha_beta pos =
    let l =
      List.map
	(fun c ->
	   (move_value_alpha_beta (-G.infinity) G.infinity pos 2 0 c,c))
	(G.legal_moves pos)
    in
    if List.length l < 2 then l else
      let current_best_moves =
	ref
	  (List.sort (fun (x,_) (y,_) -> compare y x) l)
      in
      try
MARCHE Claude's avatar
MARCHE Claude committed
182
	for max_depth = 3 to 1000 do
MARCHE Claude's avatar
MARCHE Claude committed
183 184 185 186 187 188 189 190 191 192 193
	  begin
	    match !current_best_moves with
	      | (v1,_)::(v2,_)::_ ->
		  if v1 >= G.winning_value or v2 <= - G.winning_value
		  then raise Timeout
	      | _ -> assert false
	  end;
	  let l =
	    List.map
	      (fun c ->
		 (move_value_alpha_beta (-G.infinity) G.infinity
MARCHE Claude's avatar
MARCHE Claude committed
194
		    pos max_depth 0 c,c))
MARCHE Claude's avatar
MARCHE Claude committed
195 196 197 198 199 200 201 202 203 204 205 206
	      (G.legal_moves pos)
	  in
	  current_best_moves :=
	  (List.sort (fun (x,_) (y,_) -> compare y x) l)
	done;
	!current_best_moves
      with
	| Timeout -> !current_best_moves

*)

end