البحث عن خوارزمية التوحيد في F #

Question

أنا تحويل asts وتحتاج إلى أكثر من مطابقة نمط بسيط، وبالتالي خوارزمية التوحيد.

بينما هذا مخصص لمشروع .NET وأنا أعلم أنني قد أتوقع فقط مع تطبيق .NET Prolog، إلا أنني بحاجة فقط إلى تضمين خوارزمية التوحيد؛لذلك prolog هي مبالغة.

إذا استطعت الحصول على "Martelli، Montanari: خوارزمية توحيد فعالة" مكتوبة في F # من شأنها أن تكون مثالية، لكنني سأستطيع على أي لغة وظيفية بما في ذلك 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).