Alloyで少しだけ遊ぶ

Alloyでゲームについて調べようの回！！

お題は、3x3の9マスでの○×ゲーム(三目並べ)は、先手必勝となるかどうか、です。

簡単なゲームから考える

まず次のような非常に簡単なゲームを考えます。

場にA , B , Cという3つの石がある。3種類じゃなくて、本当に3つしか石はない！
2人のプレーヤーで交互に場から石を取って自分のものにする。ただしパスはダメ。

先に"AとC"の両方を手に入れたものが勝利。

このゲーム、先手が有利なのは明らかです。取りあえず2つは石を取らないと勝ち目がないわけで、後手だと1つしか取れないわけです。

では先手がどれぐらい有利なのか。１つの指標として、「先手必勝」かどうかを考えます。

普通に考えれば、先手はAかCを取って、次に残りを取ろうとします。後手は、先手が次に取ろうとしているものを取れば、引き分けに成る筈です。
だから先手必勝ではない…。

ということで、本当に先手必勝でないかどうかをAlloyを使って調べてみましょう。
方針としては、先手必勝になるという命題を記述してそれが絶対に正しいかどうかをassertionで調べるというものです。ダメなら反例が出る筈です。

ここで重要なのは、どう書けばAlloyで楽に書けるか。皆さんも少し考えてみてください。

私は次のように書きました。

abstract sig Ishi { } // 石という集合を定義
one sig A , B , C extends Ishi {}  // ゲームで使う石はA , B , Cという3つに限る

assert sente_always_win {
	some X : Ishi | all Y : Ishi - X | some Z : Ishi - X - Y | X + Z in A + C
}

check sente_always_win

アサーション「先手必勝」は、先手は以下の制約を満たすXを取る事が出来る事を言っています。
制約 : 後手がXを除いたどんなYを取った場合でも、更に先手が残るたった１つのZについて、XとZは実はAとCの組になっている。

これが満たせるなら、先手必勝となる先手の石の取り方が確かに存在するという事になります。

ところが実際は、Xとしてどんなに上手くとっても、後手のYによって「邪魔」されてしまうのは前に述べた通りです。なので、この例だと反例が発生するはずです。実際に調べてみると…。

skolem $sente_always_win_Y={A$0->C$0, B$0->C$0, C$0->A$0}

という結果を得ます。それとなく見ると、何かに気付けると思います。

そう、これは実は、後手が先手の勝利を防ぐパターンになっているのです！！！

先手がAを取ったら、俺はCを取る！
先手がBを取ったら、俺はCを取る！
先手がCを取ったら、俺はAを取る！

戦略はもう1種類あります。

skolem $sente_always_win_Y={A$0->C$0, B$0->A$0, C$0->A$0}

これもAlloyが教えてくれます。

○×ゲームに戻る

では、○×ゲームはどうAlloyで記述すれば楽に書けるのでしょうか。まぁぼくは良く分からないので、先の考えを本当にそのまんま使って、次のように書きました。

abstract sig Board {
	right : lone Board ,
	up    : lone Board ,
	down : lone Board
}

one sig
A , B , C ,
D , E , F ,
G , H , I extends Board {}

fact {
	A.right = B B.right = C C.right = none
	D.right = E E.right = F F.right = none
	G.right = H H.right = I I.right = none

	A.down = D B.down = E C.down = F
	D.down = G E.down = H F.down = I
	G.down = none H.down = none I.down = none

	all X : Board | all Y : Board | X.down = Y <=> Y.up = X
}

pred win(have : set Board) {
	some p : have | 
	(
		(#p.^right = 2 && p.^right in have) ||
		(#p.^down = 2 && p.^down in have) ||
		(#p.^(right.down) = 2 && p.^(right.down) in have) ||
		(#p.^(right.up) = 2 && p.^(right.up) in have)
	)
}

assert always_win {
	some X_1 : Board                | let Xs = X_1 |
	all      Y_1 : Board - Xs        | let Ys = Y_1 |
	some X_2 : Board - Xs - Ys | let Xs = Xs + X_2 |
	all      Y_2 : Board - Xs - Ys | let Ys = Ys + Y_2 |
	some X_3 : Board - Xs - Ys | let Xs = Xs + X_3 | win[Xs] or (
	all      Y_3 : Board - Xs - Ys | let Ys = Ys + Y_3 | (not win[Ys]) && (
	some X_4 : Board - Xs - Ys | let Xs = Xs + X_4 | win[Xs] or (
	all      Y_4 : Board - Xs - Ys | let Ys = Ys + Y_4 | (not win[Ys]) && (
	some X_5 : Board - Xs - Ys | let Xs = Xs + X_5 | win[Xs] ) ) ) )
}

check always_win

かなり強引ですが、まぁ単純ではあります。ではこれを動かしてみましょう！！！先手必勝と言えるのか！！！

結果は

ダメ！！！ 反例が見つかりました。どんな感じかというと…

skolem $always_win_Y_1={A$0->E$0, B$0->H$0, C$0->E$0, D$0->F$0, E$0->I$0, F$0->E$0, G$0->E$0, H$0->E$0, I$0->E$0}

skolem $always_win_Y_2={A$0->B$0->C$0, A$0->C$0->B$0, A$0->D$0->G$0, A$0->F$0->C$0, A$0->G$0->D$0, A$0->H$0->D$0, A$0->I$0->B$0, B$0->A$0->C$0, B$0->C$0->A$0, B$0->D$0->A$0, B$0->E$0->A$0, B$0->F$0->A$0, B$0->G$0->A$0, B$0->I$0->A$0, C$0->A$0->B$0, C$0->B$0->A$0, C$0->D$0->G$0, C$0->F$0->I$0, C$0->G$0->B$0, C$0->H$0->I$0, C$0->I$0->F$0, D$0->A$0->G$0, D$0->B$0->A$0, D$0->C$0->G$0, D$0->E$0->G$0, D$0->G$0->A$0, D$0->H$0->G$0, D$0->I$0->G$0, E$0->A$0->C$0, E$0->B$0->H$0, E$0->C$0->G$0, E$0->D$0->F$0, E$0->F$0->D$0, E$0->G$0->C$0, E$0->H$0->B$0, F$0->A$0->C$0, F$0->B$0->A$0, F$0->C$0->I$0, F$0->D$0->B$0, F$0->G$0->I$0, F$0->H$0->I$0, F$0->I$0->C$0, G$0->A$0->D$0, G$0->B$0->D$0, G$0->C$0->B$0, G$0->D$0->A$0, G$0->F$0->C$0, G$0->H$0->I$0, G$0->I$0->H$0, H$0->A$0->F$0, H$0->B$0->G$0, H$0->C$0->I$0, H$0->D$0->I$0, H$0->F$0->I$0, H$0->G$0->I$0, H$0->I$0->G$0, I$0->A$0->H$0, I$0->B$0->C$0, I$0->C$0->F$0, I$0->D$0->B$0, I$0->F$0->C$0, I$0->G$0->H$0, I$0->H$0->G$0}

skolem $always_win_Y_3={A$0->B$0->D$0->G$0, A$0->B$0->F$0->G$0, A$0->B$0->G$0->D$0, A$0->B$0->H$0->I$0, A$0->B$0->I$0->H$0, A$0->C$0->D$0->H$0, A$0->C$0->F$0->I$0, A$0->C$0->G$0->H$0, A$0->C$0->H$0->G$0, A$0->C$0->I$0->H$0, A$0->D$0->B$0->C$0, A$0->D$0->C$0->B$0, A$0->D$0->F$0->C$0, A$0->D$0->H$0->I$0, A$0->D$0->I$0->H$0, A$0->F$0->B$0->I$0, A$0->F$0->D$0->G$0, A$0->F$0->G$0->D$0, A$0->F$0->H$0->I$0, A$0->F$0->I$0->G$0, A$0->G$0->B$0->F$0, A$0->G$0->C$0->B$0, A$0->G$0->F$0->I$0, A$0->G$0->H$0->I$0, A$0->G$0->I$0->H$0, A$0->H$0->B$0->F$0, A$0->H$0->C$0->F$0, A$0->H$0->F$0->I$0, A$0->H$0->G$0->I$0, A$0->H$0->I$0->G$0, A$0->I$0->C$0->H$0, A$0->I$0->D$0->G$0, A$0->I$0->F$0->H$0, A$0->I$0->G$0->H$0, A$0->I$0->H$0->G$0, B$0->A$0->D$0->G$0, B$0->A$0->E$0->I$0, B$0->A$0->F$0->I$0, B$0->A$0->G$0->D$0, B$0->A$0->I$0->E$0, B$0->C$0->D$0->F$0, B$0->C$0->E$0->G$0, B$0->C$0->F$0->I$0, B$0->C$0->G$0->E$0, B$0->C$0->I$0->F$0, B$0->D$0->C$0->I$0, B$0->D$0->E$0->F$0, B$0->D$0->F$0->E$0, B$0->D$0->G$0->F$0, B$0->D$0->I$0->F$0, B$0->E$0->C$0->G$0, B$0->E$0->D$0->F$0, B$0->E$0->F$0->D$0, B$0->E$0->G$0->C$0, B$0->E$0->I$0->F$0, B$0->F$0->C$0->I$0, B$0->F$0->D$0->E$0, B$0->F$0->E$0->D$0, B$0->F$0->G$0->E$0, B$0->F$0->I$0->C$0, B$0->G$0->C$0->E$0, B$0->G$0->D$0->E$0, B$0->G$0->E$0->C$0, B$0->G$0->F$0->E$0, B$0->G$0->I$0->E$0, B$0->I$0->C$0->F$0, B$0->I$0->D$0->E$0, B$0->I$0->E$0->F$0, B$0->I$0->F$0->C$0, B$0->I$0->G$0->F$0, C$0->A$0->D$0->H$0, C$0->A$0->F$0->I$0, C$0->A$0->G$0->D$0, C$0->A$0->H$0->I$0, C$0->A$0->I$0->H$0, C$0->B$0->D$0->I$0, C$0->B$0->F$0->I$0, C$0->B$0->G$0->I$0, C$0->B$0->H$0->I$0, C$0->B$0->I$0->F$0, C$0->D$0->A$0->B$0, C$0->D$0->B$0->A$0, C$0->D$0->F$0->I$0, C$0->D$0->H$0->I$0, C$0->D$0->I$0->F$0, C$0->F$0->A$0->B$0, C$0->F$0->B$0->A$0, C$0->F$0->D$0->H$0, C$0->F$0->G$0->H$0, C$0->F$0->H$0->G$0, C$0->G$0->A$0->H$0, C$0->G$0->D$0->H$0, C$0->G$0->F$0->I$0, C$0->G$0->H$0->I$0, C$0->G$0->I$0->H$0, C$0->H$0->A$0->B$0, C$0->H$0->B$0->A$0, C$0->H$0->D$0->G$0, C$0->H$0->F$0->G$0, C$0->H$0->G$0->B$0, C$0->I$0->A$0->D$0, C$0->I$0->B$0->D$0, C$0->I$0->D$0->G$0, C$0->I$0->G$0->H$0, C$0->I$0->H$0->G$0, D$0->A$0->B$0->C$0, D$0->A$0->C$0->B$0, D$0->A$0->E$0->I$0, D$0->A$0->H$0->I$0, D$0->A$0->I$0->E$0, D$0->B$0->C$0->E$0, D$0->B$0->E$0->H$0, D$0->B$0->G$0->H$0, D$0->B$0->H$0->E$0, D$0->B$0->I$0->H$0, D$0->C$0->A$0->B$0, D$0->C$0->B$0->A$0, D$0->C$0->E$0->I$0, D$0->C$0->H$0->B$0, D$0->C$0->I$0->A$0, D$0->E$0->A$0->I$0, D$0->E$0->B$0->H$0, D$0->E$0->C$0->A$0, D$0->E$0->H$0->B$0, D$0->E$0->I$0->A$0, D$0->G$0->B$0->I$0, D$0->G$0->C$0->E$0, D$0->G$0->E$0->C$0, D$0->G$0->H$0->I$0, D$0->G$0->I$0->H$0, D$0->H$0->A$0->I$0, D$0->H$0->B$0->E$0, D$0->H$0->C$0->B$0, D$0->H$0->E$0->B$0, D$0->H$0->I$0->E$0, D$0->I$0->A$0->E$0, D$0->I$0->B$0->E$0, D$0->I$0->C$0->E$0, D$0->I$0->E$0->A$0, D$0->I$0->H$0->A$0, E$0->A$0->B$0->H$0, E$0->A$0->D$0->F$0, E$0->A$0->F$0->D$0, E$0->A$0->G$0->D$0, E$0->A$0->H$0->F$0, E$0->B$0->A$0->G$0, E$0->B$0->C$0->G$0, E$0->B$0->D$0->G$0, E$0->B$0->F$0->D$0, E$0->B$0->G$0->C$0, E$0->C$0->A$0->B$0, E$0->C$0->B$0->H$0, E$0->C$0->D$0->H$0, E$0->C$0->F$0->H$0, E$0->C$0->H$0->B$0, E$0->D$0->A$0->C$0, E$0->D$0->B$0->C$0, E$0->D$0->C$0->G$0, E$0->D$0->G$0->C$0, E$0->D$0->H$0->B$0, E$0->F$0->A$0->G$0, E$0->F$0->B$0->H$0, E$0->F$0->C$0->G$0, E$0->F$0->G$0->C$0, E$0->F$0->H$0->B$0, E$0->G$0->A$0->D$0, E$0->G$0->B$0->H$0, E$0->G$0->D$0->F$0, E$0->G$0->F$0->D$0, E$0->G$0->H$0->B$0, E$0->H$0->A$0->G$0, E$0->H$0->C$0->G$0, E$0->H$0->D$0->F$0, E$0->H$0->F$0->D$0, E$0->H$0->G$0->C$0, F$0->A$0->B$0->I$0, F$0->A$0->D$0->G$0, F$0->A$0->G$0->D$0, F$0->A$0->H$0->I$0, F$0->A$0->I$0->G$0, F$0->B$0->C$0->I$0, F$0->B$0->D$0->H$0, F$0->B$0->G$0->H$0, F$0->B$0->H$0->I$0, F$0->B$0->I$0->C$0, F$0->C$0->A$0->B$0, F$0->C$0->B$0->A$0, F$0->C$0->D$0->H$0, F$0->C$0->G$0->H$0, F$0->C$0->H$0->D$0, F$0->D$0->A$0->G$0, F$0->D$0->C$0->I$0, F$0->D$0->G$0->A$0, F$0->D$0->H$0->I$0, F$0->D$0->I$0->C$0, F$0->G$0->A$0->D$0, F$0->G$0->B$0->D$0, F$0->G$0->C$0->D$0, F$0->G$0->D$0->A$0, F$0->G$0->H$0->D$0, F$0->H$0->A$0->G$0, F$0->H$0->B$0->G$0, F$0->H$0->C$0->G$0, F$0->H$0->D$0->G$0, F$0->H$0->G$0->D$0, F$0->I$0->A$0->H$0, F$0->I$0->B$0->H$0, F$0->I$0->D$0->G$0, F$0->I$0->G$0->H$0, F$0->I$0->H$0->G$0, G$0->A$0->B$0->F$0, G$0->A$0->C$0->F$0, G$0->A$0->F$0->I$0, G$0->A$0->H$0->I$0, G$0->A$0->I$0->F$0, G$0->B$0->A$0->C$0, G$0->B$0->C$0->A$0, G$0->B$0->F$0->I$0, G$0->B$0->H$0->I$0, G$0->B$0->I$0->H$0, G$0->C$0->A$0->D$0, G$0->C$0->D$0->A$0, G$0->C$0->F$0->I$0, G$0->C$0->H$0->I$0, G$0->C$0->I$0->H$0, G$0->D$0->B$0->I$0, G$0->D$0->C$0->I$0, G$0->D$0->F$0->I$0, G$0->D$0->H$0->I$0, G$0->D$0->I$0->H$0, G$0->F$0->A$0->D$0, G$0->F$0->B$0->I$0, G$0->F$0->D$0->A$0, G$0->F$0->H$0->I$0, G$0->F$0->I$0->H$0, G$0->H$0->A$0->D$0, G$0->H$0->B$0->C$0, G$0->H$0->C$0->D$0, G$0->H$0->D$0->A$0, G$0->H$0->F$0->C$0, G$0->I$0->A$0->D$0, G$0->I$0->B$0->F$0, G$0->I$0->C$0->F$0, G$0->I$0->D$0->B$0, G$0->I$0->F$0->C$0, H$0->A$0->B$0->D$0, H$0->A$0->C$0->D$0, H$0->A$0->D$0->G$0, H$0->A$0->G$0->D$0, H$0->A$0->I$0->G$0, H$0->B$0->A$0->C$0, H$0->B$0->C$0->A$0, H$0->B$0->D$0->I$0, H$0->B$0->F$0->I$0, H$0->B$0->I$0->D$0, H$0->C$0->A$0->B$0, H$0->C$0->B$0->A$0, H$0->C$0->D$0->G$0, H$0->C$0->F$0->B$0, H$0->C$0->G$0->F$0, H$0->D$0->A$0->G$0, H$0->D$0->B$0->G$0, H$0->D$0->C$0->G$0, H$0->D$0->F$0->G$0, H$0->D$0->G$0->A$0, H$0->F$0->A$0->D$0, H$0->F$0->B$0->G$0, H$0->F$0->C$0->G$0, H$0->F$0->D$0->G$0, H$0->F$0->G$0->B$0, H$0->G$0->A$0->D$0, H$0->G$0->B$0->F$0, H$0->G$0->C$0->F$0, H$0->G$0->D$0->A$0, H$0->G$0->F$0->D$0, H$0->I$0->A$0->D$0, H$0->I$0->B$0->F$0, H$0->I$0->C$0->F$0, H$0->I$0->D$0->F$0, H$0->I$0->F$0->C$0, I$0->A$0->B$0->C$0, I$0->A$0->C$0->B$0, I$0->A$0->D$0->G$0, I$0->A$0->F$0->C$0, I$0->A$0->G$0->D$0, I$0->B$0->A$0->H$0, I$0->B$0->D$0->H$0, I$0->B$0->F$0->H$0, I$0->B$0->G$0->H$0, I$0->B$0->H$0->G$0, I$0->C$0->A$0->B$0, I$0->C$0->B$0->D$0, I$0->C$0->D$0->H$0, I$0->C$0->G$0->D$0, I$0->C$0->H$0->G$0, I$0->D$0->A$0->H$0, I$0->D$0->C$0->F$0, I$0->D$0->F$0->H$0, I$0->D$0->G$0->H$0, I$0->D$0->H$0->G$0, I$0->F$0->A$0->G$0, I$0->F$0->B$0->H$0, I$0->F$0->D$0->G$0, I$0->F$0->G$0->H$0, I$0->F$0->H$0->G$0, I$0->G$0->A$0->D$0, I$0->G$0->B$0->F$0, I$0->G$0->C$0->B$0, I$0->G$0->D$0->B$0, I$0->G$0->F$0->C$0, I$0->H$0->A$0->F$0, I$0->H$0->B$0->F$0, I$0->H$0->C$0->F$0, I$0->H$0->D$0->F$0, I$0->H$0->F$0->C$0}

これを使えば、3x3の○×ゲームでは負けることは無いですね！！

このお話で何が言いたかったか

実はこの3x3の○×ゲームで先手必勝がない事を言うのに3,4時間はかけました…。

というのは、どうやればAlloyで簡単に書けるか考えたり(面倒臭い書き方は嫌ですし)、sequenceという列を作ってあれこれするモジュールがあるので、それ使って石の選び方の列のようなものを作って…などなど考えたり、実際に書いたり、色々嵌って困るという事を一通りしました。

で、上のsomeとallが交互に出現するパターンはどこから出したかというと、ゲームの手番のやりとりをどう実装するかということではなくて、そもそもの「何が言えれば先手必勝が言えるか」を考え直してみたという所です。

そうするとあとに残るのは、縦横ナナメに揃っているかどうかを調べる述語を追加してあげれば良いだけです。これについても、Alloyに組込まれている「関係の推移閉包を求める」機能を使いました。まぁ細かい事は、「抽象によるソフトウェア設計を参考にしてください！」という事で。

また、Alloyはどのようにしてこの反例を見付けたのかという事についての興味が出た方もいると思います。
重要なのは、出力結果の中にも出て来ているのですがskolem化というものです。
スコーレム化そのものは、述語論理のエルブランの定理などの文脈などで自然(…?)に出てくるのですがまぁ詳しくは適当なLogicの本も参考にしてください。

それで結局なんなのかというと、ぼくは出来るだけAlloyっぽく手抜きして気楽に書こうという事だけをひたすら考えて上のものを作ったのですが、他の人が挑戦するとどんな感じに短くなるのかなーという所に興味があるので、
皆さんも簡単な練習問題としてやってみてくださいよーということでした。

いやーでも慣れて無いというのは勿論あるのですが、ただでさえこう動き辛い感じなので少しでも余計な事しようとするとすぐにこれは無理だやめようみたいな感じになるのは果たしてどう効いてくるのかっていうのが。

まぁでも上から被せて機械に頑張らせるっていうのは21世紀は人間の時代なので間違って無いと信じています。