Differences From Artifact [b75bd46f8bc82eec]:
- File
lib/doc/nim.txt
- 2014-10-24 12:49:30 - part of checkin [339e20815a] on branch trunk - 637 (user: kinaba) [annotate]
To Artifact [afbe18987eb71e60]:
- File
lib/doc/nim.txt
- 2014-10-24 13:25:36 - part of checkin [0366fb35b4] on branch trunk - nim.txt generalization of more combinators. (user: kinaba) [annotate]
45 45 注意:
46 46 必勝 + 必勝 = 必敗
47 47 は成り立たない! *2 + *1 は 初手で *1 + *1 に行けるのでこれは勝てる
48 48
49 49 補題:G+G は必敗
50 50 - まねっこmoveをされると負けるしかない
51 51
52 +-------------------------------------------------------------------------------------------
52 53 補題:A≡A', B≡B' ならば A+B≡A'+B'
53 54 - A+B+A'+B' = (A+A')+(B+B') = 必敗+必敗 = 必敗
54 55
55 -補題:Ai≡Ai' ならば {A0,A1,A2,...}≡{A0',A1',A2',...}
56 - - {A0,A1,A2,...}+{A0',A1',A2',...} は必敗。なぜならこちらがどう動かしても
57 - A0+A0', A1+A1', A2+A2', ... のいずれかの必敗状態に遷移させられるから。
58 -
59 --------------------------------------------------------------------------------------------
60 56 定理【ゲームの和はxor】
61 57 - *n1 + *n2 = *(n1 xor n2)
62 58 - より一般的に G1≡*n1, G2≡*n2 ならば、G1 + G2 ≡ *(n1 xor n2)
63 59
64 60 証明
65 61 - *n1 + *n2 + *(n1 xor n2) が必敗であることを言えば良い。
66 62 - (n1 xor n2 xor (n1 xor n2)) は 0 である
................................................................................
71 67 >> つまりa,b,cのどれかは^xすると減ることを言えばよい。
72 68 >> a,b,cのうち最上位ビットが立っているものが奇数個ならxも立つのでxorすれば減る
73 69 >> 偶数個(2個)なら、その最上位ビットを無視した残りをa',b',c'とするとこれも
74 70 >> xorがxなので数学的帰納法的にやることにより巧い減らし方が見つかる。
75 71 - よって最終局面"全部 0"になるのは絶対に自分のターン
76 72
77 73 -------------------------------------------------------------------------------------------
74 +補題:Ai≡Ai' ならば {A0,A1,A2,...}≡{A0',A1',A2',...}
75 + - {A0,A1,A2,...}+{A0',A1',A2',...} は必敗。なぜならこちらがどう動かしても
76 + A0+A0', A1+A1', A2+A2', ... のいずれかの必敗状態に遷移させられるから。
77 +
78 78 定理【ゲームの状態遷移はmex】
79 79 - {*n1, ..., *nk} ≡ *mex(n1,...,nk)
80 80 where mex(S) = min(nat \setminus S)
81 81
82 82 - より一般的に G1≡*n1, ..., Gk≡*nk ならば、G={G1, ..., Gk} ≡ *mex(n1,...,nk)
83 83 帰納的に、全てのゲームはなんらかの *n と等価
84 84
................................................................................
91 91 で両側等価を保ててしまう。
92 92
93 93
94 94 -------------------------------------------------------------------------------------------
95 95 まとめ
96 96
97 97 ・一手動かした次の局面が *n1 または *n2 または ... なゲーム
98 - {*n1, ..., *nk} = *mex(n1, ..., nk)
98 + {*n1, ..., *nk} ≡ *mex(n1, ..., nk)
99 +
99 100 ・ゲーム *n1 と *n2 とどちらかを選んで一手進められるゲーム
100 - *n1 + *n2 = *(n1 xor n2)
101 -・ゲーム *n1 と *n2 とどちらか一方または両方一気に進められるゲーム
102 - *n1 <+> *n2 = *(n1 + n2) //単に1個の山なのとかわらない
103 -・両方一手ずつ進めるゲーム?????
104 - *n1 X *n2 = ?
101 + *n1 + *n2 ≡ *(n1 xor n2)
102 +
103 +
104 +-------------------------------------------------------------------------------------------
105 +その他のゲームの組み合わせ(証明があやしい)
106 +
107 +定理: ゲーム *n1 と *n2 とどちらか一方または両方一気に進められるゲーム
108 + *n1 <+> *n2 ≡ *(n1 + n2)
109 +証明: 単に1個の山なのとかわらないので勝敗一致どころか同型
110 +
111 +補題:A≡A' かつ B≡B' ならば (A<+>B)≡(A'<+>B')。
112 + ゆえに一般に G1≡*n1, G2≡*n2 ならば G1<+>G2 ≡ *(n1+n2)
113 +証明:(A<+>B)+(A'<+>B')が必敗であることを言えばよい。
114 + 相手がどう動かしても A<+>B ==> a<+>b
115 + a+a'、b+b'が必敗であるように (a<+>b)+(a'<+>b') と動かせる。
116 + いずれ相手は死ぬ
117 +
118 +
119 +定理: 先手はゲーム *n1、後手はゲーム *n2 を交互に一手ずつ進めるゲーム
120 + *n1 X *n2 ≡ *(n1<=n2 ? 0 : n2+1)
121 + 後手
122 + 0 1 2 3 4
123 + ------+----------
124 + 先手 0|0 0 0 0 0
125 + 1|1 0 0 0 0
126 + 2|1 2 0 0 0
127 + 3|1 2 3 0 0
128 + 4|1 2 3 4 0
129 + 左辺のゲームのmex計算してみるとこうなる。
130 +
131 +補題:A≡A' かつ B≡B' ならば (A X B)≡(A' X B')。
132 + ゆえに一般に G1≡*n1, G2≡*n2 ならば G1 X G2 ≡ *(n1<=n2 ? 0 : n2+1)
133 +証明:AxB + A'xB' を Bxa + A'xB' と動かされたら Bxa + B'xa' に動かせて≡が
134 + 保てるのでいずれ相手は死ぬ