F #

Question

에서 통일 알고리즘을 찾고 있습니다. 나는 AST를 변형하고 있으며 단순한 패턴 매칭 이상의 통일 알고리즘이 필요합니다.

.NET 프로젝트 용이지만 .NET PROLOG 구현과 상호 운용 할 수 있다는 것을 알고 있지만 통일 알고리즘 만 포함하면됩니다. 그래서 PROLOG는 잔인합니다.

F #으로 작성된 "Martelli, Montanari : 효율적인 통합 알고리즘"을 사용하면 완벽 할 수 있지만 HASKELL을 (를) 포함한 모든 기능 언어를 해결하고 F #으로 변환합니다.

Answer 1

일반적으로 SO에 대해 질문 할 때 시도를 공유하는 것이 좋습니다. 사람들은 일반적으로 문제에 대한 완벽한 해결책을 제공하지 않습니다. 특정 질문이 있거나 문제에 접근하는 방법을 알았을 때 대답합니다.

일반적인 접근법에 대한 몇 가지 힌트를 공유 하겠지만 은 완전한 해결책이 아닙니다입니다. 먼저 AST를 어떤 식 으로든 표현해야합니다. F #에서는 차별화 된 노동 조합을 사용하여이를 수행 할 수 있습니다.

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

통일 (변수 명 string로 표현 Expr 할당) 타입 (Expr * Expr) list 통일적 할 표현의리스트를 취하고 변수 할당을 반환하는 함수이다

:

다음은 변수 값 함수 애플리케이션을 지원

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 목록에 새 제약 모든 인수 식을 추가 한 후 (그렇지 않으면 실패) 함수 이름이 동일한 지 확인해야한다는 것을 의미

Answer 2

바더의 마지막 구문 통일 & Snyder는 union-find를 사용하여 두 구조의 노드를 등가 클래스로 분할합니다. 그런 다음 삼각형 대체를 만드는 클래스를 따라갑니다.

순수한 기능적 대답을 찾으려면 union-find를 사용하므로 운이 없다. 아무도 기능적 노조 찾기를 작성하는 방법을 알지 못합니다. 그러나, 우리는 지속적으로 유니온 찾기를 작성하는 법을 알고 있는데, Conchon and Filliâtre (OCaml로 작성) 덕분에 적어도 이 분명히입니다.