問題タブ [unification]

型推論の問題

タイピング環境で

統一問題で転送できますか?

どんな助けでも本当に感謝します!

質問

最も効率的な MGU アルゴリズムは何ですか? その時間複雑度は? スタックオーバーフローの回答で説明するのは簡単ですか?

Google で答えを見つけようとしていますが、ACM サブスクリプションを介してのみアクセスできるプライベート PDF を見つけ続けています。

SICP で 1 つのディスカッションを見つけました: here

「最も一般的な統一アルゴリズム」とは何かについての説明: 「自由変数」と「定数」を含む 2 つの式ツリーを取得します。たとえば、

次に、Most General Unifier アルゴリズムは、2 つの式を同等にする最も一般的なバインドのセットを返します。例えば：

「最も一般的な」とは、代わりに{x ↦ 1}and {z ↦ 1}and をバインドできることを意味しますが、それはe1and とe2同等になりますが、より具体的になります。

SICP の記事は、それがかなり高価であることを暗示しているようです。

情報については、私が尋ねている理由は、型推論にもこの「統一」アルゴリズムが含まれていることを知っており、それを理解したいからです。

I'm trying to get my head around how type inference is implemented. In particularly, I don't quite see where/why the heavy lifting of "unification" comes into play.

I'll give an example in "pseudo C#" to help clarify:

The naive way to do it would be something like this:

Suppose you "parse" your program into an expression tree such that it can be executed with:

So something like "Multiplication" might be implemented with:

Then to "implement" type inference, you could just do something like:

Then "Multiplication"'s type inference might just be something like:

lhs and rhs might be simple constants, or "variables" which are looked up in the environment:

But nowhere in this do we end up with the need for a "unification" algorithm.

So, clearly, my example is not complex enough. Does it need higher order functions? Do we need "parametric polymorphism"?

What is the simplest possible example where "unification" is actually needed to correctly infer the type of an expression.

An example in Scheme would be ideal (i.e. an example of a very small Scheme program where you require unification to correctly infer the type of the s-expression).

ここでSICPで説明されている統合アルゴリズムを理解しようとしています

特に、プロシージャ「extend-if-possible」には、右側の「式」がすでに何かにバインドされている変数であるかどうかをチェックするチェック（アステリックス「*」でマークされた最初の場所）があります。現在のフレーム：

関連する解説は次のように述べています。

「最初のケースでは、照合しようとしている変数がバインドされていないが、照合しようとしている値自体が（異なる）変数である場合、値がバインドされているかどうかを確認する必要があります。もしそうなら、その価値を一致させるために。一致の両方の当事者がバインドされていない場合、私たちはどちらか一方にバインドすることができます。」

しかし、これが実際に必要な場合は考えられません。

それが話しているのは、現在、次のフレームバインディングが存在する可能性がある場所だと思います。

次に、？zから？yへのバインディングを「extendIfPossible」するように求められます。

その「*」チェックが存在する場合、「？z」を「？y」で拡張するように求められると、「？y」はすでに4にバインドされていることがわかり、「？z」を「4」で再帰的に統合しようとします。これにより、フレームを「？z=4」で拡張します。

チェックを外すと、「？z =？y」だけでフレームを拡張することになります。しかし、どちらの場合も、？zがまだ他の何かにバインドされていない限り、問題は発生しません。

？zがすでに他の何かにバインドされている場合、コードは「*」とマークされた部分に到達しないことに注意してください（？zがすでに一致していたものと統合するためにすでに再帰しているはずです）。

よく考えてみると、「最も単純な」MGU（Most General Unifier）を生成するための何らかの議論があるかもしれないことに気づきました。たとえば、他の変数を参照する変数の数が最小のMGUが必要な場合があります...つまり、置換{？x =？y、 ？y = 4} ...しかし、このアルゴリズムがこの動作を保証するとは思わない。「（？x 4）」を「（？y？y）」と統合するように要求した場合は、それでも{？x =？y、？y=4}になります。そして、動作が保証できない場合、なぜ追加の複雑さがあるのでしょうか。

ここでの私の推論はすべて正しいですか？そうでない場合、正しいMGUを生成するために「*」チェックが必要な反例は何ですか？

入手した AI の教科書に取り組んでいると、セクションの最後の宿題の問題にたどり着きました。

「69 ページで概説されている統合アルゴリズムを任意の言語で実装します。」

69 ページには、統一アルゴリズムの次の擬似コードがあります。

これで、統合の一般的な概念は理解できましたが、Java や C# などの言語でこれをどのように実装し始めるかはまったくわかりません。

メソッドの署名がどのように見えるかさえわかりません。どのタイプの変数が必要ですか? 述語計算構造を表すためにリストを返す必要があることは確かですが、それは推測です。

たとえば、「E1 は変数です」と書かれている場合、それを Unify メソッドに渡すとしたら、それ以外の何かである可能性はありません。null をチェックすることはできますが、それは「空のリスト」とは異なりますか?

Unificaiton アルゴリズムを C# または Java で実装するために、誰かが私を助けたり、正しい方向に向けたりすることはできますか?

なぜこれが機能するのですか：

そして、これはスタックオーバーフローの例外を与えますか?

Prolog で統一アルゴリズムがどのように機能するかを理解するために、過去 5 日間を費やしました。今、私はJavaでそのようなアルゴリズムを実装したい..

おそらく最善の方法は、文字列を操作し、スタックなどのデータ構造を使用してその部分を分解することだと思いました..

明確にするために：

ユーザー入力が a(X,c(d,X)) = a(2,c(d,Y)) であるとします。

私はすでにそれを 1 つの文字列として取り、2 つの文字列 ( Expression1 と 2 ) に分割しています。さて、次の文字が変数か定数かなどかどうかをどうやって知ることができますか..ネストされたifでそれを行うことができますが、それは良い解決策ではないようです..継承を使用しようとしましたが、まだ問題があります(どのように読み取られている文字のタイプを知ることはできますか?)

なぜこれは失敗しL is [1,2,3,4]、これはうまくいくのですL = [1,2,3]か？

しかしL is 1、L = 1両方とも同じように機能します。

X、Y を (1,2)、(1,-2)、(-1,2)、(-1,-2)、(2,1)、(2,-1) で統一するエレガントな方法は何ですか? , (-2,1), (-2,-1)?

このようにすると、エラーが発生しやすく、退屈に思えます。

そして、この方法は高すぎるようです：

統一の（実用的な）アプリケーションは何ですか？実世界のどこで実際に使われているのでしょうか？

それが実際に何であるか、そしてなぜそれが人工知能の一部と見なされるのかについての全体的な考えを理解することができませんでした。