alphaBeta.mlw 5.25 KB
 MARCHE Claude committed Aug 24, 2012 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 committed Aug 24, 2012 23 `````` on position [p]. `````` MARCHE Claude committed Aug 24, 2012 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 committed Aug 24, 2012 40 `````` axiom position_value_bound : `````` MARCHE Claude committed Aug 24, 2012 41 `````` forall p:position. - infinity < position_value p < infinity `````` MARCHE Claude committed Aug 24, 2012 42 `````` `````` MARCHE Claude committed Aug 24, 2012 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 committed Aug 24, 2012 59 `````` clone import set.Min as MinMaxRec with `````` MARCHE Claude committed Aug 24, 2012 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: `````` MARCHE Claude committed Aug 24, 2012 68 69 `````` forall p:position, n:int. n > 0 -> minmax p n = `````` MARCHE Claude committed Aug 24, 2012 70 71 `````` let moves = Elements.elements (legal_moves p) in if Fset.is_empty moves then position_value p else `````` MARCHE Claude committed Aug 24, 2012 72 `````` - MinMaxRec.min (p,n-1) moves `````` MARCHE Claude committed Aug 24, 2012 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 committed Aug 24, 2012 81 82 83 `````` lemma minmax_bound: forall p:position, d:int. `````` MARCHE Claude committed Aug 24, 2012 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 committed Aug 24, 2012 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 committed Aug 24, 2012 106 107 `````` use list.Elements use set.Fset `````` MARCHE Claude committed Aug 24, 2012 108 `````` `````` MARCHE Claude committed Aug 24, 2012 109 `````` let rec move_value_alpha_beta alpha beta pos depth move = `````` Andrei Paskevich committed Oct 13, 2012 110 111 112 `````` requires { depth >= 1 } ensures { let pos' = G.do_move pos move in `````` MARCHE Claude committed Aug 24, 2012 113 `````` let m = G.minmax pos' (depth-1) in `````` MARCHE Claude committed Aug 24, 2012 114 115 `````` if - beta < m < - alpha then result = - m else if m <= - beta then result >= beta `````` Andrei Paskevich committed Oct 13, 2012 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 committed Aug 24, 2012 120 121 `````` with negabeta alpha beta pos depth = `````` Andrei Paskevich committed Oct 13, 2012 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 committed Aug 24, 2012 127 `````` if depth = 0 then G.position_value pos else `````` MARCHE Claude committed Aug 24, 2012 128 129 130 `````` let l = G.legal_moves pos in match l with | Nil -> G.position_value pos `````` MARCHE Claude committed Aug 24, 2012 131 `````` | Cons m l -> `````` MARCHE Claude committed Aug 24, 2012 132 `````` let best = `````` MARCHE Claude committed Aug 24, 2012 133 `````` move_value_alpha_beta alpha beta pos depth m `````` MARCHE Claude committed Aug 24, 2012 134 135 `````` in if best >= beta then best else `````` MARCHE Claude committed Aug 24, 2012 136 `````` negabeta_rec (max best alpha) beta pos depth best l `````` MARCHE Claude committed Aug 24, 2012 137 138 `````` end `````` MARCHE Claude committed Aug 24, 2012 139 `````` with negabeta_rec alpha beta pos depth best l = `````` Andrei Paskevich committed Oct 13, 2012 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 committed Aug 24, 2012 148 149 150 151 `````` match l with | Nil -> best | Cons c l -> let s = `````` MARCHE Claude committed Aug 24, 2012 152 `````` move_value_alpha_beta alpha beta pos depth c `````` MARCHE Claude committed Aug 24, 2012 153 154 155 `````` in let new_best = max s best in if new_best >= beta then new_best else `````` MARCHE Claude committed Aug 24, 2012 156 `````` negabeta_rec (max new_best alpha) beta pos depth new_best l `````` MARCHE Claude committed Aug 24, 2012 157 158 159 160 `````` end (* alpha-beta at a given depth *) `````` MARCHE Claude committed Aug 24, 2012 161 ``````let alpha_beta pos depth = `````` Andrei Paskevich committed Oct 13, 2012 162 163 `````` requires { depth >= 0 } ensures { result = G.minmax pos depth } `````` MARCHE Claude committed Aug 24, 2012 164 `````` negabeta (-G.infinity) G.infinity pos depth `````` MARCHE Claude committed Aug 24, 2012 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 committed Aug 24, 2012 182 `````` for max_depth = 3 to 1000 do `````` MARCHE Claude committed Aug 24, 2012 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 committed Aug 24, 2012 194 `````` pos max_depth 0 c,c)) `````` MARCHE Claude committed Aug 24, 2012 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``````