Fでの統一アルゴリズムを求める＃

Question

私はASTを変換しており、単純なパターンマッチング以上の統一アルゴリズムを必要としています。

これは.NETプロジェクト向けですが、私は.NET PROLOG実装との相互運用が可能であることを知っていますが、統合アルゴリズムを組み込む必要があります。だからPROLOGは過剰です。

私が「Martelli、Montanari：効率的な統一アルゴリズム」をF＃で書いてあれば完全ですが、私はHASKELLを含む任意の機能言語を解決し、F＃に変換します。

Answer 1

一般的に、あなたはSOに関する質問をするときにあなたの試行を共有することをお勧めします。人々は一般的にあなたにあなたの問題の完全な解決策を与えることはありません - あなたが特定の質問を持っているとき、または問題に近づく方法を示唆した時に答えます。

一般的なアプローチについてのヒントをいくつかお伝えしますが、は完全な解決策ではありません。です。 まず、何らかの方法でASTを表現する必要があります。 F＃では、区別された共用体を使用してこれを行うことができます。以下は、変数、値、および機能アプリケーションをサポート：

：

type Expr = 
    | Function of string * Expr list 
    | Variable of string 
    | Value of int 

統一型(Expr * Expr) list統一される式のリストを取得し、変数（変数名stringに発現Exprを割り当てる）に割り当てを返す関数です。

let rec unify exprs = 
    match exprs with 
    // Unify two variables - if they are equal, we continue unifying 
    // the rest of the constraints, otherwise the algorithm fails 
    | (Variable s1, Variable s2)::remaining -> 
     if s1 = s2 then unify remaining 
     else failwith "cannot unify variables" 
    // Unify variable with some other expression - unify the remaining 
    // constraints and add new assignment to the result 
    | (Variable s, expr)::remaining 
    | (expr, Variable s)::remaining -> 
     let rest = unify remaining 
     // (s, expr) is a tuple meaning that we assign 'expr' to variable 's' 
     (s, expr)::rest 

    // TODO: Handle remaining cases here! 
    | _ -> failwith "cannot unify..." 

追加する必要があるケースがいくつかあります。最も重要なのは、FunctionでFunctionを統一することで、関数名が同じである（そうでない場合は失敗）、その後remainingリストに新しい制約条件として、すべての引数式を追加することを確認する必要があることを意味します...

Answer 2

バーダーの最後の構文統一& Snyderは、union-findを使用して、2つの構造のノードを等価クラスに分割します。次に、それらのクラスを歩き、三角形置換を構築します。

純粋に機能的な答えを探しているのなら、union-findを使用しているので運が悪いです。機能的な共用体を見つける方法を知っている人は誰もいません。しかし、われわれは永続的なユニオン検索を書く方法を知っています。これはConchon and Filliâtre（OCamlで書かれています）のおかげで、少なくともであり、明らかにです。