MaudeTypedLog: A Typed Interpreter for Prolog in Maude

あなたは、トランプの家を作っているところを想像してください。コンピュータサイエンスの世界には、プログラミング言語「Prolog」と呼ばれる、熟練した建築家のような言語があります。しかし、そのルールブックは非常に寛容です。重いレンガを繊細な紙のテントの上に載せようとしても、彼は気にしません。ただ、それらがうまく組み合わさるようにしようとするだけです。もしレンガが重すぎれば、後で全体が崩壊するか、あるいは建築家は「これはうまくいかなかった」と言うだけで、なぜ失敗したのかについては教えてくれません。これは、Prologが伝統的に「型なし（untyped）」であるためです。つまり、パーツを結合しようとする前に、それらが正しい形や素材であるかどうかをチェックしないのです。

しかし、時には建築家の方が物事を知っていることもあります。もし、特定のやり方で数値のリストと単一の数値を混ぜ合わせようとした場合、彼は手を挙げて「エラー！」と叫ぶかもしれません。しかし、それは建物がすでに揺れ始めてから起こることです。長年、コンピュータサイエンスの研究者たちは、Prologに優れたルールブック（型システム）を与えようと試みてきました。目的は、建物を組み立て始める前に素材をチェックすることです。問題は、ほとんどの試みが人間にとって使いにくすぎるか、あるいはあまりにも曖昧で、明らかな間違いを見逃してしまうことです。それは、屋根について具体的に尋ねた時にだけ検査を行う安全点検員や、「おそらくレンガは大丈夫だろう」と、明らかにゼリーでできているのに言う点検員のようです。

ここで、新しいツールが登場します。研究者のEnrique Gallifa-Tronch、João Barbosa、そしてSantiago Escobarによって構築された、MaudeTypedLogという、非常に厳格な新しいインタプリタです。これは、Prologの設計図を取り出し、Maudeと呼ばれる魔法のような高速シミュレーションエンジンに通すようなものです。このエンジンは、単にパーツを組み合わせようとするだけでなく、パーツ同士がそもそも接触することを許されているかどうかをチェックします。もし「数値」を「単語」に接着しようとすれば、マシンは即座に停止し、「型エラー（Type Error!）」と叫びます。

この論文は、この新しいインタプリタを紹介しています。これは、特定の「三値論理（three-way logic）」システムを使用した、この種のものとしては初のものです。単に「はい（動作する）」または「いいえ（動作しない）」と言う代わりに、このシステムは「間違い（型エラーである）」と言うことができます。著者たちは、これがうまくいくと推測しただけではありません。彼らはコードを書き、インタプリタを構築し、いくつかの論理プログラムでテストを行いました。彼らは、自分たちのツールが、他のツールが見逃す可能性のあるプログラム（命令）とクエリ（質問）の両方の間違いを、正常に特定できることを示しました。また、彼らは、単に「犯罪が起きた」と言うだけでなく、正確に容疑者を指し示す探偵のように、問題を引き起こしている特定のコードの行を正確に指し示すことができることも実証しました。彼らは、自分たちのツールがまだ完璧ではなく、複雑な数学的機能のテストが必要であることを認めていますが、彼らのシミュレーションは、Prologプログラムをチェックするこの厳格な方法が、エラーを早期に発見するための実行可能で強力な手段であることを証明しています。

MaudeTypedLogの物語

問題点：チェックを行わない「接着剤」
Prologは、パズルや論理問題を解くために使用される言語です。それは事実とルールのリストを取り込み、それらを組み合わせて質問に答えようとします。伝統的に、Prologは「型なし」です。あなたが靴下を合わせるゲームをしていると想像してください。Prologでは、赤い靴下と青い靴を合わせようとしても、ゲームは諦めるまでそのまま試行を続けます。それは、「おい、それらは同じ種類のオブジェクトですらないぞ！」と叫ぶことはありません。たとえ最後まで行ったとしても、単に「一致しません」と言うだけで、靴下が問題だったのかどうかは説明してくれないかもしれません。

著者たちは、これが危険であると主張しています。プログラムが「いいえ」と言うとき、それは本当に答えが「いいえ」である場合（例：2は[1, 3]の中に存在しない）もあれば、不可能に思えることをしようとしたために「いいえ」となる場合（例：単語のリストの中に数値を入れようとする）もあります。Prologは両方を同じ「いいえ」として扱うため、混乱を招きます。

解決策：三色の信号機
研究者たちは、Prologプログラムを実行しながら、あらゆるステップで厳格な「型チェック」を追加するインタプリタ、MaudeTypedLogを構築しました。単純な「緑（進め）」と「赤（止まれ）」だけの信号機ではなく、このシステムには第三の光、**「黄色（間違い）」**があります。

• 緑（真/True）： パーツが適合し、型が一致し、論理が機能しています。
• 赤（偽/False）： 型は一致していますが、論理が機能していません（例：2はリストの中に存在しない）。
• 黄色（間違い/Wrong）： パーツは適合できません。なぜなら、型が間違っているからです（例：単語に数値を足そうとする）。

この「黄色」の光こそが、核心となる革新です。これにより、システムはプログラムがクラッシュしたり、混乱を招く回答を出したりする前に、即座に停止することができます。

どのように構築したか
これを実現するために、著者たちはMaлоdeと呼ばれる強力なツールを使用しました。Maudeは、ルールを非常に高速に書き換えることができる、超強力なシミュレーションエンジンです。著者たちはPrologのルールを取り出し、それをMaudeの中で書き換えました。

1. 型付き単一化アルゴリズム（The Typed Unification Algorithm）： これが核心となるエンジンです。通常のPrologでは、「単一化（unification）」とは二つのものを同じに見せるプロセスです。MaudeTypedLogでは、「型付き単一化」アルゴリズムを作成しました。二つのものを結合しようとする前に、それはそれらの「型」をチェックします。もし型が一致しない場合、単に失敗するのではなく、特定の「Wrong（間違い）」信号を返します。
2. TSLD-Resolution： これは、彼らがパズルを解くために使用する方法の、洗練された名称です（標準的なPGLD-resolutionのアップグレード版です）。これは、「T」が付いた「Typed（型付き）」のSLD-resolutionです。これは、問題を解決するためのあらゆる方法のツリーを構築します。もしツリーの枝が「Wrong」信号に当たると、その枝は即座に切り落とされ、システムはどのルールがエラーを引き起こしたのかを正確に把握します。

何を発見したか
著者たちは、いくつかの例を用いて新しいインタプリタをテストしました。

• 例1： 彼らは、ルール r が、数値のリストと文字のリストの両方に含まれる数値を見つけようとするプログラムを作成しました。システムは、一部の経路が機能する一方で（数値の1を見つける）、他の経路は数値と文字を混ぜようとしたために「Wrong」信号に当たったことを正しく特定しました。
• 例2： 彼らは、隠れた型エラーを持つプログラムを作成しました。一つのルールが、数値用のスロットに文字を入れようとしました。彼らが「チェック」コマンドを実行したとき、MaudeTypedLogは単にプログラムが失敗したと言うだけでなく、原因となった特定のルール（節3）を直接指し示しました。

結果は、ツールが理論通りに動作することを示しました。これは、プログラム自体と、プログラムに対して投げかけられた質問の両方において、型エラーを検出できることを示しています。

現時点での限界
著者たちは、自分たちの仕事の限界についても正直に述べています。彼らのツールはプロトタイプです。現在のところ、Prologが通常備えている複雑な数学関数（平方根を計算したり、動的に数値を加算したりするなど）をすべて扱うことはできません。また、プロフェッショナルなPrologプログラムが使用する大規模なルールライブラリについても、まだテストを行っていません。彼らは将来、これらの高度な数学的機能をツールに教え、木構造のようなより複雑なデータ構造を扱えるようにする必要があると示唆しています。

なぜ重要なのか
この論文は、コンピュータサイエンスのあらゆる問題を解決したと主張しているわけではありません。代わりに、論理プログラミングに対する、より明確な新しい視点を提示しています。Maudeを使用して厳格な型付きインタプリタを作成することで、著者たちは、エラーを早期に発見し、どこで発生したかを正確に特定することが可能であることを示しました。それは、壁が傾いていることを伝えるだけでなく、どのレンガが間違った形をしているかを正確に教えてくれるレーザーレベルを建築家に与えるようなものです。