HMPOパスポート申請ゲームの論理と自動化

Passport ApplicationはHMPOが提供する書類収集パズルゲームで、10年ごとに更新する英国人証明を遊びながら集める仕組みです。

ゲームではオリジナル書類の郵送提出や、身分証明者探し、翻訳取得、家族協力などのサイドクエストがあり、書類要求には待ち時間による演出もあります。

HMPOは帰納的な「官僚的論理」に基づき、背理法や排中律を使わず、原本提出を『証人』として扱い、祖先まで遡る再帰的な書類要求を行います。

英国籍取得ルールは出生場所や時期、両親の国籍・定住状況に依存し、1983年以前UK出生や天然化が基底ケースとなり得ます。

著者はHaskellのLogicTモナドでこれらのルールをプログラム化し、対話的に証明探索を行い得られる書類セットを自動列挙しました。

プログラムは複数の英国籍証明経路（Proof）を生成し、HMPOは最も複雑な経路を選ぶ傾向があることを示しました。

書類収集の自動化は可能だが、HMPOは誤判定や苦情回避のため完全自動化を避けている可能性があります。