Inconsistent unification in atomese

noskill commented 4 years ago

I tried to use EqualLink for unification of a variable with a pattern:

(MemberLink 
     (EvaluationLink
            (PredicateNode "has_name")
            (ListLink (ConceptNode "node1") (ConceptNode "name1")))
     (ConceptNode "node2"))

(define (pred1 x x1)
                (display (list x x1)) (newline) 
                (stv 1 0))

For some reason this is ok:

(cog-execute! (QueryLink
    (AndLink 
        (MemberLink 
            (EvaluationLink (VariableNode "X")  (VariableNode "Y"))
            (ConceptNode "node2"))
       (EqualLink (VariableNode "X") (PredicateNode "has_name"))
       (EvaluationLink (GroundedPredicate "scm:pred1") (VariableNode "Y"))) 
   (VariableNode "Y")
))
$1 = (QueueValue
    (ListLink
     (ConceptNode "node1") ; [480756faa9d577d8][1]
     (ConceptNode "name1") ; [e064383668383b3][1]
   ) ; [8057748bbf1ea089][1]
)

But this one causes "C++-EXCEPTION' with args `("cog-execute!" "Infinite Loop detected! Recursed 6 times!"

(cog-execute! (QueryLink  
   (AndLink 
       (MemberLink 
             (EvaluationLink (PredicateNode "has_name") (VariableNode "Y"))
             (ConceptNode "node2"))
        (EqualLink (VariableNode "Y") 
              (ListLink (VariableNode "N") (ConceptNode "name1"))))
    (VariableNode "Y")))

Another inconsistency:

(DefineLink
    (DefinedPredicate "pred1")
    (PredicateFormula
        (Number 1)
        (Times
            (ConfidenceOf (Variable "$X"))
            (ConfidenceOf (Variable "$Y"))))
)

ok

(cog-evaluate! (Evaluation (DefinedPredicate "pred1") (ListLink 
...          (ConceptNode "node1")
...          (ConceptNode "name1"))))
$3 = (stv 1.000000 0.000000)

not ok

(cog-execute! (QueryLink
  (AndLink
     (MemberLink
       (EvaluationLink (VariableNode "X") (VariableNode "Y"))
       (ConceptNode "node2"))
     (EqualLink (VariableNode "X") (PredicateNode "has_name"))
     (Evaluation (DefinedPredicate "pred1") (VariableNode "Y")))
   (VariableNode "Y"))
)
$1 = (QueueValue
)

I think it would be useful to expose unification of subgraphs as a link:

(cog-evaluate! (EqualLink 
   (ListLink (ConceptNode "A") (ConceptNode "B"))
   (ListLink (VariableNode "$X") (VariableNode "$Y"))))
$4 = (stv 0.000000 1.000000)

Here first list link may be unified with the second.

noskill commented 4 years ago

As i understand, unification is currently implemented in URE, we may expose it as UnificationLink which should be a Evaluateable link returning true on successful unification.

noskill commented 4 years ago

Also it shouldn't be difficult to support matching of value types, at least ListValue may be described by the same pattern as ListLink.

linas commented 4 years ago

One quick remark:

To indent scheme properly, indent exactly the same way you would in python. This is not an accident: when python was being invented, it took inspiration from scheme for many design ideas, e.g. lists, comprehensions, etc. but also for indentation! It took the scheme indentation rules and made them mandatory, instead of optional. So - to indent scheme properly, just pretend it was python and it was "significant whitespace".

linas commented 4 years ago

The inf-loop thing is a bug. I'll try to fix it now.

I don't understand the comment about unification. Could you elaborate?

linas commented 4 years ago

In the meanwhile, you can avoid the inf-loop by tightening up the search. Try this

(cog-execute! (Query
   (And
      (TypedVariable (Variable "Y") (Type 'List))
      (TypedVariable (Variable "N") (Type 'Concept))
      (Member
         (Evaluation (Predicate "has_name") (Variable "Y"))
         (Concept "node2"))
      (Equal (Variable "Y")
         (List (Variable "N") (Concept "name1"))))
  (Variable "Y")))

This speeds things up by avoiding potentially goofy groundings for the variables. Due to the bug, one of the goofy groundings included plugging in everything for variable Y and N, including the Member, the And, the Query and the Equal itself, and I think the plugging the Equal back into itself was the inf loop. Some craziness similar to (Equal (Equal (Equal ...)) (List (Variable "N") (Concept "name1")))

linas commented 4 years ago

So, the first part of this bug report is fixed in #2652

There's also a performance side-effect. Instead of writing

(define qsplit
   (Query
      (And
         (Member
            (Evaluation (Predicate "has_name") (Variable "Y"))
            (Concept "node2"))
         (Equal
            (Variable "Y")
            (List (Variable "N") (Concept "name1"))))
      (Variable "Y")))

it would be more efficient to write

(define qonce
   (Query
      (Member
         (Evaluation (Predicate "has_name") 
            (List (Variable "N") (Concept "name1")))
         (Concept "node2"))
      (List (Variable "N") (Concept "name1")))

The reason for this is that qsplit splits into two distinct, disconnnected graphs. One component is

         (Member
            (Evaluation (Predicate "has_name") (Variable "Y"))
            (Concept "node2"))

and the second component is

    (List (Variable "N") (Concept "name1"))

Each component is grounded separately, and then these are pair-wise compared with the EqualLink This is quadratic in run-time, since all possible pairs are compared.

The other way to avoid the quadratic run-time is to use "deep types". That looks like this:

(define qdeep
   (Query
      (And
         (Member
            (Evaluation (Predicate "has_name") (Variable "Y"))
            (Concept "node2"))
         (TypedVariable (Variable "Y")
            (Signature (List (Type 'Concept) (Concept "name1")))))
     (Variable "Y")))

The correct way to read this is that variable Y can be anything, as long as that anything has the shape of (List * (Concept "name1")) and the wild-card has to be of type 'Concept. Note that, in this case, the `is not given a name. Before, you explicitly named itN` but you never used that name, so it was not really needed. The deep type idea allows you to write patterns without having to explicitly name every wild-card location.

linas commented 4 years ago

The query with the PredicateForumla is also a bug.

The short answer: PredicateFormulas are so new, they've never been used with the pattern engine before, and there seem to be three or 4 different bugs, each of which is causing that example to fail.

noskill commented 4 years ago

about unification: ure unifier is described here https://github.com/opencog/ure/tree/master/opencog/unify. I think it's functionality should be exposed in atomese as an evaluateable link, not only through c++. @ngeiswei what do you think?

Well, actually why EqualLink doesn't work like that? Evaluation link has with the same arguments:

(cog-execute! (Query
   (And
      (TypedVariable (Variable "Y") (Type 'List))
      (TypedVariable (Variable "N") (Type 'Concept))
      (Member
         (Evaluation (Predicate "has_name") (Variable "Y"))
         (Concept "node2"))
      (Equal (Variable "Y")
         (List (Variable "N") (Concept "name1"))))
  (Variable "Y")))

and here

(cog-evaluate! (EqualLink 
   (ListLink (ConceptNode "node1") (ConceptNode "name1"))
   (ListLink (VariableNode "N") (ConceptNode "name1"))))

As for value matching i think about something like that:

(cog-execute! (QueryLink  
   (AndLink 
       (MemberLink 
             (EvaluationLink (stv (Variable "Strength") (Variable "Conf")) (PredicateNode "has_name") (VariableNode "Y"))
             (ConceptNode "node2"))
        (EqualLink (VariableNode "Y") 
              (ListLink  (VariableNode "N") (ConceptNode "name1"))))
       (GreaterThanLink 
                     (Variable "Strength")
                     (NumberNode "0.5"))
    (VariableNode "Y")))

noskill commented 4 years ago

By the way, is there a way to perform recursive matching, to let say calculate a height of an atomese tree?

linas commented 4 years ago

why EqualLink doesn't work like that?

Work like what? Please explain. I showed you SignatureLink, it seems that this is what you want.

(cog-evaluate! (EqualLink (ListLink (ConceptNode "node1") (ConceptNode "name1")) (ListLink (VariableNode "N") (ConceptNode "name1"))))

I have no clue at all what you expect to happen here. You'll have to explain.

As for value matching

This already works, and is simpler:

Query
   (And 
      (Member
         (Evaluation (Predicate "has_name") (Variable "Y"))
         (Concept "node2"))
      (TypedVariable (Variable "Y")
         (Signature (List (Type 'Concept) (Concept "name1"))))
      (GreaterThan (StrengthOf (Variable "Y")) (Number 0.5)))
  (Variable "Y"))

linas commented 4 years ago

Closing. Fixed in pull req #2655

@noskill I don't understand what you are trying to get at with the talk of unification -- open a new issue with more detailed explanations...

linas commented 4 years ago

@noskill Oh, maybe I do understand what you mean by "unification": it is described in this enhancement request: issue #554

The example I just added today:

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

Currently, the pattern matcher runs this and evaluates the EqualLink last. It could have done this at pattern compile-time instead, and just plugged in for (Variable "?AGENT") everywhere, and simplified the search. This is a particularly simple "unification", I suppose fancier ones are possible.

ngeiswei commented 4 years ago

@noskill said:

I think [unification] should be exposed in atomese as an evaluateable link, not only through c++. @ngeiswei what do you think?

You're absolutely right. Actually, I think the following branch (a prototype to support meta-rule in the backward chainer [EDIT: that I indent to review and merge as time permits]) contains such a link (or bindings) https://github.com/opencog/ure/tree/rTreutlein-MetaRuleSupport

linas commented 4 years ago

@ngeiswei If you understand what is being asked for, please explain either here or in a new issue or maybe #554 if appropriate (I think #554 wants to do an implicit automatic unification, not an explicit one supported by a new atom type) I do not understand what is being asked for here ...

ngeiswei commented 4 years ago

@linas, I'm not sure I understand what is being asked for, but in @noskill's words

As i understand, unification is currently implemented in URE, we may expose it as UnificationLink which should be a Evaluateable link returning true on successful unification.

I think UnificationLink would be a virtual link that would be true if any two terms containing variables can be syntactically unified (modulo some algebraic transformations such as commutativity), for instance

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

would evaluate to true.

Though in the context of having such virtual link in a query, thus having variables eventually replaced by grounded atoms, I guess it would be equivalent to

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

What the URE unifier can offer though is statically rule out unsatisfyable equalities.

linas commented 4 years ago

OK, so .. it is certainly plausible to have a UnificationLink outside of the pattern engine, that returns true/false. Do you also expect to get a listing of the variable groundings?

ngeiswei commented 4 years ago

Do you also expect to get a listing of the variable groundings?

Not groundings but substitutions, so for instance if we try to unify

(Inheritance X Y)

with

(Inheritance (And Z W) (Concept "A"))

the set of possible substitutions (here only one) would be

X -> (And Z W)
Y -> (Concept "A")

linas commented 4 years ago

OK, so, a new UnificationLink would then have to look something like this:

UnificationLink
   <optional variable declarations>
   clause-1
   ...
   clause-n

where typically, n=2 for the usual case, and the variables, if not specified, are implicitly extracted. I guess all the usual stuff about typed-variables would apply (so in your example, if there was a (TypedVariable (Variable "Y") (Type 'Predicate)) then the unification fails, cause Y would be the wrong type.)

One could then say (cog-execute! (UnificationLink ...)) and get back the list of substitutions. The returned thing could be either a SetLink or a LinkValue (I prefer the latter, these days).

Does the above describe the idea? Did I miss something? Is there something more?

All of your examples show something unusual: the unification never-ever depends on the other contents of the AtomSpace. That is, the unification can be done once and for-all statically, and it will never change. Is that correct?

If so, then we have two choices: perform the unification immediately, when the atom is created, or defer unification until later, when it's asked for, and then cache the result, in case it is ever asked for again.

I'm wondering if we really need a new UnificationLink or if the existing EqualLink should have this gain-of-function and be unleashed on the world.

linas commented 4 years ago

FWIW, what you are calling "unification" is what I am trying do do more generally, with the idea of "connectors" and "sheaves". In your examples, variables can be aligned with other atoms, and as long as they line up, the connection can be made. The result of a single connection is a "linkage" - what you are calling a "substitution".

For the general link-grammar case, you don't have just "variables" and "things that the variables match up to", but rather two end-points, and either the end-points can connect, or they cannot. In your case, a variable can connect to anything, (if the variable has no type constraints)

I'm trying to change the vocabulary from "variables" and "things that plug into variables" to instead be "connectors" and "rules for connecting connectors". The reason for changing the vocabulary is that the language "variables" and "things that plug into variables" has an implicit directionality from->to and I want to have non-directional connections.

The reason for this is partly due to the influence of link-grammar (and more generally, categorial grammars) where the vocabulary of "variables" and "things that plug into variables" is confusing and misleading, whereas "connectors that can plug together" is more accurate. This minor change in vocabulary solves a lot of problems, and avoids a lot of confusion ... A lot of what I see written up in academic papers is rife with this confusion, and thus results in bizarre and unfounded claims. However, de-tangling this concept of "things that can be plugged together" is hard, because .. well, I used to make that mistake too, and the entire pattern engine is founded on that confusion. Undoing that confusion will be a large undertaking.

ngeiswei commented 4 years ago

(so in your example, if there was a (TypedVariable (Variable "Y") (Type 'Predicate)) then the unification fails, cause Y would be the wrong type.)

Exactly.

Does the above describe the idea? Did I miss something? Is there something more?

No, it perfectly describes what the unifier does.

All of your examples show something unusual: the unification never-ever depends on the other contents of the AtomSpace. That is, the unification can be done once and for-all statically, and it will never change. Is that correct?

Yes. It is purely functional, and as such can easily be memoized (though it's not implemented yet).

I'm wondering if we really need a new UnificationLink or if the existing EqualLink should have this gain-of-function and be unleashed on the world.

For regular queries EqualLink should be enough, but for more sophisticated ones, such as queries sticking together queries to produce larger queries, then I think a UnificationLink is necessary. With that I think the URE could actually be implemented in Atomese, it seems.

ngeiswei commented 4 years ago

I'm trying to change the vocabulary from "variables" and "things that plug into variables" to instead be "connectors" and "rules for connecting connectors".

Very interesting!

linas commented 4 years ago

To clarify several more things:

Issue #554 proposes that unification should be done during the static-analysis stage, in the pattern engine, not at run time.
It makes a lot more sense to use the existing EqualLink for this (inside a pattern), instead of inventing a new UnificationLink. I see no benefit for a UnificationLink inside a pattern, I think it just confuses things.
If we have a UnificationLink, then it would need to be useful outside of the pattern matcher. But I still do not understand how users would use it. What good is it, if you do it only need it once, ever? What would you do with it? What purpose does it serve, what problem does it solve? (I can see how its useful inside of URE , as a C++ tool. I can almost see how it would be useful in python or scheme, but am not thrilled by that idea. I don't understand how its useful in Atomese)

The last bullet is the important one...

Just to provide contrast: once could also ask "what good is EqualLink outside of the pattern matcher?" It doesn't "do" anything outside of the pattern-engine. You can use it to declare numeric formulas as a form of KR - knowledge representation, but it doesn't really make sense to evaluate it or execute it. Maybe it could be useful in asmoses in some way.

For PLN, we have SimilarityLink which is a fuzzy equal of some sort. We have EquivalenceLink documented on the wiki, but I guess its not a part of PLN? I copied that wiki page out of some email chain long ago.

ngeiswei commented 4 years ago

It makes a lot more sense to use the existing EqualLink for this (inside a pattern), instead of inventing a new UnificationLink. I see no benefit for a UnificationLink inside a pattern, I think it just confuses things.

Agreed.

If we have a UnificationLink, then it would need to be useful outside of the pattern matcher. But I still do not understand how users would use it.

I don't precisely see either but I vaguely see piping its output to some put link to create new inference trees, etc.

I don't understand how its useful in Atomese

To write specialized chainers.

linas commented 4 years ago

I vaguely see piping its output to some put link

Yes. I'm also vaguely and slowly working through the connectors idea, but for something so "obvious", it's also surprisingly difficult.

@noskill its kind-of on you now, to push on this if you want this to work in some certain way, or to be used for something.

opencog / atomspace

Inconsistent unification in atomese #2650