Haskellで英国「パスポート申請」問題を解く

 (jameshaydon.github.io)
1 ポイント 投稿者 GN⁺ 2025-06-29 | 1件のコメント | WhatsAppで共有
  • 英国のパスポート申請手続きを官僚的な文書収集パズルと捉え、国籍証明に必要な文書の組み合わせをHaskellの論理探索で計算した事例
  • HMPOの文書要求は、申請者・親・祖父母の出生地と生年月日、親の国籍・定住ステータス、婚姻状況に応じて、家系図の方向へ再帰することがある
  • 海外出生の子どもの初回パスポート申請で、曾祖父の出生証明書と婚姻証明書まで求められ、1983年以前の英国出生のような基底ケースに到達して初めて再帰が止まる
  • 実装はPrologではなく、HaskellのLogicTとStateT Claims IOで可能な国籍証明Proofを列挙し、各経路に必要なSet Documentを計算する
  • 同じ申請でも複数の証明経路があり得るため、より単純な経路が残っていても実際の要求は長くなる場合があり、自動化は文書準備や要求理由の理解に役立つ可能性がある

パスポート申請を文書収集ゲームとして見る

  • 英国のPassport ApplicationはHMPOが運営するオンライン申請手続きで、標準のオンライン版は開始費用が約**£100**
  • 目的は、複数の官僚機関に散らばる原本文書を集めて「申請者はBritishである」という命題を証明すること
  • 最終報酬は、再申請できる日付が書かれた小さな冊子、つまりパスポート
  • 紙ベースの申請は、郵便に依存する「ハードコア」版に近い

実際の申請で続いた文書要求

  • 事例は、娘に代わってオンラインで「first child passport born abroad」の難易度を選んだ申請
  • 申請は「examiner」が処理するが、申請者はチャットや電話のadvice agentを通じてしか問い合わせできない
    • advice agentの案内は公式決定ではない
    • examinerに質問を伝えると、数日、事例では最大10日ほどの待ち時間が発生する
  • 初期の文書要求のうち約**50%**は、チャットサービスで不要だと案内され、その後も追加の文書要求が続いた
  • 要求メールには壊れたテンプレートのように見える__APPLICANT_NAME__が含まれ、親権証明の条件も明確ではなかった
  • 最終的に、珍しい要求である父方の曾祖父の出生証明書と婚姻証明書が求められた
    • “applicant's Paternal great grandfather”は、2人のうちどちらを指すのか曖昧になり得る
    • これをapplicant's father's father's father's birth certificateと解釈した

HMPOの論理を再帰的な証明問題として解釈する

  • HMPOの論理は、文書ベースのBureaucratic Logicと見ることができる
    • Constructive Logicのように、単なる論理的可能性だけでは不十分
    • 証明には原本文書という「証人」が必要
  • 排中律P ∨ ¬Pをそのまま使うことはできない
    • 例えば「父の父が英国出生か否か」のどちらかは真だと言い、両方のシナリオの文書を提出するやり方は認められない
    • 1つの代替案を選び、それに合った文書を提出しなければならない
  • HMPOの案内によると、1982年12月31日以降に英国外で生まれた人は、一般に出生時点で親の一方が「British citizen otherwise than by descent」でなければBritish citizenにならない
  • HMPOは自らのパスポート記録だけでBritishnessを証明しないため、一部の申請では親・祖父母の方向へ再帰的な文書要求が発生する
  • 再帰は、Britishnessが親に依存しない祖先で止まる
    • 例：帰化した人
    • 例：1983年以前の英国出生者、親に関係なくBritishである基底ケース

事例の要求チェーン

  • HMPOが最初の文書を受け取った日は6月7日で、申請者の出生証明書と申請者の父の出生証明書が含まれていた
  • 6月12日の要求：
    • 申請者の父が1983年1月1日以降の出生であるため、父のBritish citizenship claimの証拠が必要だと案内された
    • その結果、父の父の出生証明書が求められた
  • 6月26日の要求：
    • 申請者の祖父が海外出生なので、British citizenship claimの証拠が必要だと案内された
    • これにより、申請者の父方の曾祖父の文書が求められた
    • 必要な文書は出生証明書と婚姻証明書
  • この再帰はメールでの要求という形で進んだ

Haskell実装の構造

  • 全コードはGitHubにある
  • 当初はPrologで規則をエンコードしていたが、Haskellの**LogicTモナド**へ移行した
  • 目標は単一の文書リストではなく、可能な複数の文書集合を見つけること
    • 国籍主張の方法が複数あるため、必要な文書集合も複数になり得る
    • 概念的にはSet (Set Document)が必要
  • 文書モデルは、申請者と祖先、証明書の種類を型で表現する
    • Parent = Mother | Father
    • Person = Applicant | Parent Parent Person
    • Document = BirthCertificate Person | MarriageCertificate Person Person | NaturalizationCertificate Person | Passport Person
  • 単純な文書リストだけではなぜ十分なのか分かりにくいため、問題を証明探索として扱う
    • LogicTで申請者のBritishnessに関するすべてのProofを列挙する
    • 各Proofに必要な文書集合を計算する

Proofと知識状態

  • 証明型は3つの形で構成される
    • ViaParent Person Proof：親を通じたBritishnessの派生
    • And Proof Proof：2つの主張の結合
    • Evidence Predicate：基礎証拠
  • 必要な質問は実行中にユーザーへ尋ね、過去の回答はすべての分岐とバックトラッキングで再利用する
  • そのためにIO、State、LogicTを組み合わせる
    • type Claims = Map Predicate Knowledge
    • type M a = LogicT (StateT Claims IO) a
  • KnowledgeはSureYes、SureNo、Unsureに分かれる
  • Predicateは規則判定に必要な条件を表す
    • IsBritish Person
    • Settled Person
    • BornBefore Int Person
    • BornInUK Person
    • BornAfter Int Person
    • Naturalized Person
    • Years3LivingInUK Person
    • IsBritOtbd Person
    • Married Person Person

国籍判定規則の核心

  • brit関数は、人がBritishかどうかを判定するルート関数
    • まずIsBritish pを確認する
    • 出生によるBritishnessと、帰化によるBritishnessを探索する
  • 帰化は単純な経路で、帰化証明書1つが主要文書になる
  • 英国出生者は大きく2つの場合に分かれる
    • 1983年以前の英国出生なら、基底ケースとしてBritishnessを得る
    • それ以降の出生なら、親の一方がBritishだったか、当時定住ステータスだったかを確認する
  • 英国外で生まれた場合はより複雑
    • 親がBritish otherwise than by descentかどうかを確認する
    • または、親がBritishで、英国に3年連続で居住した証拠があるかを確認する
  • 「British otherwise than by descent」とは、親からのみBritishnessを得た人ではないことを指す
    • 例：帰化
    • 例：英国出生
    • 例：海外出生だが、親が「Crown Service」勤務中だった場合

親を通じた伝播と2006年条件

  • viaParentは、子が親を通じてBritishnessを得る場合を表す
  • 母親と父親の両方の経路を探索するが、父親経路には追加条件が付く
    • 子が2006年以降の出生なら、父親経路をそのまま使える
    • 2006年以前の出生なら、父親と母親が出生時に婚姻状態だったかを確認する
  • 実装には「registration」のような迂回可能な経路や、一部の性差別的な歴史条項は含まれていない
  • 現在は適用されない法律でも、祖先のBritishnessを判定する際には歴史的に適用される場合がある

実行結果と3つの証明経路

  • run (brit Applicant)の実行は対話形式の質問で進む
    • 例：申請者が英国出生か
    • 例：父がBritish otherwise than by descentか
    • 例：祖父母が定住ステータスだったか
    • 事例では合計37個の質問が続いた
  • ユーザーはdkで分からないと答えられ、その場合は該当分岐の探索を続ける
  • 結果は、申請者に3つのBritishness proofがあることを出力する
  • Proof 1：
    • 申請者は2006年以降の出生
    • 父を通じたBritishness
    • 父は英国出生
    • 父の母が出生時に定住ステータスだった
    • 必要文書は、申請者の出生証明書、父の出生証明書、父の母の定住ステータス文書
  • Proof 2：
    • 父の父の母が1983年以前の英国出生者である経路
    • 必要文書には、申請者、父、祖父、祖父の母の出生証明書と、祖父母の婚姻証明書が含まれる
  • Proof 3：
    • 父の父の父、つまり父方の曾祖父が1983年以前の英国出生者である経路
    • 必要文書には、申請者、父、祖父、父方の曾祖父の出生証明書と、2世代分の婚姻証明書が含まれる
    • HMPOが要求したBirth certificate for Applicant's Father's Father's Fatherがこの経路に現れる

Crown Serviceとさらに複雑な経路

  • 事例では父方の曾祖父のCrown Serviceステータスが混乱を招いたが、実行結果上はそのステータスは必要なかった
  • 父のBritish otherwise than by descentステータスは、英国出生と祖父の単純なBritishnessからすでに導出されている
  • ただし、祖父の単純なBritishnessは依然として証明する必要があるため、再帰は祖父の世代へ降りていく
  • 祖父の「legitimacy」を証明するため、婚姻証明書も必要
  • HMPOが選んだ経路は、3つの中で最も長く複雑なProof 3
    • Proof 1は、1人の祖先の定住ステータスだけを証明すればよい、より単純な経路
    • 非Britishの定住祖先を通じた市民権は非再帰的なので、より単純になり得る
    • ただし、特定時点の定住ステータスを証明すること自体は難しい場合がある

実装上の限界と自動化の判断

  • orElseは最初の分岐が成功すると2つ目の分岐を探索しないが、<|>は両方の分岐を探索する
  • 一部の規則では<|>を使うと、より多くの市民権証明経路が出るが、HMPOが先に特定の経路を使い切ろうとしているように見える場合がある
  • 実装は、特定時点の条件を十分に精密には追跡していない
    • 例：婚姻状態や定住ステータスが特定人物の出生時点で成立していなければならない場合
    • これは難しくなく追加できる部分と見ている
  • 英国国籍法全体を実装したものではなく、事例に関連するか興味深い部分だけをエンコードしている
    • 全体実装には、はるかに多くのコードと多くの例外が必要
  • こうしたソフトウェアがあれば、正しい文書集合をより早く用意し、要求が複雑になった理由を理解するのに役立った可能性がある
  • 完全自動化にはリスクもある
    • プログラムがfalse positiveを出すと、「コンピューターができると言った」という抗議が起こり得る
    • 人間の専門性を置き換える自動化は、「コンピューターができないと言った」という理由で市民権が拒否される状況につながり得る
  • 現在の申請はまだ終わっておらず、Proof 2とProof 3を同時に進め、失敗したらProof 1を試す予定

関連記事

1件のコメント

 
GN⁺ 2025-06-29
Hacker News のコメント

  • この10年でいくつかの大規模な英国政府システムに関わってきたが、この記事は政府サービス／ソフトウェアを作るときに奇妙な結果が生まれる理由をよく示している。
    政府ソフトウェアは本質的に、何百年分もの議会法をコードに移し替える作業だ。HMPO のパスポートシステムを作ったとして、その根拠となる法律が変わったり廃止されたりすると、誰かが全システムの中からその法律が影響している箇所を見つけて直さなければならない。
    そこに、政府が高額なコンサルティング会社へ頻繁に外注し、業者側には契約を広げ、顧客から最大限の価値を引き出し、居場所を確保しようとする動機がある。品質や柔軟性にばらつきのあるシステムを作るため、法律が変わるたびに同じプロセスが繰り返される。
    以前は Spend Controls のような中央の意思決定権限があったが、今はこの問題を調整する中心がなく、そのため政府サービス提供のコストがこれほど高くなっている。

    • なぜ契約上、下請け業者に動くシステムを作る義務がないように見えるのか不思議だ。
      実際には動くものに近い何かを作り、ジュニア開発者1人が3か月で作れそうな成果物に対して1000倍くらい過大請求しているのに、システムが実際に動いたかのように支払いを受けているように見える。
    • 最近フランスでパスポートを更新したが、必要な書類をすべて申請できる比較的新しいプラットフォームがあり、オンラインフォームを1つ記入するだけでよかった。
      フォームは分かりやすく、その後オフィスに一度行って手続きを終えたが、10分しかかからず、パスポートは配送された。可能な限り苦痛の少ない手続きだったと思う。
      英国の状況がどうであれ、絶望的ではない。政府は実際の職員を雇うことを恐れず、開発をすべて内製化すべきだ。
    • 再利用可能なオープンソースのルールシステムに機会があるのではないかと思う。あらゆるレベルの政府が、ルールを表現力豊かに定義し、バージョン管理できるシステムを使えるはずだ。
      指摘されているように技術業務がすべて外注化されており、かなり革命的な再設計を構想し実行する組織内部の能力が不足していることが、ギャップの一部に見える。
      政府が IT プロジェクトに下請け費用として何千万も使いながら、長期的にはより安く済むかもしれない内部エンジニアに市場価格を払えないのは非常にもどかしい。
    • 法律が本質的に、修正条項が延々と追加されていく追記専用リポジトリのようになる問題は、英国だけの話ではない。
      あちこちに例外条件文をばらまく代わりに、追記専用の形で「パッチ」だけを適用できるシステムがあればよいのにと思う。
      一部の論理型プログラミング言語ならある程度は可能だが、本当の問題は技術的負債の予算がなく、法律を扱う弁護士たちも複雑さから利益を得られる場合があることだと思う。法律をできるだけ単純に保つことを専任する人たちがいればよいのだが。
    • 外注が誰かにとって本当に成功したことはあるのだろうか。政府が何かを外注して成功したという話を、ほとんど聞いたことがない。

  • Haskell の構文は興味深い。誰かに説明してもらった後なら直感的だが、説明される前はそれほど直感的ではない。
    Algol 系の言語（C、Python など）に慣れているからだけではないと思う。これまで見た Haskell コードには、コードを簡潔にするための演算子が多すぎて、見ただけでは何をしているのか明確ではなかった: https://academy.fpblock.com/haskell/tutorial/operators/

    • 以前ざっくり数えてみたことがあるが、lens やドメイン特化ライブラリを避けた「普通の」Haskell コードで出会う演算子の数は、JavaScript で出会う演算子の数とかなり似ていた。
      かなり前なのでやり直したくはないが、JavaScript 側に甘めに見積もっても、実務 Haskell に必要な演算子は実務 JavaScript の10倍ではなく、だいたい2倍程度だ。
      Haskell には序盤に受け入れなければならない付随的な複雑さがあるが、人気の入門言語と種類が違うのではなく、程度が違うだけだ。Algol スタイルの言語について自分がどれほど多くを学んできたかは、すでに内面化しすぎていて忘れやすい。
      プログラミング初心者の中高生に Java と Python を教えたことがあるが、特に1対1で見ると、こちらが説明の必要があることすら忘れていた点でつまずくことがよくあった。Python で : の位置を間違えたり、= がどう動作するのか理解できなかったりする、といった具合だ。
      : や = のような「基本」構文でさえ、私たちが思うよりずっと複雑だ。英語ネイティブが “big red ball” と “red big ball” の形容詞の順序規則を意識しない一方で、学習者には壁のように立ちはだかるのと似ている。
    • そのリンクにある演算子の大半はごく標準的なもので、Haskell について語るときには最も面白くない部類に入る。
      プログラミングを知らない状態で任意の Java プログラムを手に取れば、やはりほとんど理解できないだろう。数学の授業を一つも受けずに数式を読もうとすれば、演算子であれ何であれ理解できないのと同じだ。
      基準にすべきなのは、基本を学び、チュートリアルをいくつかこなした後でどれだけ理解できるかだ。
    • 「説明してもらった後なら直感的だが、説明前はそうではない」というのは、直感的という意味にかなり近いのではないかと思う。
      直感的というのは、事前知識や説明がなくても簡単に理解したり学んだりできる、という意味に近い。
    • Larry Wall が Perl について似たようなことを言っていた気がする。あるものは、学んだ後で初めて直感的になり得る。
      不満の対象も、実は構文ではないように思う。Haskell の一部の構成要素はモナドやレンズのような特定のモデルを参照しており、読者がその知識をすでに持っていなければ、どんな構文もその知識を注入してはくれない。

  • この記事はよかった。最初はパロディとして始まり、徐々にその「ゲーム」に対する真面目でエレガントな解法へと変わっていく。
    終わるころには、自分でも試してみたくなるほどだった。

    • プレイすることはできそうだが、後半を突破するのはずっと難しそうだ。

  • 英国のパスポート申請は、必要書類を HMPO に郵送することを除けば完全にオンラインで完結できる。
    養子縁組、帰化、血統によって「新たに」市民になった場合でも、英国外からモバイル端末だけで、別途アプリをダウンロードせず、写真撮影まで含めて新規パスポートを申請できる。
    冗談半分で紙とペンを使って「ハードモード」を遊ぶこともできるだろうが、私の経験では非常に効率的で、速く、シンプルだった。

    • 昨年、英国のオンラインパスポート更新システムを使ってみたが、久しぶりに使ったウェブサイトの中で最高だった。本当に新鮮だった。
      古いコンピューターと「古代」のブラウザーでも完璧に動作し、色、テキスト、ボタン、入力欄、要件がどれもシンプルでアクセシブルで明確だった。ステップごとのナビゲーションもシンプルで、実際に親切だった。
      もっと多くの企業が顧客を十分に気にかけて、このようによく設計されたウェブサイトに投資しないのは残念だ。HMPO はよくやった。
    • 最近オンラインシステムで初めて更新してみたが、全体の手続きは例外的に速かった。カリフォルニアから申請したが、2週間もかからずにパスポートが戻ってきた。
      比較すると、カリフォルニアでカナダのパスポートを更新したときは、3年で損傷したパスポートで、4か月かかった。完全に紙ベースで、推薦人や写真店のスタンプが押された写真を要求するなど、ばかげた条件があった。
      デジタル試行事業が進行中なのは知っているが、できるだけ早く全面導入すべきだ。
    • 実際よりずっと単純に見えるように言っている気がする。更新手続きがかなりうまく簡素化されたことは認めるが、数年前に友人の初回パスポート申請を手伝った立場からすると、手続きは長く退屈だった。
      対面面接が必要で、多くの人には頼みにくい責任ある人物の署名も必要だ。たとえば医師は認められない。

  • 日本でこの手続きをする人のために、私が提出しなければならなかった書類はこうだった。状況によって違うだろうし、特に投稿者も英国外で生まれたようなので、別の書類やより多くの書類が必要だった可能性がある。
    提出したのは、英国 General Register Office で注文した出生証明書の認証コピー、日本の戸籍の原本と翻訳、出生届受理証明書の原本と翻訳、婚姻証明書の原本と翻訳、子どもの日本のパスポート全ページのカラーコピー、子どもが私の子であることを確認してくれる米国または英国市民のパスポートコピーだった。
    手続きはかなり不明確で、基本的には担当者が満足するまで書類を出し続ける構造に見える。

    • この場合、実際には applicant's father、つまり私は英国生まれだったが、applicant's father's father は英国生まれではなく、それが追加の複雑さの原因だった。
    • 興味深い。親の出生証明書は求められなかったのか？
      私は英国人で妻はハンガリー人、ハンガリーに住んでいるが、双方の親の出生証明書と、4人の祖父母全員の出生証明書を求められた。
      妻が父親と連絡を取っていないため、事情を説明するカバーレターを提出し、受け入れられた。ただ、いずれにせよ息子の英国国籍は私の英国国籍に由来するのだから、妻の国籍や妻の両親の国籍がなぜ関係するのかはよく分からない。
      他人のパスポートをコピーする必要はなかったが、家族の友人がオンラインで確認する必要があった。その友人は英国の弁護士なので、承認された職業リストに入っていた。
    • 子どもの日本のパスポート全ページのカラーコピーとは、なぜ必要なのだろう？

  • 米国で生まれた娘のために MN1 申請をしなければならなかった。私と配偶者がどちらも海外生まれだったからだ。
    元記事が示唆しているように、これは「登録」という一種のサイドクエストで、子どもが18歳になる前にやらないと期限切れになる。もちろん、こうした状況でも市民権を得られるルートはまだあると理解している。
    手続きで最も難しかったのは、このバージョンの Passport Application では扱われていないが将来の DLC パックに出てきそうな、自分の証拠書類を認証してくれる人を見つけることだった。原本を提出するよう書かれているが、パスポートを含む書類を3〜6か月保管するので、海外居住者には非現実的だ。
    正確な規則は覚えていないが、米国の公証人や一般的な弁護士による認証手続きは使えず、結局区役所に行く必要があった。
    5か所ほどの区役所に電話したが、どこも手続きや要件を知らないと言い、最終的に Islington Council でとても親切な人を見つけた。それでも、私が経験した英国政府とのやり取りの中ではかなり苛立たしい部類だった。

  • 私も代理で Passport Application ゲームを楽しんだことがある。
    元記事が触れていない興味深いルールの1つは、可変歴史ルールだ。1つの文書に含まれる事実が短期間でも変わり得るため、すでに審査官の事実記録システムにスキャンされた文書を、後で再スキャンするために返送しなければならないことがある。
    文書の事実が変わっていないか検証するということは、審査官という種族が多元宇宙の存在を暗黙に認めているという意味だ、と言われている。
    「NPC」の電話相談員と審査官の間の通信チャネルは祈りに似ているようで、実際に得られるのは曖昧な推論だけだ。
    ついでに言うと、元記事の筆者は Mornington Crescent 愛好家なのかもしれない。先ほどの Passport Application とルールの位相が似ているゲームだ。

    • 英国の制度では名前が流動的で、別途宣言なしに好きに変えられる。そのため、私の母は自分の母親の3度目の結婚姓で私の出生届を出すことができた。
      出生証明書もある意味では変更不能だが、そこに書かれているすべてが完全に変更不能というわけではない。
      さらにパスポート事務所は、こうした姓の不一致を説明して通した私の以前のパスポートに関する判断を忘れていた。しかも、あるパスポートでは私は母のパスポートの1ページに載っていたことすらあった。
      NPC たちは本当に腹立たしい。電話やメールをするたびに答えが違った。ひどい大規模言語モデルのようだった。
      申請後、母に、同じ束の申請書の中で一人の娘には追加の英国書類が必要だが、もう一人の娘には必要なくパスポートが発行された、と説明しなければならなかった。ただ一人は英国で生まれ、もう一人はそうではなかったからだ。
      母は当然爆発し、国会議員に問題を提起し、1日で解決した。

  • 娘の一人のために、この地獄のような手続きをちょうど経験したところだ。娘は日本で生まれ、私の出生証明書に記載されたものと母の姓を一致させるのに苦労した。
    短く言えば、私がイングランドで生まれ、市民権、つまりパスポートを持っていることを証明したのだから、どんな可能性を考えても娘に伝えられる地位であるはずに見えた。必要書類のガイドラインとは合わないが、はるかに苦痛の少ない方法だと思う。

  • 「基底ケースは何か？ 基底ケースとは、イギリス人としての地位が親に依存しない祖先、たとえば帰化した人や1983年以前にイギリスで生まれた人のことだ。1983年から未来へ離れるほど、この呼び出しスタックは深くなる」という部分は、市民と外国人居住者に関する中央データベースがあり、市民権の確認はSQLテーブルに対する単一の SELECT 程度で済む国から来た身としては、正気とは思えない

    • 多くの国には、自国民が誰なのかを知る方法がない
      海外で生まれた人も市民であることが多く、イギリスは市民権に影響する領土変更をとんでもない数経験してきた
      現在の市民の一部はBombay、つまりMumbaiで生まれたために市民権があり、別の一部はHong Kongで生まれたために市民権がある
      信頼できる市民名簿を維持するには定期登録が必要で、登録しなければ市民権を失うようにしなければならない
    • 市民権の確認がSQLテーブルに対する単一の SELECT で済む可能性はないと思う。自分に極端に不利なオッズでも、喜んで賭けてもいい

  • 数年前にこのゲームをやったことがある
    イギリスでイギリス人の父のもとに生まれたにもかかわらず、自分のキャラクターは以前はイギリス人ではなかった。両親が結婚しておらず、1983年以降だが2006年の規則変更前の出生だったからだ
    正確な時期ははっきりしないが、2010年代のどこかで2006年のアップデートが遡及適用され、自分のキャラクターもプレイ可能になったようだ。サイドクエストはあまり多くはなく、主なものは父の出生証明書を探すことだった
    自分のキャラクターもエンドゲームの儀式に出席して女王への忠誠を誓わなければならなかったが、この国で生まれ、生涯ここで暮らしてきた人間にとっては奇妙に感じられた

    • それでもボーナスのエンディングクレジットはもらえたね！