Non monotonic behavior of the pattern matcher with present clauses

[ngeiswei]

Problem description

I have a query, containing only present clauses, that correctly succeeds. However the presence of an another atom in the atomspace makes it fails.

How to reproduce

Run the following scheme code:

(use-modules (opencog))
(use-modules (opencog exec))

;; Query
(define query
  (let* (
     ;; Constants
     (R (Predicate "R"))
     (A (Execution (Schema "A")))
     ;; Variables
     (P (Variable "$P"))
     (Q (Variable "$Q"))
     ;; Clauses
     (P↝Q (Quote
            (Implication
              (Unquote P)
              (Unquote Q))))
     (Q∧A (And Q A))
     (Q∧A↝R (Implication
              Q∧A
              R)))
    ;; Query
    (Get
      (VariableSet P Q)
      (Present P↝Q Q∧A↝R))))

;; KB

;; Culprit
(Implication
  (And
    (Predicate "Qbis") ; Culprit
    (Execution (Schema "A"))
  )
  (Predicate "R"))

;; Premises
(Implication
  (Predicate "P")
  (Predicate "Q"))
(Implication
  (And
    (Predicate "Q")
    (Execution (Schema "A"))
  )
  (Predicate "R"))

;; PM
(define results (cog-execute! query))

It, incorrectly, returns nothing.

Remove the culprit atom and then it works.

[ngeiswei]

@linas, I'm working on it. However, if you have some idea at the top of your head as to why it fails, that's welcome.

[ngeiswei]

When I uncomment the following lines

atomspace/opencog/query/PatternMatchEngine.cc

Lines 2608 to 2611 in 7385233

	// Do we have a negative cache? If so, it will always fail.
	const auto& nac = _nack_cache.find(key);
	if (nac != _nack_cache.end())
	return false;

it no longer fails.

[ngeiswei]

@linas, since I have a workaround (disabling that negative cache check) and more urgent work to do I'm gonna leave that bug for now and will come back to it after a few days or weeks, unless you fix it by then.

[linas]

Caches (on any kind of system) are notoriously hard to make work right. These caches made a huge difference on the bio-agi search patterns (major speedup on multi-minute searches).

I'll look. I've got something else I should be doing, but this kind of bug is very irritating.

[linas]

BTW, Some off-topic comments but I know you will read them if I post them here.

• That's an awesome-looking mini-DSL (domain-specific language) in the unit test. I (strongly) encourage developing it further. From what I can tell, one of the main stumbling blocks to the wider use of the URE is the lack of any easy-to-grok API for the rules.

• FYI. I created a simple shim for storing arbitrary s-expressions in the atomspace (with each element becoming an Atom.) What I don't have is a cut DSL for specifying searches. I was panning on doing JSON expressions too, (its easy), but didn't see the point of it. It should be "kind-of easy" to port GraphQL to sit on top of the pattern engine, but this is boring, so I didn't do it.

• Backward-chaining (forward-chainging??). The recent fixes to OrLink should enable single-query chaining in the pattern engine. I think. Not sure. The idea is this. Write a bunch or rules as

(Define (DefinedSchema "foo-induction-axiom")
    (Lambda (Variable "P")(Variable "Q"))( stuff))

and then a recursive rule

(Define (DefinedSchema "recurse")
    (Lambda (Variable "R")(Variable "S"))
       (Or
            (Put
                (DefinedSchema "foo-induction-axiom")
                 (List (Variable "R")(Variable "S")))
            (Put
                (DefinedSchema "bar-deduction-axiom")
                 (List (Variable "R")(Variable "S")))
            (Put
                (DefinedSchema "recurse"))
                 (List (Variable "R")(Variable "S"))))))

and the chaining query is

  (Get (VariableList (Variable "x")(Variable "y")) 
      (Put
          (DefinedSchema "recurse")
          (List  (Variable "x")(Variable "y")) ))

something like that. Details TBD. There is a simplified example of this in examples/pattern-matcher/recursive.scm and I think a more sophisticated demo is possible.

Anyway, what happens is the pattern matcher keeps walking the graph, recursing one step deeper, until it runs out of possibilities. Early termination/pruning would have to be done in the rules, because yes, infinite recursion is possible. (In practice, it runs out of temp atomspaces, and throws an exception. Each level of recursion starts a new temp atomspace, aka "kripke frame".)

[linas]

Comment about AndLink: the unit test uses AndLink. These are unordered links, which means the pattern matcher explores all possible permutations. Which makes it both slower, and the debug prints harder to read. Perhaps we should change AndLink to be an ordered link? No clue how many unit tests this would break...

[linas]

I think this is not about caching, I think it's got something to do with quotation. The pattern term tree shows up as (Quote (Variable "P") (Variable "Q")) instead of (Quote (Implication (Unquote (Variable "P")) (Unquote (Variable "Q")))) and because the pattern term is just plain ... wrong ... it does not get matched, and the cache remembers the failed match.

FWIW, removing the quotes makes the test run fine.

The pattern tree is assembled before any matching is done. So this is not a pattern matcher issue, its a pattern compiler issue.

[linas]

@ngeiswei please review and merge (or don't merge) #2889 as appropriate. On of my attempted fixes ends up with negative quotation levels. (Its not the right fix, but still ...)

[linas]

BTW, #2889 also happens to fix this bug!

Changed my mind, see next comment.

Now, I don't like this fix ... if I turn on debugging, the pattern is printed as

================ Mandatory clause 0:
(QuoteLink		; Q: HABV: HBV: L: [c2a916688f963e36][1]
  (VariableNode "$P")	; HABV: BV: L: [5638bfd3c771402][1]
  (VariableNode "$Q")	; HABV: BV: L: [60c52269c6f2aa28][1]
)

which is ... insane. This is NOT a printing error! The term tree is actually constructed like this, right here:

atomspace/opencog/atoms/pattern/PatternLink.cc

Lines 1133 to 1138 in 23884b6

	for (const Handle& ho: h->getOutgoingSet())
	{
	if (chk_const and is_constant(_variables.varset, ho)) continue;
	PatternTermPtr po(ptm->addOutgoingTerm(ho));
	make_term_tree_recursive(root, po);
	}

It's not unwrapping the quote correctly, and when I do try to unwrap it by hand, so that Mandatory clause 0: no longer looks insane, then I get half-a-dozen unit tests failing. Oddly enough, the pattern engine seems not to care about this bizarro clause: the way that it walks the graph allows it to find and correctly match the ImplicationLink, although how it does this is a bit opaque. (The ImplicationLink is still there, underneath the PatternTerm, which is how its found. Just that the PatternTerm itself is insane.)

[linas]

Changed my mind, and struck out what I wrote above. A minor printing fix does print the term tree correctly. I've merged that printing fix into master already.

I inserted an OC_ASSERT into #2889 to see where the quotation level goes negative. The answer is: any and every unit test involving quotes. The pattern cannot even be constructed: that is because during pattern compilation, we call any_unquoted_unscoped_in_tree() which calls is_unquoted_in_tree() which calls min_quotation_level() which calls Quotation::update() which sends the count negative.

There are two possible fixes:
(1) just merge #2889 and forget about it.
(2) look at where any_unquoted_unscoped_in_tree() is being called -- seems like maybe it is being called on things where it shouldn't be.

I will look at (2) for a while.

Sorry to spam you with all these comments, but ... it seems like recording the debug process is the right thing to do.

[ngeiswei]

Thanks for fixing this @linas!!! I skimmed through your changes, I understand some but not all of it. I don't have time to look deeper right now so I'm gonna leave it and only get back to it if more problems arise.

[ngeiswei]

Regarding combining Put and Or to create a forward chainer, yeah, that's cool, likely this could be used to implement the forward chainer purely on top of the pattern matcher. However for the backward chainer, I think a syntactic unifier would still be required. One option could be to integrate the unifier https://github.com/opencog/ure/tree/master/opencog/unify into the pattern matcher. I haven't carefully thought about the details though.

[ngeiswei]

Looks like everything works as it should on my end, I think I can close that issue.

[linas]

For the record: there were two classes of changes.

• Parts of pattern compilation started in the middle of quotes. By the time it got to the bottom, the quote count went negative. As a side effect, a handful of cases were treated incorrectly; thus this bug. These were fixed in Balanced quotes during pattern compilation #2890
• ScopeLink and friends would attempt to find variables and do scoping, even though they were quoted. One can tell if they are quoted because there are more unquotes than quotes, when going to the bottom. Thus, when ScopeLink is quoted, all scoping and variable-finding can be skipped. Should make the chainers run a tiny bit faster! This was fixed in Track down and fix more unbalanced QuoteLinks. #2893

What remains TBD:

• One unit test case explicitly goes negative.
• Half the URE unit tests go negative. I don't know why. This might be due to bugs in the URE, or it might be harmless. I've opened a bug report/enhancement request for the URE for this. its Unbalanced quotations ure#119