examples_in_progress/alphaBeta.mlw

   1 (** {2 Finite set iterators} *)
   2
   3 module Min
   4
   5   use set.Fset
   6   use int.Int
   7
   8   type param
   9
  10   type elt
  11
  12   function cost param elt : int
  13
  14   function min param (fset elt) : int
  15
  16   axiom min_is_a_lower_bound:
  17     forall p: param, s: fset elt.
  18     forall x. mem x s -> cost p x >= min p s
  19
  20   axiom min_appears_in_set:
  21     forall p: param, s: fset elt. not (is_empty s) ->
  22     exists x. mem x s /\ cost p x = min p s
  23
  24 end
  25
  26 theory TwoPlayerGame
  27
  28   use int.Int
  29   use list.List
  30
  31
  32   (** type describing a position in the game. It must include every
  33      needed info, in particular in general it will include whose
  34      turn it is. *)
  35   type position
  36
  37   (** type describing a move *)
  38   type move
  39
  40   (** the initial_position of the game *)
  41   constant initial_position : position
  42
  43   (** gives the list of legal moves in the given position *)
  44   val function legal_moves position : list move
  45
  46   (** [do_move p m] returns the position obtained by doing the move [m]
  47      on position [p].
  48   *)
  49   val function do_move position move : position
  50
  51   (** [position_value p] returns an evaluation of position [p], an
  52      integer [v] between [-infinity] and [+infinity] which is supposed
  53      to be as higher as the position is good FOR THE PLAYER WHO HAS
  54      THE TURN. [v] must be 0 for a position where nobody can win
  55      anymore (draw game). For a position where the player who has the
  56      turn wins, [v] must be between [winning_value] and [infinity],
  57      and if the other player wins, [v] must be between [-infinity] and
  58      [-winning_value].
  59   *)
  60   constant winning_value : int
  61   val constant infinity : int
  62   val function position_value position : int
  63
  64   axiom position_value_bound :
  65     forall p:position. - infinity < position_value p < infinity
  66
  67   (*
  68
  69     [minmax p d] returns the min-max evaluation of position [p] at depth [d].
  70     As for [position_value], the value is for the player who has the turn.
  71
  72   *)
  73   val function minmax position int : int
  74
  75   axiom minmax_depth_0 :
  76     forall p:position. minmax p 0 = position_value p
  77
  78   type param = (position,int)
  79   function cost (p:param) (m:move) : int =
  80     match p with (p,n) -> minmax (do_move p m) n
  81     end
  82
  83   clone import Min as MinMaxRec with
  84     type param = param,
  85     type elt = move,
  86     function cost = cost
  87
  88   use list.Elements
  89   use set.Fset
  90
  91   axiom minmax_depth_non_zero:
  92     forall p:position, n:int. n > 0 ->
  93      minmax p n =
  94         let moves = Elements.elements (legal_moves p) in
  95         if Fset.is_empty moves then position_value p else
  96           - MinMaxRec.min (p,n-1) moves
  97
  98   use list.Mem
  99
 100   goal Test:
 101     forall p:position, m:move.
 102       let moves = legal_moves p in
 103       Mem.mem m moves -> - (position_value (do_move p m)) <= minmax p 1
 104
 105
 106   lemma minmax_bound:
 107     forall p:position, d:int.
 108       d >= 0 -> - infinity < minmax p d < infinity
 109
 110   lemma minmax_nomove :
 111     forall p:position, d:int.
 112       d >= 0 /\ legal_moves p = Nil ->
 113          minmax p d = position_value p
 114 end
 115
 116
 117 (*
 118
 119    alpha-beta
 120
 121 *)
 122
 123 module AlphaBeta
 124
 125   use int.Int
 126   use int.MinMax
 127
 128   use TwoPlayerGame as G
 129   use list.List
 130   use list.Elements
 131   use set.Fset
 132
 133   let rec move_value_alpha_beta alpha beta pos depth move =
 134     requires { depth >= 1 }
 135     ensures  {
 136       let pos' = G.do_move pos move in
 137       let m = G.minmax pos' (depth-1) in
 138       if - beta < m < - alpha then result = - m
 139       else if m <= - beta then result >= beta
 140       else result <= alpha }
 141     variant { depth, 0 }
 142     let pos' = G.do_move pos move in
 143     let s = negabeta (-beta) (-alpha) pos' (depth-1)
 144     in -s
 145
 146   with negabeta alpha beta pos depth =
 147     requires { depth >= 0 }
 148     ensures  {
 149       if alpha < G.minmax pos depth < beta then result = G.minmax pos depth else
 150       if G.minmax pos depth <= alpha then result <= alpha else
 151       result >= beta }
 152     variant { depth, 1 }
 153     if depth = 0 then G.position_value pos else
 154     let l = G.legal_moves pos in
 155     match l with
 156       | Nil -> G.position_value pos
 157       | Cons m l ->
 158           let best =
 159             move_value_alpha_beta alpha beta pos depth m
 160           in
 161           if best >= beta then best else
 162             negabeta_rec (max best alpha) beta pos depth best l
 163     end
 164
 165   with negabeta_rec alpha beta pos depth best l =
 166     requires { depth >= 1 }
 167     ensures {
 168       let moves = Elements.elements l in
 169       if Fset.is_empty moves then result = best else
 170       let m = G.MinMaxRec.min (pos,depth) moves in
 171       if alpha < m < beta then result = m
 172       else if m <= alpha then result <= alpha else
 173       result >= beta }
 174     variant { depth, 1, l }
 175     match l with
 176       | Nil -> best
 177       | Cons c l ->
 178           let s =
 179             move_value_alpha_beta alpha beta pos depth c
 180           in
 181           let new_best  = max s best in
 182           if new_best >= beta then new_best else
 183             negabeta_rec (max new_best alpha) beta pos depth new_best l
 184     end
 185
 186 (* alpha-beta at a given depth *)
 187
 188 let alpha_beta pos depth =
 189   requires { depth >= 0 }
 190   ensures  { result = G.minmax pos depth }
 191   negabeta (-G.infinity) G.infinity pos depth
 192
 193 (* iterative deepening *)
 194
 195 (*
 196   let best_move_alpha_beta pos =
 197     let l =
 198       List.map
 199         (fun c ->
 200            (move_value_alpha_beta (-G.infinity) G.infinity pos 2 0 c,c))
 201         (G.legal_moves pos)
 202     in
 203     if List.length l < 2 then l else
 204       let current_best_moves =
 205         ref
 206           (List.sort (fun (x,_) (y,_) -> compare y x) l)
 207       in
 208       try
 209         for max_depth = 3 to 1000 do
 210           begin
 211             match !current_best_moves with
 212               | (v1,_)::(v2,_)::_ ->
 213                   if v1 >= G.winning_value or v2 <= - G.winning_value
 214                   then raise Timeout
 215               | _ -> assert false
 216           end;
 217           let l =
 218             List.map
 219               (fun c ->
 220                  (move_value_alpha_beta (-G.infinity) G.infinity
 221                     pos max_depth 0 c,c))
 222               (G.legal_moves pos)
 223           in
 224           current_best_moves :=
 225           (List.sort (fun (x,_) (y,_) -> compare y x) l)
 226         done;
 227         !current_best_moves
 228       with
 229         | Timeout -> !current_best_moves
 230
 231 *)
 232
 233 end