【追記あり】 MTGの「無限ループ」を形式的に決定することは可能か

2022年9月14日 追記

　コメント欄の指摘により、この記事には結論部分に影響する誤りが含まれていることが分かりました。
　誤りの概要ですが、この記事では「無限ループの形式的定義が可能であるかどうか」に関する主張が書かれていますが、定義可能かどうかと決定可能であるかどうかを混同して議論が進んでいます。
　後ほど記事を修正する予定ですが、今のバージョンを読まれる方は「定義可能」の部分を「決定可能」に読み替えてお読みください。
　コメント欄にてご指摘くださったハイチュウリツさんに感謝致します。
　この記事の元のタイトルは『MTGの「無限ループ」を形式的に定義することは可能か』でした。

究極の平和主義

　まずはこちらの動画をご覧ください。

　この状況、お互いに《白金の天使/Platinum Angel》をコントロールしていて、敗北が禁止されている状況です。さらに、お互いの手札とライブラリは全て失われ、墓地に置いてあるカードを唱えることも不可能、お互いの《白金の天使》は両方とも《平和な心/Pacifism》がエンチャントされているため、攻撃もブロックすることも不可能です。この状況では、投了以外にどちらかの勝利を確定させる手段が存在しません。

この状況はルールで無限ループと定義されているか

　筆者は上記の動画を観たときに、そういえばこの状況は現在のマジック総合ルールでは明確に引き分けだと定義されていなかったような気がするなと思いました。実際のトーナメントではジャッジに強い裁量が与えられているため、その権限によってゲームの結果を引き分けにすることでこういった状況に対処していますが、アリーナではジャッジの判断による柔軟な対応ではなく、機械的な判定が行われます。アリーナやMOにおいてこういった状況に状況に対する対応をどうするのか、少なくともマジック総合ルールでは定義されていなかったはずです。自分のMTG仲間が集うDiscordチャンネルにこの疑問を投げかけてみたところ、いつも統合ルールについていろいろ助言を与えてくれるVienosNotes氏からこのような返事が返ってきました。

この状態を CR722.3 の断片化したループだと見なせば、CR722.4 によって引き分けになりそうな気はする

　CR722.3とCR722.4は以下のようになります。

722.3. 断片化したループというものがしばしば存在する。つまり、ループに関連している各プレイヤーがそれぞれに行動を取った結果、元と同じ局面が発生したという状況がありうる。その場合、アクティブ・プレイヤー(アクティブ・プレイヤーがループに関連していない場合、ループに関連している中でターン順で最初のプレイヤー)は違う選択をして、ループが続かないようにしなければならない。
722.4. ループが選択的でない処理のみからなる場合、ゲームは引き分けになる。

　なるほど、上記の動画で起こった状況に関して言えば、引き分けであると言えそうな気がします。もちろん、断片化したループと言えるかどうかの判定が結局アリーナやMOにおける機械判定可能かどうかに関しては開発スタッフの頑張りにかかっていますが、少なくともマジック総合ルール側はこの問題に対して一つの答えを出しています。

MTGにおける無限ループを形式的に定義することは可能か

　VienosNotes氏とこの件に関して話をしていると、彼からこのような疑問が出てきました。

マジックにおけるループって形式的に定義できないんですか

　なるほど、いい質問ですね！ 幸いなことに、私はこの疑問に答える知識を持ち合わせていたので、それをこの場で皆様にご紹介しましょう。
　この疑問に答えるために前提となる三つの知識をまずはご紹介します。
一つ目は「形式的」という言葉の意味です。わかりやすさのために、誤解を恐れずにかみ砕いて説明致しますと、「形式的に定義する」とは、論理的に取り扱うことができる様に定義されたものだと思ってください。言い方を変えると、形式的に定義されたものは、コンピュータで取り扱いできる様に曖昧さを完全に排除したものと思っていただいても構いません。詳しく知りたい方は検索エンジンなどで「形式手法」などのキーワードを調べてみてください。
　次に二つ目は停止性問題です。この問題は簡単に言うと、「どんなプログラムを与えても、『そのプログラムが停止するか無限ループに陥るかを判定すること』が可能なプログラムを作ることは可能かどうか」というものです。結論から言うと、これは不可能です。可能だと仮定した場合、与えられたプログラムが停止可能なときに無限ループに陥り、そうでないときに停止するプログラムを書けますが、そのプログラムにそのプログラム自身を与えると矛盾するため、仮定は誤りであることが示せます。ややこしいですが、結論である「「どんなプログラムを与えても、『そのプログラムが停止するか無限ループに陥るかを判定すること』が可能なプログラムは作れない（存在しない）」ということだけ覚えてください。
　最後の三つ目はMTGがチューリング完全であるという事実です。「MTGがチューリング完全である」とどういうことかを誤解を恐れずにざっくりと説明すると、皆さんが今この記事を見ているPCやスマホなどで計算できることならば何でも理論上はMTGを用いて計算することが可能だということです。これを事実3と呼びます。
　以上の三つの事実から、以下のような推論が可能です。

MTGにおける無限ループを形式的に定義できると仮定すれば、MTGで存在しうるいかなる状況においても、それが無限ループであるかどうかをMTG自身に判定させることが可能である。しかし、MTG上に構成された任意のプログラム停止性を判定できるプログラムはMTG上に構成できない。以上より矛盾するので、仮定は誤り。

　従って、MTGにおける無限ループを形式的に定義することは不可能という結論になります。
　ちなみに、いかなる状況においても有効な厳密な無限ループの定義をすることは不可能ですが、これはよく起こりうる無限ループの状況を例示することを妨げるものではありません。つまりどういうことかというと、冒頭の動画の状況ぐらいにはアリーナも対応してほしいものです。（これが言いたかった）

参考文献

Alex Churchill「Magic: the Gathering is Turing Complete」
https://www.toothycat.net/~hologram/Turing/index.html （2020年5月24日）
Wizards of the Coast LLC 「マジック総合ルール(和訳 20200417.1 版)」
https://mtg-jp.com/gameplay/rules/docs/0006836/ （2020年5月24日）

謝辞

この記事を執筆するためのインスピレーションを与えたくれたデッキの考案者であるnotenki ever氏に深く感謝致します。また、冒頭の動画の投稿者であるトスカ氏と、マジック統合ルールに関してアドバイスを与えてくれたVienosNotes氏に感謝致します。