Equality at pattern compile time (static-analysis unification)

[linas]

Consider the following:

(use-modules (opencog) (opencog query) (opencog exec))
(Inheritance (Concept "foo") (Concept "baz"))
(Inheritance (Concept "bar") (Concept "baz"))

(define b
   (BindLink
      (And
         (Inheritance (Concept "foo") (Variable "$x"))
         (Equal (Variable "$x") (Variable "$y"))
      )
      (Variable "$y")))

ERROR: Throw to key `C++-EXCEPTION' with args `("cog-new-link" "Variable
not groundable: (VariableNode \"$y\") ; [782][1]\n\n
(/src/atomspace-git/opencog/atoms/pattern/PatternLink.cc:776)")'.

Obviously, we should be able to deduce, whatever x is, that is what y should be, so the above should execute fine, and do what we think it should, instead of throwing.

[linas]

Another example:

(Get
   (And
      (Equal (Variable "?AGENT") (Concept "Andrew"))
      (Evaluation
         (Predicate "leaving")
         (List (Variable "?AGENT") (Variable "?LOCATION")))
     (Inheritance
         (Variable "?LOCATION") (Concept "movie-theatre"))))

The above can be reduced at pattern-compile-time, by plugging in (Concept "Andrew") for (Variable "?AGENT") throughout the entire pattern. Thus, the complexity of the search can be reduced.

This can be generally performed whenever the EqualLink has a "straight-forward" structure, e.g. with one side being a single variable.

More generally, if the EqualLink has a more complex structure, then "unification" can be done, at the time that the pattern is compiled, instead of at the time that the pattern is run.

[linas]

Another example, from @ngeiswei in #2650 (comment)

(EqualLink
  (Inheritance (Concept "A") (Variable "$Y"))
  (Inheritance (Variable "$X") (Concept "B"))

can be statically analyzed before the search is even started. The URE has a unifier that does this.

[ngeiswei]

I suppose the unifier could be moved to its own repository, if it is to be used more broadly than by just the URE.

[linas]

So far, the atomspace has no dependencies other than cogutils.

Although it could be a stand-alone repo, it would need work to be usable for this issue. For example, Unify.h has BindLinktr which makes no sense in the current context. There are substitute methods in there ... which must be only the 4th or 5th or 6th sixth substitute-stuff code that we have laying around. Sadly, the kind of substitution that would be needed for this issue is likely to be different, again, from all the others....

Right now, its just two files, about 2KLocs of code .. do you expect that it might grow?

[ngeiswei]

Right now, its just two files, about 2KLocs of code .. do you expect that it might grow?

Not much, it's pretty mature at that point. There are limitations with with types (for instance deep types are not supported), but this can or should be done outside of the unifier.

However, I'm frankly uncomfortable having that code go to the atomspace repo, due to the opencog/atomspace vs singnet/atomspace divergence. Keeping my main work away from the atomspace repo allows me to minimize the pain resulting from the opencog vs singnet situation. Ideally I would only develop on one side but for reasons outside of my control that's not possible.

[ngeiswei]

I do agree however that from a design standpoint, having the unifer inside the atomspace repo is sensible, and it should be examined, independently of my personal comfort.

[linas]

the opencog/atomspace vs singnet/atomspace divergence

I very strongly and very sharply encourage this divergence to be fixed. If you have any pull or sway with Ben or the other developers, please, please, please encourage them to set things right again! I've tried to convince @vsbogd to do this, but he is unwilling, because it's a fair amount of work. Someone of authority would need to apply pressure to make this happen. If you can bend the ear of those people .. that would be great.

[noskill]

@linas have you changed your mind on merging ptrvalue and grounded object node from singnet? We use them for integration with pytorch as it was proposed here #1970. So far it's the only difference, but i expect divergence between branches will grow.