À la recherche d'un algorithme d'unification dans F #

Question

Je transforme des asts et j'ai besoin de plus que de simples motifs correspondant, donc l'algorithme d'unification.

Bien que cela soit pour un projet .NET et que je sache que je pourrais simplement interopérer avec une implémentation de PRAGolog .NET, je n'ai besoin que d'intégrer l'algorithme d'unification;Donc, Prolog est surcharge.

Si je pouvais obtenir "Martelli, Montanari: un algorithme d'unification efficace" écrit en F # qui serait parfait, mais je vais me contenter de tout langage fonctionnel, y compris HASKELL et traduire à 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).