unify 0.2.2
Unify #
An implementation of Ruzicka und Privara's algorithm of logical unification for dart and flutter.
This algorithm is an optimization of Corbin and Bidoit's algorithm, which itself is based on Robinson's well known algorithm available as 'package:unification'.
Robinson's algorithm is inefficient if the same subterm is given in several locations of a term, leading to unnecessarily repeated calculations. Ruzicka und Privara's algorithm takes the structure of the term into account by using a directed acyclic graph [DAG] instead of the original term tree to avoid such unnecessarily repeated calculations. Ideally, in this reduced DAG all equal subterms are represented by one identical subgraph, i.e. one and the same term object.
The current implementation is an approximation of Ruzicka und Privara's algorithm. The original version is given in directory src2 and can be
imported by as dart import 'package:unify/unify2.dart'
;
Getting started #
Add the dependency to your pubspec.yaml file:
dependencies:
unify: #latest version
Add the import statement to your source files:
import 'package:unify/unify.dart';
Or, give it a try and run the example:
dart ./example/main.dart
Modify the example to test more complex tasks!
Examples: #
import 'package:unify/unify.dart';
// set up the unification procedure
void unify(t1, t2) {
var b = Bindings.empty();
print('');
print('Term 1 $t1.');
print('Term 2 $t2.');
mgu(t1, t2, b); // side effect on b
print(b);
var o1 = t1.occurs(b);
print('Occurs check for term 1 ${o1}');
var o2 = t2.occurs(b);
print('Occurs check for term 2 ${o2}.');
if (!o1 && !o2) {
var u1 = t1.substitute(b);
print('Unified term 1 ${u1}');
var u2 = t2.substitute(b);
print('Unified term 2 ${u2}');
}
}
// run some examples
void main() {
// Always use different numbers for differents clauses!
//1.
var t1 = t(1, 1, [v(1, 2), v(1, 2)]);
var t2 = t(2, 1, [
t(2, 2, [v(2, 3)]),
v(2, 3) // no circularity v(2, 4)
]);
unify(t1, t2);
//2.
var t3 = v(1, 2);
var t4 = v(2, 1);
unify(t3, t4);
//3.
var t5 = t(1, 1, [
v(1, 2),
v(1, 2),
v(1, 3),
t(1, 4, [
t(1, 5, [v(1, 3)])
]),
v(1, 3),
]);
var t6 = t(2, 1, [
t(2, 2, [v(2, 3)]),
v(2, 4),
v(2, 3),
v(2, 5),
v(2, 4),
]);
unify(t5, t6);
//4.
var t7 = t(1, 1, [
v(1, 2),
v(1, 2),
]);
var t8 = t(2, 1, [
v(2, 2),
t(2, 3, [
v(2, 4), // circularity: v(2, 2)
]),
]);
unify(t7, t8);
//5.
var t9 = t(3, 1, [
v(3, 3),
v(3, 2),
v(3, 2),
v(3, 3),
v(3, 4),
v(3, 4),
]);
var t10 = t(4, 1, [
v(4, 6),
v(4, 2),
t(4, 3, [
v(4, 4),
]),
v(4, 5),
v(4, 2),
v(4, 6),
]);
unify(t9, t10);
}
Changelog #
0.2.2 #
 improve README
0.2.1 #
 use dynamic instead of null aware operators because pana isn't able to deal with nnbd
0.2.0 #
 new implementation
0.1.6 #
 remove prints
0.1.5 #
 Improve docs and README
0.1.4 #
 Improve example and README
0.1.3 #
 Improve example and README
0.1.1 #
 Remove unused variables
0.1.0 #
 Publish initial release
import 'package:unify/unify.dart';
void main() {
var t1 = t(1, 1, [v(1, 2), v(1, 2)]);
var t2 = t(2, 1, [
t(2, 2, [v(2, 3)]),
v(2, 4) // circularity v(2, 3)
]);
var t3 = v(1, 2);
var t4 = v(2, 1);
var t5 = t(1, 1, [
v(1, 2),
v(1, 2),
v(1, 3),
t(1, 4, [
t(1, 5, [v(1, 3)])
]),
v(1, 3),
]);
var t6 = t(2, 1, [
t(2, 2, [v(2, 3)]),
v(2, 4),
v(2, 3),
v(2, 5),
v(2, 4),
]);
// Clause 1
var t7 = t(1, 1, [
v(1, 2),
v(1, 2),
]);
// Clause 2
var t8 = t(2, 1, [
v(2, 2),
t(2, 3, [
v(2, 4), // circularity: v(2, 2)
]),
]);
// Always use different numbers for differents clauses!
// Clause 3
var t9 = t(3, 1, [
v(3, 3),
v(3, 2),
v(3, 2),
v(3, 3),
v(3, 4),
v(3, 4),
]);
// Clause 4
var t10 = t(4, 1, [
v(4, 6),
v(4, 2),
t(4, 3, [
v(4, 4),
]),
v(4, 5),
v(4, 2),
v(4, 6),
]);
unify(t1, t2);
unify(t3, t4);
unify(t5, t6);
unify(t7, t8);
unify(t9, t10);
}
void unify(t1, t2) {
var b = Bindings.empty();
print('');
print('Term 1 $t1.');
print('Term 2 $t2.');
mgu(t1, t2, b); // side effect on b
print(b);
var o1 = t1.occurs(b);
print('Occurs check for term 1 ${o1}');
var o2 = t2.occurs(b);
print('Occurs check for term 2 ${o2}.');
if (!o1 && !o2) {
var u1 = t1.substitute(b);
print('Unified term 1 ${u1}');
var u2 = t2.substitute(b);
print('Unified term 2 ${u2}');
}
}
Use this package as a library
1. Depend on it
Add this to your package's pubspec.yaml file:
dependencies:
unify: ^0.2.2
2. Install it
You can install packages from the command line:
with pub:
$ pub get
with Flutter:
$ flutter pub get
Alternatively, your editor might support pub get
or flutter pub get
.
Check the docs for your editor to learn more.
3. Import it
Now in your Dart code, you can use:
import 'package:unify/unify.dart';
Popularity:
Describes how popular the package is relative to other packages.
[more]

9

Health:
Code health derived from static analysis.
[more]

100

Maintenance:
Reflects how tidy and uptodate the package is.
[more]

100

Overall:
Weighted score of the above.
[more]

54

We analyzed this package on Feb 12, 2020, and provided a score, details, and suggestions below. Analysis was completed with status completed using:
 Dart: 2.7.1
 pana: 0.13.5
Dependencies
Package  Constraint  Resolved  Available 

Direct dependencies  
Dart SDK  >=2.7.0 <3.0.0  
unification  ^0.1.0  0.1.15  
Transitive dependencies  
tailcalls  0.1.3  
Dev dependencies  
pedantic  ^1.0.0 