Skip to content

Alpha–beta pruning

InductiveGame tree#✓fully proved

A game tree with values in a type \(\alpha\) is either a leaf, which carries a value in \(\alpha\) (the value of a terminal position), or an inner node, which carries a finite list of game trees (the positions reachable in one move; the list may be empty). Game trees are built inductively, so every game tree is finite.

inductive GameTree (α : Type u) where
  | leaf : α → GameTree α
  | node : List (GameTree α) → GameTree α
Used by 16
Used byAlpha-beta pruning · Alpha-beta with the full window returns the minimax value · Alpha-beta is exact inside the window · Alpha-beta fails low when the minimax value is at most the lower bound · Alpha-beta scan of the children · The minimizer's alpha-beta scan stays at or below its upper bound · Correctness of the alpha-beta scan · Cost of the alpha-beta scan · Alpha-beta is correct · Alpha-beta never evaluates more leaves than the tree has · Lower bound for the maximizer's scan · Alpha-beta at or above the top of the window · Number of leaves · Number of leaves of a list of game trees · Minimax value · Minimax value of a list of positions

DefinitionNumber of leaves#✓fully proved

The number of leaves of a game tree is defined recursively: a leaf counts \(1\), and an inner node counts the total number of leaves of its children (so an inner node without children counts \(0\)).

def leaves : GameTree α → ℕ
  | .leaf _ => 1
  | .node ts => leavesList ts
Uses 1 · Used by 2
Statement usesGame tree
Used byCost of the alpha-beta scan · Alpha-beta never evaluates more leaves than the tree has

DefinitionNumber of leaves of a list of game trees#✓fully proved

The number of leaves of a finite list of game trees is the sum of the numbers of leaves of its members (\(0\) for the empty list).

def leavesList : List (GameTree α) → ℕ
  | [] => 0
  | t :: ts => leaves t + leavesList ts
Uses 1 · Used by 2
Statement usesGame tree
Used byCost of the alpha-beta scan · Alpha-beta never evaluates more leaves than the tree has

DefinitionAlpha-beta pruning#✓fully proved

For a player \(p\) to move and values \(a\) and \(b\) in a linear order, alpha-beta pruning with window \([a, b]\) returns the value of a leaf at a cost of one unit (one leaf evaluation), and on an inner node runs the alpha-beta scan of its children for \(p\) with window \([a, b]\).

def alphaBeta : Bool → α → α → GameTree α → TimeM ℕ α
  | _, _, _, .leaf x => do
      TimeM.tick 1
      pure x
  | p, a, b, .node ts => alphaBetaList p a b ts
Uses 1 · Used by 10
Statement usesGame tree
Used byAlpha-beta with the full window returns the minimax value · Alpha-beta is exact inside the window · Alpha-beta fails low when the minimax value is at most the lower bound · The minimizer's alpha-beta scan stays at or below its upper bound · Correctness of the alpha-beta scan · Cost of the alpha-beta scan · Alpha-beta is correct · Alpha-beta never evaluates more leaves than the tree has · Lower bound for the maximizer's scan · Alpha-beta at or above the top of the window

DefinitionAlpha-beta scan of the children#✓fully proved

Given the player \(p\) to move, values \(a\) and \(b\) in a linear order and a list of game trees (the children of a position), the scan runs alpha-beta pruning for the other player on the children in order, each time with the current bounds \(a\) and \(b\). The maximizer replaces \(a\) by \(\max(a, v)\), where \(v\) is the child's returned value, and stops as soon as \(b \le a\), returning the new \(a\); if it never stops early it returns the final \(a\) (\(a\) itself for an empty list). The minimizer replaces \(b\) by \(\min(b, v)\) and stops as soon as \(b \le a\), returning the new \(b\); if it never stops early it returns the final \(b\) (\(b\) itself for an empty list). The cost of the scan is the total cost of the children it evaluates.

def alphaBetaList : Bool → α → α → List (GameTree α) → TimeM ℕ α
  | true, a, _, [] => pure a
  | false, _, b, [] => pure b
  | true, a, b, t :: ts => do
      let v ← alphaBeta false a b t
      let a' := max a v
      if b ≤ a' then pure a' else alphaBetaList true a' b ts
  | false, a, b, t :: ts => do
      let v ← alphaBeta true a b t
      let b' := min b v
      if b' ≤ a then pure b' else alphaBetaList false a b' ts
Uses 1 · Used by 6
Statement usesGame tree
Used byThe minimizer's alpha-beta scan stays at or below its upper bound · Correctness of the alpha-beta scan · Cost of the alpha-beta scan · Alpha-beta is correct · Alpha-beta never evaluates more leaves than the tree has · Lower bound for the maximizer's scan
17 fully proved

Scan bounds and order facts

TheoremLower bound for the maximizer's scan#✓fully proved

Let values lie in a linear order. For all values \(a\) and \(b\) and every finite list of game trees, the value returned by the alpha-beta scan of the list with the maximizer to move and window \([a, b]\) is at least \(a\).

theorem le_alphaBetaList_true (a b : α) :
    ∀ ts : List (GameTree α), a ≤ (alphaBetaList true a b ts).ret
Uses 3 · Used by 2
Statement usesGame tree · Alpha-beta scan of the children
Proof usesAlpha-beta pruning
Used byCorrectness of the alpha-beta scan · Alpha-beta is correct

TheoremThe minimizer's alpha-beta scan stays at or below its upper bound#✓fully proved

For all values \(a, b\) in a linear order and every list \(ts\) of game trees, the value returned by the alpha-beta scan of \(ts\) for the minimizer with lower bound \(a\) and upper bound \(b\) is at most \(b\).

theorem alphaBetaList_false_le (a b : α) :
    ∀ ts : List (GameTree α), (alphaBetaList false a b ts).ret ≤ b
Uses 3 · Used by 2
Statement usesGame tree · Alpha-beta scan of the children
Proof usesAlpha-beta pruning
Used byCorrectness of the alpha-beta scan · Alpha-beta is correct

Cost

TheoremAlpha-beta never evaluates more leaves than the tree has#✓fully proved

For either player \(p\) to move and all values \(a, b\) in a linear order, alpha-beta pruning run on a game tree \(t\) for \(p\) with window \([a, b]\) evaluates at most as many leaves as \(t\) has, each leaf evaluation costing one unit.

theorem alphaBeta_time_le : ∀ (p : Bool) (a b : α) (t : GameTree α),
    (alphaBeta p a b t).time ≤ leaves t
Uses 5
Statement usesGame tree · Alpha-beta pruning · Number of leaves
Proof usesAlpha-beta scan of the children · Number of leaves of a list of game trees

TheoremCost of the alpha-beta scan#✓fully proved

For either player \(p\), all values \(a, b\) in a linear order and every list \(ts\) of game trees, the alpha-beta scan of \(ts\) for \(p\) with lower bound \(a\) and upper bound \(b\) evaluates at most as many leaves as the trees in \(ts\) have in total, each leaf evaluation costing one unit.

theorem alphaBetaList_time_le : ∀ (p : Bool) (a b : α) (ts : List (GameTree α)),
    (alphaBetaList p a b ts).time ≤ leavesList ts
Uses 5
Statement usesGame tree · Alpha-beta scan of the children · Number of leaves of a list of game trees
Proof usesAlpha-beta pruning · Number of leaves

The minimax value; from here on the order is bounded

DefinitionMinimax value#✓fully proved

Let values lie in a bounded linear order. The minimax value of a game tree with player \(p\) to move (the maximizer or the minimizer) is defined recursively: a leaf is worth the value it carries; an inner node is worth, for the maximizer, the maximum of the minimax values of its children with the minimizer to move, and for the minimizer, the minimum of the minimax values of its children with the maximizer to move. An inner node without children is worth \(\bot\) to the maximizer and \(\top\) to the minimizer.

def minimax : Bool → GameTree α → α
  | _, .leaf x => x
  | p, .node ts => minimaxList p ts
Uses 1 · Used by 6
Statement usesGame tree
Used byAlpha-beta with the full window returns the minimax value · Alpha-beta is exact inside the window · Alpha-beta fails low when the minimax value is at most the lower bound · Correctness of the alpha-beta scan · Alpha-beta is correct · Alpha-beta at or above the top of the window

DefinitionMinimax value of a list of positions#✓fully proved

Let values lie in a bounded linear order. For a player \(p\) and a finite list of game trees, the value for \(p\) is the best of their minimax values with the other player to move: for the maximizer, the maximum of these values, or \(\bot\) if the list is empty; for the minimizer, the minimum of these values, or \(\top\) if the list is empty.

def minimaxList : Bool → List (GameTree α) → α
  | true, [] => ⊥
  | false, [] => ⊤
  | true, t :: ts => max (minimax false t) (minimaxList true ts)
  | false, t :: ts => min (minimax true t) (minimaxList false ts)
Uses 1 · Used by 2
Statement usesGame tree
Used byCorrectness of the alpha-beta scan · Alpha-beta is correct

Correctness

TheoremAlpha-beta is correct#✓fully proved

Alpha-beta is correct (Knuth and Moore 1975, Theorem 1): for a ≤ b, the result of alpha-beta agrees with the minimax value after clamping both to the window [a, b].

theorem alphaBeta_spec : ∀ (p : Bool) (a b : α) (t : GameTree α), a ≤ b →
    max a (min b (alphaBeta p a b t).ret) = max a (min b (minimax p t))
Uses 7 · Used by 4
Statement usesGame tree · Alpha-beta pruning · Minimax value
Proof usesAlpha-beta scan of the children · The minimizer's alpha-beta scan stays at or below its upper bound · Lower bound for the maximizer's scan · Minimax value of a list of positions
Used byAlpha-beta with the full window returns the minimax value · Alpha-beta is exact inside the window · Alpha-beta fails low when the minimax value is at most the lower bound · Alpha-beta at or above the top of the window

TheoremCorrectness of the alpha-beta scan#✓fully proved

Let \(p\) be the player to move, \(ts\) a list of game trees with values in a bounded linear order, and \(a \le b\). Let \(r\) be the value returned by the alpha-beta scan of \(ts\) for \(p\) with window \([a, b]\), and let \(m\) be the best value for \(p\) among \(ts\): the maximum of the minimax values of the trees in \(ts\) for the minimizer (\(\bot\) if \(ts\) is empty) when \(p\) is the maximizer, and the minimum of their minimax values for the maximizer (\(\top\) if \(ts\) is empty) when \(p\) is the minimizer. Then \(\max(a, \min(b, r)) = \max(a, \min(b, m))\).

theorem alphaBetaList_spec : ∀ (p : Bool) (a b : α) (ts : List (GameTree α)), a ≤ b →
    max a (min b (alphaBetaList p a b ts).ret) = max a (min b (minimaxList p ts))
Uses 7
Statement usesGame tree · Alpha-beta scan of the children · Minimax value of a list of positions
Proof usesAlpha-beta pruning · The minimizer's alpha-beta scan stays at or below its upper bound · Lower bound for the maximizer's scan · Minimax value

TheoremAlpha-beta fails low when the minimax value is at most the lower bound#✓fully proved

Let \(t\) be a game tree with values in a bounded linear order, \(p\) the player to move and \(a < b\) values. If the minimax value of \(t\) for \(p\) is at most \(a\), then alpha-beta pruning run on \(t\) for \(p\) with the window \([a, b]\) returns a value at most \(a\).

theorem alphaBeta_le_of_minimax_le {p : Bool} {a b : α} {t : GameTree α} (hab : a < b)
    (h : minimax p t ≤ a) : (alphaBeta p a b t).ret ≤ a
Uses 4
Statement usesGame tree · Alpha-beta pruning · Minimax value
Proof usesAlpha-beta is correct

TheoremAlpha-beta is exact inside the window#✓fully proved

Let \(t\) be a game tree with values in a bounded linear order, \(p\) the player to move and \(a, b\) values. If the minimax value \(v\) of \(t\) for \(p\) satisfies \(a < v < b\), then alpha-beta pruning run on \(t\) for \(p\) with the window \([a, b]\) returns exactly \(v\).

theorem alphaBeta_eq_of_mem_window {p : Bool} {a b : α} {t : GameTree α}
    (ha : a < minimax p t) (hb : minimax p t < b) : (alphaBeta p a b t).ret = minimax p t
Uses 4
Statement usesGame tree · Alpha-beta pruning · Minimax value
Proof usesAlpha-beta is correct

TheoremAlpha-beta at or above the top of the window#✓fully proved

Let values lie in a bounded linear order, let \(t\) be a game tree, let \(p\) be a player, and let \(a < b\). If the minimax value of \(t\) with \(p\) to move is at least \(b\), then the value returned by alpha-beta pruning on \(t\) with \(p\) to move and window \([a, b]\) is at least \(b\).

theorem le_alphaBeta_of_le_minimax {p : Bool} {a b : α} {t : GameTree α} (hab : a < b)
    (h : b ≤ minimax p t) : b ≤ (alphaBeta p a b t).ret
Uses 4
Statement usesGame tree · Alpha-beta pruning · Minimax value
Proof usesAlpha-beta is correct

TheoremAlpha-beta with the full window returns the minimax value#✓fully proved

Let \(t\) be a game tree whose values lie in a bounded linear order with least element \(\bot\) and greatest element \(\top\). For either player \(p\) to move, alpha-beta pruning run on \(t\) for \(p\) with the window \([\bot, \top]\) returns exactly the minimax value of \(t\) for \(p\).

theorem alphaBeta_bot_top (p : Bool) (t : GameTree α) :
    (alphaBeta p ⊥ ⊤ t).ret = minimax p t
Uses 4
Statement usesGame tree · Alpha-beta pruning · Minimax value
Proof usesAlpha-beta is correct

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.