unification 0.0.1+2 unification: ^0.0.1+2 copied to clipboard
unification using trampolining
unification #
[unification] is a concrete implementation of logical first-order unification and library to apply a first-order unification procedure [unify] given by the library on two terms of [Termtype] given by the library.
A solution of a unification problem is a substitution, that is, a mapping assigning a symbolic value to each variable of the problem's expressions. The unification algorithm reports unsolvability for a given problem or computes a complete, and minimal singleton substitution set containing the so-called most general unifier, that is, a set covering all its solutions, and containing no redundant members.
Example: #
import "package:tailcalls/tailcalls.dart";
import "package:unification/unification.dart";
var test = unify(
new List()
..add(
new Tupl(
new Term("b0", [new Term("b1", []),new Term("b2", [])]),
new Term("b0", [new Term("b1", []),new Term("b2", [])]),
),
),
).result();
var mgu = test;
print(mgu.toString());
Read more about unification in logic on Wikipedia.