체스 모델링: 불변량과 상태 전이의 복잡성
체스는 종종 단순한 전략 게임으로 인식되지만, 소프트웨어 공학 및 형식 검증(formal verification) 관점에서는 엣지 케이스(edge cases)의 악몽과도 같습니다. 게임의 규칙을 형식적으로 모델링하려고 시도할 때—특히 TLA+와 같은 도구를 사용할 때—복잡성은 보드의 기하학적 구조가 아니라, 모든 수(move)에 걸쳐 유지되어야 하는 복잡한 불변량(invariants) 세트에서 발생합니다.
형식적 모델링은 무엇이 "법적" 상태를 구성하는지에 대한 엄격한 정의를 요구합니다. 체스에서 이는 단순히 기물이 올바른 위치에 있는지 확인하는 것 이상의 것을 의미합니다. 특정 동작을 검증하기 위해 수의 이력을 추적하고, 어떤 수도 왕(king)을 불법적인 상태로 만들지 않도록 보장해야 합니다.
상태 불변량 vs. 전이 불변량
형식적 모델링의 핵심은 상태 불변량(state invariants)과 전이 불변량(transition invariants)의 구분입니다. 상태 불변량은 게임의 모든 유효한 상태에 대해 참이어야 하는 술어(predicate)입니다. 예를 들어, 체스의 근본적인 상태 불변량은 보드 위에 항상 각 색깔의 왕이 정확히 하나씩 있어야 한다는 것입니다.
하지만 전이 불변량은 더 복잡합니다. 이는 현재 상태와 다음 상태라는 상태 쌍에 대한 술어입니다. 이들은 이동과 잡기(capture)의 규칙을 정의합니다. "이 보드 구성이 합법적인가?"라고 묻는 대신, 전이 불변량은 "상태 A에서 상태 B로의 이동이 게임 규칙에 따라 합법적인가?"라고 묻습니다.
이 구분은 매우 중요합니다. 왜냐하면 일부 규칙은 단순한 상태 속성으로 표현될 수 없기 때문입니다. 예를 들어, en passant(앙파상) 규칙은 전적으로 상대방이 둔 이전 수에 달려 있습니다. 전이를 추적하지 않으면, 보드 상태만으로는 en passant 잡기가 합법적인지 판단하기에 불충분합니다.
체스 규칙의 "숨겨진" 복잡성
많은 개발자는 체스를 일련의 단순한 수로 보기 때문에 구현의 어려움을 과소평가합니다. 그러나 게임은 상태 머신(state machine)을 복잡하게 만드는 규칙들로 가득 차 있습니다.
- Castling (캐슬링): 왕이나 룩(rook)이 움직인 적이 있는지에 대한 지식이 필요하며, 이는 게임에 "숨겨진" 상태를 추가합니다.
- En Passant (앙파상): 단 한 차례의 턴 동안만 존재하는 일시적인 기회이며, 특정 전이 이력을 요구합니다.
- Pawn Promotion (폰 프로모션): 특정 좌표에 도달했을 때 하나의 기물 유형을 다른 유형으로 변환하는 상태 변화입니다.
- Stalemate (스테일메이트): 자신의 차례인 플레이어가 합법적인 수를 둘 수 없지만 체크(check) 상태는 아닌 교착 상태입니다.
한 댓글 작성자가 언급했듯이, 복잡성은 매우 커서 숙련된 개발자조차 이러한 도전 과제와 실제 시스템 통합 사이의 유사점을 발견할 수 있습니다. "프랑스 폰 잡기 규칙 때문에 울지" 않고 1,500년 된 게임을 모델링하려는 노력은, 상태 불변량 위반이 현대적인 CRUD 애플리케이션이나 결제 통합에서도 흔히 발생한다는 점을 상기시켜 줍니다.
행동 모델링 vs. 데이터 모델링
이러한 문제에 접근하는 방식에는 상당한 철학적 차이가 있습니다. 어떤 이들은 행동을 표현하는 것이 목표일 때 데이터(상태)에 집중하는 것은 잘못된 접근 방식이라고 주장합니다.
행동에 집중하는 것이 훨씬 더 유용하다고 생각합니다. 따라서 상태 전이에 대해 생각하는 대신, 근본적인 데이터 구조와 상관없이 프로그램이 무엇을 수행할 수 있도록 허용되는지에 집중하십시오.
이러한 관점에서는 코드가 단순히 상태 전이가 수학적으로 가능한지 계산하는 대신, 기물이 왜 움직일 수 없는지를 명시적으로 기술해야 합니다. "데이터 중심"에서 "행동 중심" 모델링으로의 이러한 전환은, TLA+와 같은 형식 검증 도구에는 덜 적합할 수 있지만, 인간이 읽고 유지보수하기에 더 직관적일 수 있습니다.
구현 관점
이러한 규칙을 코드로 구현하려는 사람들에게는 함수형 프로그래밍이 매 compelling한 경로를 제공합니다. 가능한 수를 확장하고, 불법적인 수를 버리고, 잡기를 완료하는 일련의 변환(transformations)으로 규칙을 모델링함으로써, 시스템은 매우 확장 가능해집니다. 이 방식은 핵심 엔진을 다시 작성하지 않고도 새로운 기물 유형이나 사용자 정의 규칙을을 쉽게 추가할 수 있게 하며, 게임을 하드코딩된 if-else 문 세트가 아닌 가능한 수의 필터링된 세트(filtered sets of possible moves)로 취급합니다.