f# - 在 F# 中寻求统一算法

Question

我正在转换 AST，需要的不仅仅是简单的模式匹配，因此需要统一算法。

虽然这是针对 .NET 项目的，而且我知道我可以与 .NET PROLOG 实现互操作，但我只需要嵌入统一算法；所以PROLOG是矫枉过正的。

如果我能得到用 F# 编写的“Martelli, Montanari: An Efficient Unification Algorithm”，那将是完美的，但我会接受任何功能语言，包括 HASKELL 并翻译成 F#。

Answer 1

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

Answer 2

一般来说，在提出关于 SO 的问题时分享您的尝试是一种很好的做法。人们通常不会为您的问题提供完整的解决方案 - 只是在您有特定问题或提示如何解决问题时回答。

所以，我将分享一些关于一般方法的提示，但这不是一个完整的解决方案。首先，您需要以某种方式表示您的 AST。在 F# 中，您可以使用可区分联合来执行此操作。以下支持变量、值和函数应用程序：

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

统一是一个函数，它将表达式列表的类型统一(Expr * Expr) list并返回对变量的赋值（将表达式分配给Expr变量 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..."

您需要添加一些案例。Function最重要的是，统一Function意味着您需要检查函数名称是否相同（否则失败），然后将所有参数表达式作为新约束添加到remaining列表中......