Mô hình hóa Cờ vua: Bài học về Bất biến trong Hệ thống Đồng thời

Mô hình hóa Cờ vua: Bài học về Bất biến trong Hệ thống Đồng thời

Cờ vua phức tạp hơn vẻ bề ngoài rất nhiều. Nó chứa đựng hàng loạt quy tắc chi tiết: nhập thành, bắt tốt qua đường, phong cấp, chặn quân, chiếu lộ, và trường hợp cờ hòa (stalemate) khi hết nước đi. Tuy nhiên, dưới góc nhìn của một kỹ sư phần mềm, cờ vua thực chất là một hệ thống đồng thời (concurrent system), nhưng với một kiểu đồng thời rất cụ thể: thực thi xen kẽ (interleaved execution). Nói cách simpler hơn, là luân phiên nhau đi: Trắng, rồi Đen, rồi lại Trắng.

Trong khoa học máy tính, khi đối mặt với các hệ thống đồng thời, chúng ta thường mô hình hóa chúng và chắt lọc ra các "bất biến" (invariants). Đây là chìa khóa để hiểu và chứng minh tính đúng đắn của hệ thống.

Mô hình hóa hệ thống

Bất biến là gì?

Khi suy luận về các bất biến, chúng ta tự đặt câu hỏi: Điều gì luôn luôn đúng? Tôi nhận thấy hữu ích nếu chia các bất biến an toàn (safety invariants) thành hai nhóm chính: bất biến trạng thái (state invariants) và bất biến chuyển đổi (transition invariants).

Bất biến trạng thái là các vị từ (predicates) trên một trạng thái duy nhất, trong khi bất biến chuyển đổi là các vị từ trên một bước chuyển đổi. Mặc dù bất biến chuyển đổi không phổ biến bằng bất biến trạng thái, nhưng chúng cực kỳ hữu ích khi suy luận về các chuyển đổi của hệ thống, đặc biệt là trong trường hợp của cờ vua.

Các bất biến trạng thái

Đầu tiên, chúng ta có TypeOK: quy tắc này đảm bảo mọi biến đều nằm trong không gian đúng. Nó có vẻ nhàm chán nhưng lại bắt được nhiều lỗi hơn mức chúng ta sẵn lòng thừa nhận.

Tiếp theo là OneKingPerColor (Mỗi màu một vua) và BothKingsOnBoard (Cả hai vua đều phải trên bàn cờ) - đây là các kiểm tra tính hợp lý cơ bản.

Bàn cờ và các quy tắc

TurnParity (Tính chẵn lẻ của lượt) là bất biến đầu tiên thú vị hơn. Nó liên kết hai biến trạng thái lại với nhau: TRẮNG đi ở các nước đi chẵn, ĐEN đi ở các nước đi lẻ. Hành động MakeMove (Đi quân) phải thỏa mãn TurnParity này.

PreviousPlayerNotInCheck tái khẳng định quy tắc "bạn phải kết thúc lượt của mình mà không bị chiếu" dưới dạng "nhìn lại: người vừa đi không bị chiếu". Từ đó suy ra NotBothInCheck (Không cả hai vua đều bị chiếu cùng lúc).

Các bất biến chuyển đổi

Đây là các vị từ trên cặp trạng thái, thường được viết dưới dạng ngoặc vuông: [][P]_vars. Chúng diễn tả cách mọi thứ thay đổi dưới các ràng buộc.

Ký pháp rất đơn giản: x là giá trị của biến x ở trạng thái hiện tại, và x' là giá trị ở trạng thái tiếp theo.

MoveCountStrictlyIncreases (Số nước đi tăng nghiêm ngặt) và TurnAlternates (Lượt luân phiên) cho biết mỗi bước sẽ tăng số nước đi và đổi màu lượt đi. Nếu một chuyển đổi nào đó làm sai lệch điều này, chắc chắn đã có lỗi xảy ra.

PieceCountNonIncreasing (Số lượng quân cờ không tăng) loại trừ khả năng quân cờ xuất hiện từ hư không. SingleCapturePerMove (Chỉ bắt một quân mỗi nước đi) thắt chặt điều này: tối đa một quân biến mất mỗi bước. ExactlyTwoSquaresChange (Chính xác hai ô thay đổi) là quy tắc chặt chẽ nhất. Nó nói rằng chính xác hai ô thay đổi mỗi nước đi: ô nguồn (giờ trống) và ô đích (giờ chứa quân vừa di chuyển).

Suy luận logic trong cờ vua

Khi các quy tắc đặc biệt xuất hiện

Đây là mô hình của các quy tắc cờ vua cơ bản. Một bài tập hữu ích ở đây là xem xét xem những bất biến nào sẽ sống sót khi chúng ta thêm vào nhập thành, tốt, và bắt tốt qua đường.

ExactlyTwoSquaresChange bị vi phạm khi thêm nhập thành: bốn ô thay đổi trong một nước đi. Tương tự, bắt tốt qua đường (en passant) bắt một quân không nằm ở ô đích, nên ba ô thay đổi.

Tuy nhiên, PieceCountNonIncreasing vẫn sống sót qua phong cấp (khi một tốt biến thành hậu, số lượng quân không đổi).

Việc liệt kê các quy tắc giúp chúng ta tư duy rõ ràng hơn trước cả khi phân tích. Ví dụ, rõ ràng mãi đến thế kỷ 19, mọi người mới làm rõ rằng bạn không thể phong cấp một tốt thành Vua - một quy tắc đã ngăn chặn bất kỳ ai cố gắng chiếu bí bằng cách trả lời "Vua đã chết, muôn năm Vua!" (Le roi est mort, vive le roi!).