jetbrains.mps.unification
Class Unification

java.lang.Object
  extended by jetbrains.mps.unification.Unification

public class Unification
extends java.lang.Object

This is an implementation of the "near linear" algorithm for solving syntactic unification as described in the paper linked below.1 No recursive terms are allowed, meaning the "occurrs check" is performed on the input. If successful, the returned Substitution contains the variable bindings.

The variables are sorted using Comparable to ensure uniqueness of bindings whereas the substituted term is also a variable.

1. Baader, Franz, and Wayne Snyder. "Unification Theory." Handbook of automated reasoning 1 (2001): 445-532.

Constructor Summary
Unification()
           
 
Method Summary
static Substitution unify(Node a, Node b)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

Unification

public Unification()
Method Detail

unify

public static Substitution unify(Node a,
                                 Node b)