Komakuro

English/日本語

将棋の数学的定義:well-definedness

前回定義した禁止局面・詰み・打ち歩詰めの3つの概念がwell-definedであることを示します。
再帰的定義な定義がwell-definedかどうか気にならないという人は、本記事は読まなくても今後の記事を読むのに差し支えはないと思います。
なお、ここでは狭義の禁止局面の方について証明しますが、広義の方もまったく同様です。

g∈Gameとi∈ℕを任意にとります。
g(i)の手番をtとおきます。
まず、
(step0-2) gのi番目が打ち歩詰めである
ことがwell-definedであるか考えましょう。
打ち歩詰めの定義(1)の(3)のどちらか一方でも成り立たないときは、打ち歩詰めでない(したがってwell-definedである)ので、(1)も(3)もなりたつとします。
あとは
(step0-3) gのi番目が詰みである
ことがwell-definedならokです。
g(i)→<sub>β</sub>sとなる任意のs<sub>1</sub>∈Stateをとります。
このとき
(step1-1) [g(1),g(2),...,g(i),s<sub>1</sub>]のi+1番目がt側の禁止局面である
ことがwell-defineならokです。
禁止局面の定義の(1),(2),(3)のいずれか一つでもなりたつときは、禁止局面である(したがってwell-definedである)ので、これらのいずれもなりたたないとします。
あとは
(step1-2) [g(1),g(2),...,g(i),s<sub>1</sub>]のi+1番目が打ち歩詰めである
ことがwell-defineならokです。
打ち歩詰めの定義(1)の(3)のどちらか一方でも成り立たないときは、打ち歩詰めでない(したがってwell-definedである)ので、(1)も(3)もなりたつとします。
あとは
(step1-3) [g(1),g(2),...,g(i),s<sub>1</sub>]のi+1番目が詰みである
ことがwell-defineならokです。
s<sub>1</sub>→<sub>β</sub>s<sub>2</sub>となる任意のs<sub>2</sub>∈Stateをとります。
このとき
(step2-1) [g(1),g(2),...,g(i),s<sub>1</sub>,s<sub>2</sub>]のi+2番目がt側の禁止局面である
ことがwell-defineならokです。
禁止局面の定義の(1),(2),(3)のいずれか一つでもなりたつときは、禁止局面である(したがってwell-definedである)ので、これらのいずれもなりたたないとします。
あとは
(step2-2) [g(1),g(2),...,g(i),s<sub>1</sub>,s<sub>2</sub>]のi+2番目が打ち歩詰めである
ことがwell-defineならokです。
...
(step18-2) [g(1),g(2),...,g(i),s<sub>1</sub>,s<sub>2</sub>,...,s<sub>18</sub>]のi+18番目が打ち歩詰めである
ことがwell-definedならokです。
実際(step18-2)は成立しないのでwell-definedです。
(step18-2)が成立しない理由は以下のとおりです。
(step18-2)が成立するとします。
g(i-1)=(post,t), g(i)=(post',-t), s<sub>1</sub>=(post<sub>1</sub>, t), ... , s<sub>18</sub>=(post<sub>18</sub>,-t)とおけます。
まず、(step0-2)において(3)がなりたつことから、あるp∈Pieceがあって「kind(p)=歩かつpost(p)=(stand,t)かつpost'(p)≠(stand,t)」となります。
g(i-1)→<sub>β1</sub>g(i)ですから、<a href="?shogi-beta1">β1遷移の定義</a>をみると、post(p)=(stand,t)なので、<a href="?shogi-control">駒の利きの定義</a>より、β1遷移の定義の(2-1)は不成立です。
つまりpはβ1遷移の定義の(2)の意味でのpではありません。
post(p)=(stand,t)であることから(=((c',r',s'),o')とならないので)(2-3)にあてはまるはずですが、post(p)=(stand,t)≠post'(p)で不成立です。
よって(2)は成立せず、したがって(3)が成立します。
(3-3)よりあるc∈Column,r∈Rowがあってpost'(p)=((c,r,不成),t)です。
次に、(step1-2)において(3)がなりたつことから、あるp<sub>1</sub>∈Pieceがあって「kind(p<sub>1</sub>)=歩かつpost'(p<sub>1</sub>)=(stand,-t)かつpost<sub>1</sub>(p<sub>1</sub>)≠(stand,-t)」となります。
したがってp≠p<sub>1</sub>がわかります。
また、先程と同様にして、β1遷移の定義の(3)がなりたちます。
(3-3)よりあるc<sub>1</sub>∈Column,r<sub>1</sub>∈Rowがあってpost<sub>1</sub>(p<sub>1</sub>)=((c<sub>1</sub>,r<sub>1</sub>,不成),-t)です。
(3-4)よりpost<sub>1</sub>(p)=post'(p)=((c,r,不成),t)です。
次に、(step2-2)において(3)がなりたつことから、あるp<sub>2</sub>∈Pieceがあって「kind(p<sub>2</sub>)=歩かつpost<sub>1</sub>(p<sub>2</sub>)=(stand,t)かつpost<sub>2</sub>(p<sub>2</sub>)≠(stand,t)」となります。
したがってp<sub>2</sub>≠p<sub>1</sub>とp<sub>2</sub>≠pがわかります。
また、先程と同様にして、β1遷移の定義の(3)がなりたちます。
(3-3)よりあるc<sub>2</sub>∈Column,r<sub>2</sub>∈Rowがあってpost<sub>2</sub>(p<sub>2</sub>)=((c<sub>2</sub>,r<sub>2</sub>,不成),t)です。
(3-4)よりpost<sub>2</sub>(p)=post<sub>1</sub>(p)=((c,r,不成),t)、post<sub>2</sub>(p<sub>1</sub>)=post<sub>1</sub>(p<sub>1</sub>)=((c<sub>1</sub>,r<sub>1</sub>,不成),-t)です。
以下同様にしてp,p<sub>1</sub>,...,p<sub>18</sub>は相異なる駒であって、kind(p)=kind(p<sub>1</sub>)=...=kind(p<sub>18</sub>)=歩となり、<a href="?shogi-kind-map">駒種写像の定義</a>に反します。

長いですが、言っていることは簡単で、要は歩を打つ手を19回以上続けることは不可能だということです(歩は19個もない)。
ちなみに、同様にして次のことがいえます。
定理「連続した打ち歩詰め」s1,s2,...,sn,t<sub>1</sub>,t<sub>2</sub>,...,t<sub>19</sub>∈Stateに対し、
[s<sub>1</sub>,s<sub>2</sub>,...,s<sub>n</sub>,t<sub>1</sub>]のn+1番目、[s<sub>1</sub>,s<sub>2</sub>,...,s<sub>n</sub>,t<sub>1</sub>,t<sub>2</sub>]のn+2番目、... 、[s<sub>1</sub>,s<sub>2</sub>,...,s<sub>n</sub>,t<sub>1</sub>,t<sub>2</sub>,...,t<sub>19</sub>]のn+19番目、がすべて打ち歩詰めであることはありません。
NIL以上から打ち歩詰めはwell-definedなので、禁止局面もwell-definedであり、したがって詰みもwell-definedです。