問題タブ [unification]

Franz Baader と Tobias Nipkow による"Term Rewriting and All That" ( WoldCat ) を使用して、 AST変換で使用する F#の統合アルゴリズムを作成しています。セクション 4.6 変換による統一については、例を使った数学理論が多すぎて、私が望んでいたほど明確ではありませんでした。

誰かが変換を利用するより簡単な例を挙げたり指摘したりできますか:

削除、分解、方向付け、消去。

MarkJonesとOlegKiselyovのチュートリアルに従って、Hindley-Milner型推論アルゴリズムを実装しています。これらは両方とも、おおよその形式のタイプで「バインディングの適用」操作を行います

これは、指定されたにtyvar -> tyバインディングを適用します。を呼び出すのを忘れることは私のコードでよくある間違いであることがわかりました。また、と同じ型を持っているため、Haskellの型システムから助けを得ることができません。型システムで次の不変条件を適用する方法を探しています。TyEnvTypeapplyBindingstyapplyBindings tyenv ty

型推論を行う場合、「最終的な」結果を返す前にバインディングを適用する必要があります

単形オブジェクト言語の型推論を行う場合、wren ng thorntonのunification-fdパッケージに実装されているように、これを強制する自然な方法があります。sの2つのデータ型を定義しますType。

applyBindingsタイプを与える

（この関数は実際freeze . applyBindingsにはunification-fdにあります）。これにより、不変条件が適用されます。忘れるとapplyBindings、型エラーが発生します。

これは私が探している種類の解決策ですが、ポリモーフィズムを持つオブジェクト言語の場合です。上記のアプローチは、現状では適用されません。オブジェクト言語の型には型変数がある可能性があるためです。実際、バインディングを適用した後に変数が解放された場合、戻りたくないのですNothingが、一般化したいと思います。これらの変数。

私が説明する線に沿った解決策、つまりとはapplyBindings異なるタイプを与える解決策はありconst idますか？実際のコンパイラーは、MarkとOlegのチュートリアルが使用するのと同じしゃれ（統合変数とオブジェクト言語型変数の間）を使用しますか？

このページの下部にある演習を進めようとしていますが、3番で完全に混乱しています。

旅行情報に関する次の知識ベースが提供されます。

2つの都市間を移動できるかどうかを確認するのは簡単です。私はこれをしました：

しかし、実際にパスを変数と統合する必要がある場合、私は完全に混乱します！

私はこれを書いた：

そして呼ばれるtravel(valmont, losAngeles,X).

トレース中に、最後の匿名変数を除いて、正しいパスが表示されるポイントがあります。

travel(valmont, metz, connected(metz, paris, connected(paris, losAngeles, _17)))

しかし、これを変数と統合する方法は実際にはわかりませんX。

私は本当にこれに頭を悩ませることはできません。誰かが私を正しい方向に押し進めるためのヒントを教えてもらえますか？私が行方不明になっている終了条件か何かがありますか？

編集：

今私が持っています：

しかし、それはこのように立ち往生します：

私はそれで遊んだことがありますが、全体を構築するためにそれを取得することはできませんgo(a,b,go(b,c))...

私がやりたいことは、特定の式が Oz で別の式と統合されるかどうかをテストすることです。

たとえば、次のようなことをしたい:

それは、統合できるtrueときに返すことができ、それ以外の場合はfalse です。AB

これを使用して特定のパターン マッチングを行いたい (つまり、特定のパターンでリストをフィルター処理する)。

回答ありがとうございます。

Hindley-Milner型推論アルゴリズムの一般化にある「ボトムアップ」型推論アルゴリズムを実装しようとしています。

6ページでは、暗黙の制約がどのようになっているのかを説明しています

t1t2単形型変数のセットに関して型を一般化することによって得られる型スキームのインスタンスである必要がありますM

ただし、9ページで、暗黙の制約に置換を適用する方法の説明中に、この単相型変数のセットに置換を適用するように指示されました。問題は、私が置換を持っている場合、[t1 := t2 -> t3]それMはもはや型変数のセットではないということです。

私はここで何を誤解していますか？

プロローグでリストの特定のメンバーにアクセスする方法を教えてもらえますか? たとえば、ルールに渡されたリストの 3 番目または 4 番目の要素にアクセスする必要があるとします。

次の状況を処理するには、統合アルゴリズムが必要です。

式ツリーの各ノードには、子のリスト (連想) またはセット (連想および可換) があります。特定のパターンに可能なすべての一致を取得したいと思います。

ここに例があります。+ が可換で * が可換でない行列を扱っていると仮定しましょう。

表現：A + B*C*D + E

または:Add(A, Mul(B, C, D), E)

パターン：X + Y*Z

2試合見た

質問: これを処理する標準アルゴリズムはありますか?

重複の可能性:
Prolog- 英語から C への翻訳

基本的に、[add,3,to,5] などの英語の表記を表すリストが与えられる割り当てがあり、それを取得して、対応する C の表記を出力させる必要があります。

そして、これらの数には限りがあります。このような 2 つのリストを組み合わせて、より長いリストを作成することもできます

しかし、これらの長いリストは常に短いリストで構成されており、その数は一定です。それが私が立ち往生しているところです。パターン マッチングを使用できるようにしたいのですが、prolog で構文がどのようになるか完全にはわかりません

したがって、足し算、引き算、掛け算などの場合があります。基本的には、「I を J に追加する」というフレーズをリストから検索し、そのフレーズを (I + J) で統一したいと考えています。または、リストから「I を J で割った余りを取る」を検索し、(I '%' J) で統一します。しかし、すべてのフレーズはさまざまな長さであり、自分が何をしたいのか、どのようにそれを行うのかを知っていても、プロローグでそれを理解できないようです.

少し更新しましたが、ファイル内のすべての基本ルールのリストを現在持っていることを忘れていました。

などなど。問題は結合されたリストです。たとえば、リストは [add,I,to,J,',',then,subtract,H] で、I+JH でなければなりません。個々の基本ルール (I+J および XH) は定義されていますが、長いリストの各部分を一致させる必要があります。

Haskell では、次のようSubst aに単一のコンストラクターで多相データ型を定義しS :: [(String, a)] -> Subst aました。

get::String -> Subst a -> Maybe a変数名と置換を取り、その変数を置換する必要がある値を返す関数を定義したいと考えています。変数で置換が定義されていない場合、関数は Nothing を返す必要があります。

私は次のことを試しました：

しかし、私はエラーが発生しています。理由はありますか？

Haskell 関数を次のように記述しました。

そのようなデータ型でdata Subst a = S [(String,a)]

substassubst :: Subst a -> a -> aとvarsasを宣言しましたvars :: a -> [String]。これを実行すると、型エラーが発生します。理由はありますか？