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

Question

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

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

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

Answer 1

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

因此，我将分享一些关于一般方法的提示，但它不是一个完整的解决方案。 首先，您需要以某种方式表示您的 AST。在 F# 中，您可以使用有区别的联合来做到这一点。以下支持变量、值和函数应用:

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

Unification 是一个函数，它将表达式列表统一为 (Expr * Expr) list 类型，并返回对变量的赋值(将表达式 Expr 赋值给变量名称字符串):

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 统一意味着您需要检查函数名称是否相同(否则失败)，然后将所有参数表达式作为新约束添加到 剩余列表...