F #에서 통합 알고리즘을 찾는

Question

ASTS를 변화시키고 간단한 패턴 매칭 이상을 필요로하므로 통합 알고리즘이 필요합니다.

이는 .NET 프로젝트를위한 것이지만, 제가 .NET PROLOG 구현과 단지 상호 운용 할 수 있음을 알고 있으며, 통합 알고리즘 만 삽입하면됩니다.그래서 프롤로그는 과도한 것입니다.

Martelli, Montani : Montaniari : 효율적인 통일 알고리즘 "은 완벽하게 작성되었지만 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).