Функція Шпрага-Гранді
Функція Шпрага-Гранді широко використовується в теорії ігор для знаходження виграшної стратегії в комбінаційних іграх, наприклад, гра Нім. Дана функція визначається для ігор з двома гравцями, в яких програє той, який не має можливості зі своєї позиції зробити черговий крок. Теорема була незалежно сформульована й доведена Р. Шпрагом (1935) та П.М. Гранді (1939).
Гра "Нім"
Опис гри
Дано N купок, в кожній з яких певна додатна каменів. Кожен гравець по черзі бере з купки декілька камінців, коли всі купки стають порожніми, то гра завершується поразкою того гравця, який не може зробити крок. Відповідно, стан гри можна описати набором з N натуральних чисел, а гра закінчується тоді, коли сума цих чисел стає рівна 0.
Вирішення
Вирішення цієї гри опублікував в 1901 р Чарльз Бутон (Charles L. Bouton), і виглядає воно наступним чином.
Теорема
Поточний гравець має виграшну стратегію тоді і тільки тоді, коли XOR-сума розмірів купок відмінна від нуля. В іншому випадку поточний гравець знаходиться в програшному стані.
Основна суть наведеного нижче доведення полягає в наявності симетричної стратегії для супротивника. Ми покажемо, що, опинившись у стані з нульовою XOR-сумою, гравець не зможе вийти з цього стану - при будь-якому його переході в стан з ненульовою XOR-сумою у противника знайдеться відповідний хід, який повертає XOR-суму назад в нуль.
Доведення
Приступимо тепер до формального доведення (воно буде конструктивним, тобто ми покажемо, як саме виглядає симетрична стратегія супротивника - який саме хід потрібно буде йому здійснювати).
Доводити теорему будемо за допомогою математичної індукції.
Для порожнього "німа" (коли розміри всіх купок дорівнюють нулю) XOR-сума дорівнює нулю, і теорема вірна.
Нехай тепер ми хочемо довести теорему для деякого стану гри, з якого є хоча б один перехід. Користуючись припущенням індукції (і ациклічності гри) ми вважаємо, що теорема доведена для всіх станів, в які ми можемо потрапити з поточного.
Тоді доведення розпадається на дві частини: 1) якщо XOR-сума (s) в поточному стані рівна 0, то треба довести, що поточний стан є програшним, тобто всі переходи з нього ведуть в стану з XOR-сумою t != 0.
2) якщо s != 0, то треба довести, що знайдеться перехід, що приводить нас в стан з t = 0.