💻 computer science

Work-in-Progress: A Tactic for Pattern Matching in Autosubst

本進行中の論文は、POPLMarkおよびPOPLMark Reloadedのチャレンジにおける評価を通じて実証された、型規則、簡約関係、および非一意な解の処理におけるAutosubstの現在の限界に対処する、自動パターンマッチングタクティクスを導入するものである。

原著者： Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

公開日 2026-07-15

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

あなたは、すべてのピースに隠されたラベルが付いている巨大で魔法のようなパズルを解こうとしているところだと想像してください。コンピュータサイエンスの世界では、これらのラベルは「ド・ブラウン指数（De Bruijn indices）」と呼ばれています。これらはコード内の変数を追跡するための巧妙な方法ですが、非常に扱いが難しいことで知られています。これは、椅子（変数）が座るたびに名前を入れ替える「椅子取りゲーム」のようなものです。もし、あなたがパズルのピース（ルール）を穴（ゴール）に合わせようとすると、たとえそれらが実質的に同じものであっても、ラベルのせいで別物に見えてしまうことがあります。

長い間、「Autosubst」というツールがこの物語のヒーローでした。それは、たとえラベルがシャッフルされていても、2つのパズルピースが同一であるかどうかを瞬時に判別できる、超スマートなロボットのようなものです。これは、ピースを同一に見えるまで正規化する（ $\sigma$ -calculusと呼ばれる）一連の魔法のルールを使用することで実現されます。単に2つのものが等しいかどうかを確認したいだけであれば、このロボットは完璧です。

問題：「Apply（適用）」の罠
しかし、落とし穴があります。ルールを「適用」する（ビデオゲームの「Apply」ボタンを押すようなこと）ことで問題を解決しようとする際、ロボットは行き詰まってしまいます。ロボットは「はい、これらは等しいです」と言うのは得意ですが、「このルールをこの特定の穴にどのように適合させるか」を答えるのは非常に苦手なのです。

なぜでしょうか？それは、あるルールが複数の方法で穴に適合する場合があり、助けなしには、どの方法が「正しい」のかをロボットが判断できないからです。過去には、人間であるプログラマーが重労働を担わなければなりませんでした。彼らは、ロボットを機能させるために、ルールを奇妙で間接的な方法で書き換えたり、足りないラベルを手動で推測したりしなければなりませんでした。それは、適切な道具を見つけるのではなく、角を削って無理やり四角い杭を丸い穴に押し込むような作業でした。

新しいアイデア：スマートな推測戦術
この論文は、「as_apply」という新しいツールを紹介しています。これは、ラベルが最初から完璧に一致していなくても、パズルピースを掴んで穴に押し込もうとする、少しばかり冒険的な新しいロボットアームのようなものです。

諦めて人間にすべてを書き換えさせる代わりに、この新しい戦術は、ヒューリスティック（以前見たパターンに基づいた「教育された推測」）を使用します。それは穴を見て、ルールを見て、「もしラベルをほんの少しだけずらせば、うまくはまるはずだ！」と予測するのです。

仕組み（マジック・トリック）
プロセスは2つのステップで行われます。

準備： ロボットはまず、ピースをできるだけ整頓するために、信頼できる従来のAutosubstのルールを使用してパズルピースを掃除します。
推測ゲーム： 次に、ロボットはピースを照合しようと試みます。もしピースが完璧に一致しなくても、パニックにはなりません。代わりに、いくつかの特定のトリックを試します。
- 違いが単純な「シフト」（例えば、変数を1つ上の位置に移動させること）によるものかどうかを確認します。
- 足りないピースが単なる「アイデンティティ（恒等）」、つまり「何もしないこと」によるものかどうかを確認します。
- これらのパズルで通常発生する一般的なパターンを探します。

もしこれらの推測のいずれかが機能すれば、足りないラベルを補完して次に進みます。失敗した場合は、バックトラック（後退）して別の推測を試します。

論文が述べていること（および述べていないこと）
著者たちは、決して過大に宣伝しないよう細心の注意を払っています。彼らは、これがあらゆる可能なパズルを解決する魔法の杖ではないことを認めています。

完璧ではない： 論文では、時には一つのパズルに複数の解決策が存在し、このロボットが間違ったものを選んでしまう可能性があることを明示しています。たとえ正しい答えが存在したとしても、ロボットが誤った推測をするようなトリッキーな例を作ることは可能です。
「進行中の作業」である： 著者らは、これを「進行中の作業（work-in-progress）」として説明しています。彼らは、マッチングに関する理論全体を永遠に解決したと主張しているわけではありません。
結果： 彼らは、この新しい戦術を、POPLMarkおよびPOPLMark Reloadedと呼ばれる2つの有名な困難なチャレンジ（プログラミング言語に関する証明を行うための「オリンピック」のようなもの）でテストしました。
- POPLMarkチャレンジ（642行のコード）において、彼らはこの新しい戦術を15回使用しました。
- POPLMark Reloadedチャレンジ（683行のコード）において、彼らはこれを10回使用しました。
- いずれのケースにおいても、この戦術は目標を成功裏に解決しました。

結論
この論文は、この新しい戦術には理論的な限界（非常に奇妙で、意地悪な設計のパズルによって混乱させられる可能性があること）があることを示唆していますが、現実世界では驚くほどうまく機能することを示しています。これにより、プログラマーはルールを奇妙で間接的な方法で書き直す必要がなくなり、自然に記述できるようになります。

著者たちは、希望を持ちつつも慎重です。彼らは、このアプローチが多くの実用的なケースにおいて古い使いにくい方法に取って代わる可能性があると考えていますが、同時に、ロボットが決して間違った解決策を選ばないようにするための仕事がまだ残っていることも分かっています。彼らは現在、このロボットが100%の確実性を持って解決できるパズルの種類はどれで、どの種類が依然として人間のダブルチェックを必要とするのかを特定するために取り組んでいます。

要約すると、これは、たとえボックスの中の唯一の道具になる準備がまだ整っていなくても、乱雑なパズルピースのマッチング作業をはるかに容易にする、巧妙で役立つ新しいツールです。

技術要約：Autosubstにおけるパターンマッチングのための戦術

問題提起
本論文は、de Bruijn項および $\sigma$ 計算量に基づく置換に関する推論を自動化するRocq（旧Coq）用コード生成器であるAutosubstフレームワークにおける、特定の制限事項を取り上げている。Autosubstは、asimpl戦術を用いて仮定なしのゴールに対する等価性チェックを自動化することには成功しているが、ユーザーが標準的な戦術（applyやeapplyなど）を通じてゴールに仮定（型規則や補題など）を適用しようとする際に失敗する。

これらのシナリオにおいて、ユーザーはゴールを $\sigma$ -等価に関して仮定と単一化（unify）する必要がある。しかし、Autosubstの自動化は仮定に対するマッチングを想定して設計されていない。その結果、ユーザーは以下のような煩雑な回避策を強いられることになる：

間接的な形式（直接的な置換項の代わりに新鮮なメタ変数を使用する形式）で規則を定式化する。
ゴールと仮定の間の溝を埋めるための補助的な補題を導入する。
証明の中で、ゴールを強制的に変形したり、存在変数（existential variables）を明示的にインスタンス化したりする。

核心となる困難さは、 $\sigma$ -マッチング（ $\sigma$ -等価を考慮したマッチング）が唯一ではないという点にある。単一のマッチング問題が複数の解を持つ可能性があり、それらすべてがコンテキストの前件を満たすとは限らない。さらに、完全な $\lambda\sigma$ -計算における二次のマッチングは決定不能であり、 $\beta$ -簡約がない場合であっても、解が一意になるとは限らない。

手法
著者らは、 $\sigma$ -等価を法としたパターンマッチングを自動化するために、RocqのLtac言語で実装された、進行中のプロジェクト（work-in-progress）としてのヒューリスティック戦術**as_apply**を提案している。この戦術は、主に以下の2つのフェーズで動作する：

前処理（Preprocessing）：
- ゴールと対象となる仮定の結論の両方を、既存のasimpl戦術を用いて $\sigma$ -計算に関して正規化する。
- 仮定内の量化された変数を、存在変数（evars）に置き換える。
- 仮定の前件を、マッチングフェーズの後に解決すべきサブゴールへと変換する。
- この戦術は、substifyおよびrenamifyを用いて、明示的な名前変更操作（例： $s\langle\xi\rangle$ ）とインスタンス化操作（ $s[\xi]$ ）の間の変換を処理する。
マッチングフェーズ（Matching Phase）：
- 戦術は、ゴール項とインスタンス化された仮定項との間のマッチング方程式の集合 $M = \{s_i =_\sigma t_i\}$ を構築する。
- 方程式を左から右へと処理し、 $\sigma_{min}$ 断片（インスタンス化と合成性を特徴付ける $\sigma$ -規則のサブセット）によるモジュロ・マッチングを試みる部分的な手続きを実行する。
- ヒューリスティクス： $\sigma_{min}$ $σ_{min}$ がマッチを見つけられなかった場合、戦術は形式的な開発における一般的なパターンを捉えた一連のヒューリスティクスを適用する。これには以下が含まれる：
  - $s[t \cdot \sigma] =_\sigma ?s[t \cdot id]$ という形式の方程式を扱い、未知の項をリフトされた置換（ $?s \mapsto s[\Uparrow\sigma]$ ）でインスタンス化する。
  - 恒等置換や特定の変数構造を含むケースを扱う。
- 置換を適用した後、戦術は仮定を再正規化する。ゴールと仮定が構文的に等しくなった場合に成功と判定される。

この戦術は、複数の相互帰納的なソート、ベクトル置換、および第一級の（first-class）名前変更を含む、Autosubstコンパイラの全入力言語をサポートするように一般化されている。

主な貢献

as_applyの導入： Autosubstベースの開発においてapply/eapplyに代わるものとして設計された、 $\sigma$ -等価を法としたマッチングを可能にするヒューリスティック戦術。
一般化： 複雑なバインダや名前変更操作を含む、Autosubstがサポートする全構文をカバーするようにマッチングロジックを拡張。
実証的評価： 標準的なベンチマーク、具体的にはPOPLMarkおよびPOPLMark Reloadedのチャレンジへの適用。

結果
著者らは、POPLMark（642行）およびPOPLMark Reloaded（683行）のチャレンジ解決策に対してas_applyを評価した。

使用頻度： この戦術は、POPLMark Bの解決策で15回、POPLMark Reloadedの解決策で10回使用された。
有効性： テストされたすべてのケースにおいて、as_applyは意図されたゴールを解決することに成功した。
簡略化： この戦術の使用により、従来の解決策に見られた間接的な規則の定式化、補助的な補題、および手動のゴール変形を排除することができた。
限界： 著者らは、as_applyが $\sigma$ -完全（ $\sigma$ -complete）ではなく、決定器（decider）ではないことを認めている。 $\sigma$ -マッチングは複数の解を持ち得るため、ヒューリスティックな性質を持つ本戦術は、正しい解が存在する場合でも理論的には誤った解を選択する可能性があるが、ケーススタディにおいてそのような失敗は観察されなかった。

意義と主張
本論文は、 $\sigma$ -マッチングの理論的問題（非一意の解、完全な $\lambda\sigma$ における決定不能性）は本質的に困難であるが、実用的なヒューリスティック・アプローチによって、実務における高度な自動化を回復できると主張している。その意義は、de Bruijn構文を扱うユーザーの負担を軽減し、証明支援システムの単一化エンジン（unification engine）の制限に合わせて間接的な形式を用いるのではなく、直接的で自然な形式で型規則や補題を記述できるようにすることにある。

著者らは、現在の研究の状態を「進行中のプロジェクト（Work-in-Progress）」として謙虚に位置づけている。彼らは、無限または複数の解が存在する可能性から、現在の戦術がヒューリスティクスに依存していることを指摘している。今後の課題は、一意性の基準が成立する最大の断片 $\sigma'$ を特定し、将来的には証明された保証を持つマッチング戦術へと繋げることである。

関連論文