Haskellで英国の「Passport Application」問題を解く

• 英国のパスポート申請手続きをパズルゲームのように捉え、この複雑な申請プロセスを Haskell でプログラミングしてルール化した経験を扱う
• オンラインのパスポート申請では、さまざまな書類収集と複雑なルールの解釈、そして予期しないサブクエストが中核的な面白さとなっている
• 申請プロセスの論理を「Constructive Logic」と結び付け、それぞれの証明を裏付ける原本書類が必須であることを強調
• Haskell のLogicT モナドと状態管理（State）を活用し、必要書類の一覧と英国市民権証明の論理的な経路を追跡
• HMPO は実際には最も複雑な証明経路を最初に要求する傾向があり、自動化ツールは複雑な法解釈の限界から導入が進んでいない

---

はじめに: パスポート申請をゲームとして見る

• 最近はプログラミングでオンラインゲームやパズルを解く流れが強まる中、英国の Passport Application もそのような試みの対象として扱われる
• Passport Application は約 £100 の費用と徹底してミニマルなテキストベースのデザインを持ち、英国人が 10 年ごとに楽しむ一種の「アドベンチャーパズル文書収集ゲーム」である
• このゲームの目的は、複数の官公庁を通じて複数の証明書類（artefacts）を集め、「この申請者は英国人である」と複雑な法的基準の下で証明することにある
• ゲームの報酬はパスポート冊子 1 冊と「次回プレイ可能日」である

ゲームの構造と難易度

• 紙ベースのオフライン版は書留郵便と認証手続きで進み、各段階で集めるべき書類が説明書または表の形で案内される
• 初期手続きは比較的簡単だが、ゲームが進むにつれてさまざまな「サイドクエスト」や難関が現れる
  • 例: 特定の職業に就く知人に本人確認を依頼する、外国語書類の認証翻訳を確保する、家族で協力プレイをする、各官公庁固有の行政手続きを探検する、など

体験談: 「初の海外出生子女」難易度への挑戦

• 筆者は自分に代わって幼い娘の「初の海外出生子女」難易度に挑戦し、すでに多くの経験があったため相当な難しさを予想していた
• 初期に要求された書類の半分は後になって不要だと分かり、書類要件と説明はかなり曖昧で混乱しやすく設計されている
• 担当審査官（examiner）とは直接やり取りできず、相談中継エージェントを通じた非公式な支援しか受けられない
• 追加の要求書類が繰り返し発生し、ときには存在しない書類まで求められ、珍しい家系の祖先の出生証明書・婚姻証明書の提出まで要請されるなど、難易度は徐々に上がっていく

HMPO の論理: Bureaucratic Logic

• パスポート申請の論理は Constructive Logic（構成的論理）から派生した Bureaucratic Logic（官僚的論理）として見ることができる
• 単純に「真 / 偽」を証明するのではなく、各ルールに対応する原本書類による証拠を直接提出しなければならない
• 排中律（Excluded Middle）は認められないため、「どちらかのシナリオが正しいはずだ」という形では証明できず、必ず一つの経路に従って書類を提出しなければならない
• 特に「Britishness」は親の国籍に依存しており、書類要求は家系図の形で再帰的に進んでいく
  • ベースケース: 1983 年以前に英国で出生、帰化など、親の証明が不要な場合

Haskell コードによるルールのモデル化

• ルールのモジュール化と推論の自動化を目的として、Haskell（特に LogicT モナドの活用）で申請ロジックをプロトタイプ化
• Person / Document / Proof などの型を宣言し、各条件に応じたさまざまな証明書類の経路をモデル化
• Britishness を証明する関数は、input（各 person に関する情報）とともに可能な**複数の証明経路（Set of Proofs）**を探索する
• Proof ツリーに沿って必要な**最小書類の組み合わせ（Set of Set Document）**を算出
• StateT と LogicT IO の組み合わせでインタラクティブな問い合わせと状態共有を行い、「分かっている情報」に応じて分岐とバックトラッキングを実施
• 英国市民権構造の分析ロジック:
  • 帰化証拠による単一路線
  • 1983 年以前の英国出生時の条件付き（ベース）経路
  • 親を通じた再帰的証明（適法な婚姻などの追加条件を含む）
  • 親が BOTBD（British Otherwise Than By Descent）かどうかによる特例経路の追加
  • Crown Service などの例外規定もコード内で処理

実行例と証明経路

• ghci を通じて実際の入力（申請者の出生地、親の国籍など）に応じ、合計 3 つの証明（Proof）経路が自動的に導出される
• 各証明経路ごとに、必要書類（certificate、marriage certificate などの組み合わせ）の一覧が算出される
• 最も複雑な経路では、祖先までさかのぼる再帰的証明と婚姻関係の立証が必要になることが確認できる

議論と結論

• 現実には HMPO がわざと最も複雑な証明経路を最初に要求しているように見え、実際の法的矛盾や細かな規定は別個のガイドラインや**「balance of probabilities」**の原則に従う
• 自動化ツールが普及すれば、申請者は自分の証明経路と必要書類をはるかに容易に把握できるようになる
• しかし法律はきわめて微妙で可変的であるため、「コンピュータが yes / no verdict を出す」ような単純な自動化には危険がある
• 筆者は現在、2 番目と 3 番目の経路で証明を試みている

---

参考コードと文書構造の要約

• Haskell コード全体は GitHub で確認できる
• さまざまな型、証明経路、モジュール構造、問い合わせ関数など、Haskell ロジックの詳細実装を確認可能

[GN⁺]

Hacker Newsのコメント

• 過去10年間にさまざまな大規模な英国政府システムで働いた経験談。英国政府ソフトウェアの開発とは、数百年にわたる議会制定法をコード化する作業だという説明。HMPOのパスポートシステムのように、法律が変更されると各システムでその法律が影響する箇所をすべて見つけて修正しなければならない難しさがある。政府はこの作業を高額なコンサルティング会社に外注するが、彼らは契約をできるだけ長引かせ、顧客から利益を最大限引き出す動機を持っている。その過程でシステムの品質や柔軟性はまちまちで、法律がまた変わればこの複雑な手順を再び繰り返す。中央で意思決定を行ってこの問題を調整する機関が不足していることが、政府サービスを高コストにしている
  • 政府の外注が実際にうまく機能した事例があったのか気になる。政府が何かを外注して成功した話を一度も聞いたことがない
  • 外注業者に「動作するシステム」についての契約上の義務がないように見える理由への疑問。見栄えのするシステムを作りながら、実質的に正常動作しないシステムに対して過大請求している現象が気になる
  • 最近フランスでパスポートを更新した経験の共有。すべての書類用の新しいプラットフォームがあり、オンラインフォームを1つ記入するだけで、オフライン訪問は1回で終了。10分で完了し、パスポートも迅速に配送された。英国も絶望的というわけではなく、実際の開発者を正社員として採用し、開発を内製化すべきだという考え
• DSLを使ってオランダ税法を自動化・コード化した事例を思い出す。関連資料として Jetbrains DSLケースプレゼンテーション を推薦
• 「base case」とは市民権判定の構造を説明する文脈で、1983年以前に英国で出生した人は親に関係なく市民資格を持つという例が紹介されている。自分は市民権がSQLテーブルでSELECTを1回実行すれば終わる国の出身なので、こうした構造は信じがたい
• Haskellの文法が直感的だという評価について、誰かに説明してもらえば直感的だが、それまでは直感的ではないという意見。Haskellは演算子が多すぎて、コードを見てもすぐには意味を把握しにくい例として Haskell演算子チュートリアル のリンク共有
  • Haskellで実際に使われる演算子の数を大まかに数えてみると、JavaScriptとほぼ同じか2倍程度だという主張。Haskellには初期の参入障壁があるが、JavaやPythonなど最初に学ぶ言語もそれなりに複雑であり、学んで身につければ簡単に感じるだけ。Pythonの基礎文法である : や = も初心者には混乱ポイントなので、直感性は慣れの結果だという意見
  • 誰かに説明してもらったあとに直感的になるというのは、結局それは直感的であることにかなり近い概念だという議論
  • Larry WallがPerlについて似たようなことを言っていたという話。実際には構文の問題ではなく、Haskell固有の概念（モナド、レンズなど）を知らなければ、どれだけ構文が単純でも理解自体が難しい
  • リンク先の演算子の大半は、プログラミング初心者にとってはごく普通の部分だという指摘。Javaプログラムや数式も文脈なしに見れば同じように理解できない。基準は、基本知識を学んでチュートリアルを何回かやったあとに、どれだけ理解できるかであるべき
• このコンテンツは最初はパロディのように始まるが、次第に真面目で優雅な解決策へと発展していく。最後には自分も実際にこの「ゲーム」をプレイしてみたくなった
  • 実際にプレイ可能だが、終盤のエンディング区間ははるかに難しいというコメント
• 日本で実際に英国パスポート関連書類を提出した経験の共有。状況によって提出書類が変わることがあり、自分は本人および子どもの出生証明書、日本の戸籍謄本の原本、翻訳文、出生届受理証明書など多数の書類を用意。各ページのカラーコピーや、他人のパスポートの写しまで求められた。手続きは非常に不明瞭で、結局要求が満たされるまで書類を出し続ける構造になっている
  • コメント投稿者の父親は英国生まれだが、祖父が外国生まれだったため、さらに複雑になったという状況説明
  • 日本では親の出生証明書の要求はなかったという点。自分はハンガリーと英国の国籍を持ち、ハンガリー在住だが、両親と祖父母4人全員の出生証明書を求められた。妻とは親族関係が疎遠だったため事情説明書を添えて受理された経験があり、自分の国籍においては母方の国籍や出自は事実上重要ではないにもかかわらず、家族ぐるみの友人（法律家）にオンライン確認を依頼した状況も共有
  • 子どもの日本のパスポートの全ページをカラーコピーで提出した理由が気になる
• 英国のパスポート申請はオンラインですべて処理可能で、新規市民（養子縁組、帰化、血統）の新規申請もモバイル機器だけで、別アプリなしに写真撮影まで可能。自分の経験では効率的で速く、直感的なプロセスだった
  • 最近オンラインのパスポート更新システムを使ったが、ここ数年で触れたウェブサイトの中で最高だという評価。古いコンピューターや古いブラウザーでも完璧に動作し、非常にシンプルで誰でも使いやすいUI、親切な段階的ナビゲーション。こうした設計がビジネス分野にももっと広がってほしいという願いと、HMPOへの賛辞
  • 最近オンラインシステムを初めて使ってみたが、米国カリフォルニアでも2週間で非常に速くパスポートを受け取れた。カナダのパスポート更新体験は4か月もかかり、手続きも書類も面倒だった。スマートフォンベースのデジタル更新パイロットが拡大導入されることを期待
• 日本で娘のパスポートを準備する際、出生証明書上の親の姓の不一致問題などで大変苦労した。結局、自分が英国生まれで市民権（パスポート）保有者なので直系の子どももそれを継承できると説得した。標準の要求書類とは一致しないが、それでもまだ苦労は少ないほうだという
• 「パスポート・アプリケーション」ゲームを代理体験したという経験談。「mutable history」ルールが興味深い。特定の書類の事実関係が短期間でも変更される可能性があるため、すでにスキャン済みの文書も再提出・再スキャンしなければならない場合がある。この過程は審査官たちが平行宇宙（multiverse）を暗黙に認めていると見ることもできる、という冗談。「NPC」役の相談員や実務担当者とのコミュニケーションは、一方通行の祈りのような感じで、うまく伝わらない。OPはMornington Crescentというゲームのファンではないかという推測。パスポート申請とルールが似ている
  • 英国の制度では名前を自由に変えられるため、自分の母でさえ3度目の結婚後の姓で自分の出生登録が可能だった。出生証明書も一部項目だけが不変で、完全に不変というわけではない。パスポートオフィスは過去の履歴すら忘れることがあり、自分のパスポート関連の姓の不一致は以前に説明したのに再び問題になった。相談員（NPC）に電話、メール、問い合わせをするたびに異なる答えしか返ってこなかった。GPTのように一貫性がなかった。同じ書類を出しても、一人の娘には追加要求が来て、もう一人の娘には何の問題もなく発行されたこともあった。それを母親が国会議員に苦情を言ったところ、1日で解決した
• 数年前にパスポート・アプリケーション「ゲーム」をプレイした経験の共有。自分は英国生まれで、父も英国人だったが、両親が未婚で、1983年以降かつ2006年の規定改正前の出生だったため、当初は市民ではなかった。2010年代ごろに2006年法が遡及適用されて市民と認められた。主な「クエスト」は父の出生証明書原本の提出で、最後には「女王への忠誠宣誓式」への強制参加まであり、奇妙だった
  • 少なくともエンディングクレジットはある、という冗談