How to reason formally about optimisation in games?

Stream: Program verification

[Kabelo Moiloa]

What's the best way to learn how to formalise things like the alpha-beta pruning method for playing optimal moves in finite perfect information games, in an imperative context? I'm particularly interested in the equivalence between recursion and using a stack of postponed tasks, I'm finding it hard to formulate the usual Hoare triple style proof of correctness of that algorithm precisely. Also, in some puzzles one might want to solve one can share memory instead of copying the game state every time one wants to explore a new case, I'd be interested to see how one might reason about that too.

[GasStationManager]

Do you have in mind a particular implementation of alpha beta? I imagine that to prove optimality, you'd define the optimal value as the result of running a plain minimax search. So the proof task amounts to showing that the two algorithms return the same value, given the same game tree.

[GasStationManager]

As for equivalence of recursion and stack of tasks, that sounds like a general fact about recursion that is orthogonal to the particulars of alpha beta. In any case it'd be easier to prove optimality using the recursive versions of the algorithms