Alpha-Beta Pruning

Reference: Donald E. Knuth, Ronald W. Moore, An analysis of alpha-beta pruning, Artificial Intelligence, Volume 6, Issue 4, 1975.

module AlphaBeta

use int.Int
use int.MinMax
use list.List

type position

val constant inf: int
  ensures { 0 < result }

val function eval_position (_: position) : (v: int)
  ensures { -inf <= v <= inf }

A game tree is a position and a list of sub-game trees.

type game = Node position (list game)

The full evaluation of a game tree is its maximin value. This is the specification of the value we intend to compute.

let rec function eval (g: game) : (v: int)
  variant { g }
  ensures { -inf <= v <= inf }
= match g with
  | Node p Nil -> eval_position p
  | Node _ gl  -> eval_list gl
  end

with function eval_list (gl: list game) : (v: int)
  variant { gl }
  ensures { -inf <= v <= inf }
= match gl with
  | Nil       -> -inf
  | Cons g gl -> max (- eval g) (eval_list gl)
  end

The alpha-beta pruning procedure

let rec alpha_beta_g (a b: int) (g: game) : (v: int)
  requires { -inf <= a < b <= inf }
  variant { g }
  ensures { -inf <= v <= inf }
  ensures { eval g < a                         -> v <= a      }
  ensures {          a <= eval g <= b          -> v =  eval g }
  ensures {                         b < eval g -> v >= b      }
= match g with
  | Node p Nil -> eval_position p
  | Node _ gl  -> alpha_beta_l a b gl
  end

with alpha_beta_l (a b: int) (gl: list game) : (v: int)
  requires { -inf <= a < b <= inf }
  variant  { gl }
  ensures  { a <= v <= inf }
  ensures  { if eval_list gl <= b then v = max a (eval_list gl) else b <= v }
= match gl with
  | Nil ->
      a
  | Cons g gl ->
      let a = max a (- alpha_beta_g (-b) (-a) g) in
      if a >= b then a else alpha_beta_l a b gl
  end

Running alpha-beta with bounds -inf and inf returns the maximin value.

let alpha_beta (g: game) : (v: int)
  ensures { v = eval g }
= alpha_beta_g (-inf) inf g

end