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 ...)