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

example/main.dart

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 up-to-date the package is. [more]
100
Overall:
Weighted score of the above. [more]
54
Learn more about scoring.

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