체스 불변량

Source: Hacker News

체스는 겉보기보다 훨씬 까다롭다. 캐슬링, 앙파상, 폰 승격, 핀, 발견 체크, 그리고 스테일메이트라는 교착 상황 등 규칙이 너무 많다.

체스는 동시성 시스템이지만, 매우 특수한 형태의 동시성을 가진다: 교차 실행. 더 구체적으로 말하면 차례를 번갈아 가며 진행한다: 백, 흑, 다시 백.

여기서 우리는 동시성 시스템을 어떻게 다루는지 알겠는가? 우리는 시스템을 모델링하고, 그 불변식을 추출한다.

먼저 몇 가지 설정 정의를 살펴보자.

컴퓨터 과학이나 수학 논문에서 “Section 2: Model and Problem”을 충분히 잘 쓰면, 나머지 논문은 스스로 써진다. 이런 설정을 통해 어떤 동작이 일어날지 어느 정도 예측할 수 있다.

사실, 동작은 잊어버리자. 몇 가지 불변식에 대해 살펴보자.

불변식을 도출할 때 우리는 “항상 참이어야 하는 것은 무엇인가?” 라고 묻는다. 나는 안전 불변식을 두 부류로 나누는 것이 유용하다고 생각한다: 상태 불변식(단일 상태에 대한 술어)과 전이 불변식(한 단계에 대한 술어). 전이 불변식은 상태 불변식만큼 흔히 쓰이진 않지만, 시스템의 전이를 논리할 때 매우 도움이 된다. 체스 같은 시스템에서는 아래에서 보듯 전이 불변식이 특히 유용하다.

상태 불변식

TypeOK는 모든 변수가 올바른 공간에 존재함을 의미한다. 지루하지만, 내가 인정하고 싶지 않을 정도로 많은 버그를 잡아냈다. OneKingPerColor와 BothKingsOnBoard도 마찬가지로 기본적인 sanity check이다.

TurnParity가 첫 번째 흥미로운 불변식이다. 이는 두 상태 변수를 연결한다: 백은 짝수 수의 차례에 움직이고, 흑은 홀수 수의 차례에 움직인다.