В поисках алгоритма унификации в F # - PullRequest
Новая
       27

В поисках алгоритма унификации в F #

2 голосов
/ 02 марта 2012

Я преобразую AST и мне нужно больше, чем простое сопоставление с образцом, поэтому алгоритм объединения.

Хотя это для проекта .NET, и я знаю, что могу просто взаимодействовать с реализацией .NET PROLOG, мне нужно только внедрить алгоритм объединения; так что ПРОЛОГ - это излишество.

Если бы я мог написать «Мартелли, Монтанари: эффективный алгоритм объединения», написанный на F #, это было бы идеально, но я остановлюсь на этом на любом функциональном языке, включая HASKELL, и переведу на F #.

Ответы [ 2 ]

2 голосов
/ 02 марта 2012

Окончательное синтаксическое объединение в Baader & Snyder использует union-find для разделения узлов двух структур на классы эквивалентности.Затем он обходит эти классы, выстраивая треугольную подстановку.

Так как он использует union-find, если вы ищете чисто функциональный ответ, вам не повезло;никто не знает, как написать функциональное объединение-найти.Тем не менее, мы знаем, как написать постоянный поиск объединения, который по крайней мере , по-видимому, функционален, благодаря Conchon и Filliâtre (написано на OCaml).

2 голосов
/ 02 марта 2012

В общем, хорошей практикой является делиться своими попытками задавать вопросы по SO. Люди обычно не дадут вам полного решения ваших проблем - просто ответят, когда у вас есть конкретный вопрос, или намеки, как подойти к проблеме.

Итак, я поделюсь некоторыми советами об общем подходе, но это не полное решение . Во-первых, вы должны каким-то образом представлять свой АСТ. В F # вы можете сделать это, используя дискриминационные союзы. Поддерживаются следующие переменные, значения и приложения функций: 

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

Unification - это функция, которая принимает список выражений для объединения типа (Expr * Expr) list и возвращает присваивания переменным (присваивание выражения Expr имени переменной 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 ...

...