Reference · Algorithm guarantees

rainbow.algorithms.proofs.minimax

Algorithm guaranteessrc/rainbow/algorithms/proofs/minimax.clj1 definitions, 3 theorems

AHoF adversarial decision-making -- the minimax value of a two-ply zero-sum game. The maximizing player chooses among moves; the adversary then chooses the worst (minimizing) reply to each. The value is the max over the player's moves of the min over the adversary's replies: value a b c d = max( min(a, b), min(c, d) ) for a game where move 1 has replies (a, b) and move 2 has replies (c, d), the payoffs being exact nonnegative rationals. Both nnrat-min and nnrat-max use the decidable rational order. Proved: worked instances with replies (3,1) and (2,4) -- the minimax value is 2, and the worked certificates min(2,4) <= value and min(3,1) <= value. The game tree and move enumeration are executable concerns; what is proved here is the minimax combination at this instance. The classical security guarantee (committing to the best move secures at least the value against any reply) is not proved here. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and logic/if-data (all carried by the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.minimax` prints this classification.

minimax/value :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

minimax/value-example :
  → minimax/value 3 1 2 4 = 2

minimax/value-secures-best-move :
  → logic/if-data ℚ≥0 (audit/decide-nnrat-at-most 2 4 = audit/decide-nnrat-at-most 2 4) (audit/decide-nnrat-at-most 2 4) 2 4 ≤ minimax/value 3 1 2 4

minimax/value-dominates-other-move :
  → logic/if-data ℚ≥0 (audit/decide-nnrat-at-most 3 1 = audit/decide-nnrat-at-most 3 1) (audit/decide-nnrat-at-most 3 1) 3 1 ≤ minimax/value 3 1 2 4