F＃の統一アルゴリズムを探す

Question

私はASTSを変換し、単純なパターンマッチング以上のものを必要としているため、統一アルゴリズム。

これは.NETプロジェクトのためのものであり、私は.NET Prologの実装と相互運用できることを知っています。統合アルゴリズムを埋め込むだけです。だからPrologはオーバーキルです。

"Martelli、Montanari：効率的な統一アルゴリズム"を手に入れることができれば完璧だろうと私はそれがHaskellを含むどんな機能的な言語に解決し、f＃。

Answer 1

In general, it is a good practice to share your attempts when asking questions on SO. People will not generally give you a complete solution for your problems - just answers when you have specific question or hints how to approach the problem.

So, I'll share some hints about the general approach, but it is not a complete solution. First you need to represent your AST in some way. In F#, you can do that using discriminated unions. The following supports variables, values and function applications:

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

Unification is a function that takes list of expressions to be unified of type (Expr * Expr) list and returns assignments to variables (assigning an expression Expr to a variable name string):

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..."

There are a few cases that you'll need to add. Most importantly, unifying Function with Function means that you need to check that the function names are the same (otherwise fail) and then add all argument expressions as new constraints to the remaining list...

Answer 2

The final syntactic unification in Baader & Snyder uses union-find to partition the nodes of the two structures into equivalence classes. It then walks those classes building up the triangular substitution.

Since it uses union-find, if you're looking for a purely functional answer you're out of luck; no-one knows how to write a functional union-find. However, we know how to write a persistent union-find which is at least apparently functional, thanks to Conchon and Filliâtre (written in OCaml).