Automatic alpha-conversion during pattern matching

[ngeiswei]

The following

(define query (Get
                (VariableList
                  (Variable "$vardecl")
                  (Variable "$vardecl-0")
                  (Variable "$vardecl-1")
                  (Variable "$body-0")
                  (Variable "$body-1"))
                (Present
                  (Quote (Lambda
                           (Unquote (Variable "$vardecl"))
                           (And
                             (Unquote (Variable "$body-0"))
                             (Unquote (Variable "$body-1")))))
                  (Quote (Lambda
                           (Unquote (Variable "$vardecl-0"))
                           (Unquote (Variable "$body-0"))))
                  (Quote (Lambda
                           (Unquote (Variable "$vardecl-1"))
                           (Unquote (Variable "$body-1")))))))

attempts to grab a pattern, lambda link of 2 conjuncts, only if each conjunct is also a pattern (wrapped in a LambdaLink as well), for instance, given the KB

(define X (Variable "$X"))
(define Y (Variable "$Y"))
(define A (Concept "A"))
(define InhXA (Inheritance X A))
(define InhYA (Inheritance Y A))
(define PX (Lambda X InhXA))
(define PY (Lambda Y InhYA))
(define VarXY (VariableList X Y))
(define PXY (Lambda VarXY (And InhXA InhYA)))

We would expect to get

$vardecl = (VariableList X Y)
$vardecl-0 = X
$vardecl-1 = Y
$body-0 = Inheritance X A
$body-1 = Inheritance Y A

but instead get nothing.

It is explained by the fact that

1. The atomspace alpha-convert PY to PX
2. The pattern matcher doesn't realized that PX could be alpha-converted back to PY (or any alpha-convertion such that it doesn't collide with PX) during pattern matching.

[linas]

I don't see how this has anything to do with alpha conversion, since nothing in the search pattern is forcing the variable names to match. It's just looking for two bodies -- those should be findable, and then after that (after finding them) it looks for what is attached to the bodies -- which should be the variable declarations, whatever they may be, converted or not. What am I missing?

[linas]

Ohh, I see, the bodies cannot match up. Hmmm.

[linas]

OK, why are the quotes needed? Would it be OK to search, without the quotes?

[linas]

So I poked around just for a bit. I notice that this simpler quote-less search also fails:

(define q3 (Get
                (VariableList
                  (Variable "$vardecl")
                  (Variable "$body-0")
                  (Variable "$body-1"))
                (Present
                  (Lambda
                           (Variable "$vardecl")
                           (And
                             (Variable "$body-0")
                             (Variable "$body-1"))))))

I can't think of any good reason why it should fail. Maybe there is a reason, but I don't remember why.

Anyway, either with, or without quotes, this does indeed seem like a bug.

[linas]

The q3 above fails because of line 303 in DefaultPatternMatchCB.cc and despite the comments there, which seem to have been written by me, I don't understand (remember) what its doing, or why. The comments also say something about ForwardChainerUTest wanting to do it this way...

[linas]

OK, so pull req #2071 seems to be a necessary pre-req for fixing this problem. I understand why this is failing. I'm pondering a solution.

[linas]

I see two possible solutions. One is to create a new link type, that doesn't exist yet, called AlphaEqualLink which returns true if the two parts are alpa-convertible to one-another. Its like EqualLink, but freer. That would allow this query:

(define q6 (Get (VariableList
                  (Variable "$vardecl")
                  (Variable "$vardecl-0")
                  (Variable "$vardecl-1")
                  (Variable "$body-0")
                  (Variable "$body-1")
                  (Variable "$body-0-eqv")
                  (Variable "$body-1-eqv"))
                (And (Present (Lambda
                           (Variable "$vardecl")
                           (And (Variable "$body-0")
                             (Variable "$body-1")))
                  (Lambda
                           (Variable "$vardecl-0")
                           (Variable "$body-0-eqv"))
                  (Lambda
                           (Variable "$vardecl-1")
                           (Variable "$body-1-eqv")))
              (AlphaEqual (Variable "$body-0") (Variable "$body-0-eqv"))
              (AlphaEqual (Variable "$body-1") (Variable "$body-1-eqv"))
                ))

I think that would work. I haven't tried it yet. Its not terribly efficient, as its potentially a combinatorial explosion. But really no different than queiries with GreaterThanLink, etc.

The other solution is to automatically do something kind-of-like the above, but hidden inside the pattern matcher. This ... I kind-of don't like it because its hard to implement in a general way, and would make the pattern matcher even more complex than it already is ...

I'm gonna try the AlphaEqualLink idea real quick. @ngeiswei If you don't like it, I understand. I don't yet see a third way...

[linas]

Pull req #2072 adds the AlphaEqualLink. It seems to work, and gives at least some kind of plausible work-around for this problem. At any rate, it seems harmless. I did not add unit tests for either #2071 or for #2072 ...

[vsbogd]

@ngeiswei , to understand the issue better (as at the first glance I also could not find how it is related to alpha conversion): Am I right that issue is if one createsGet link then atomspace code alpha converts parts of the lilnk. But pattern matcher cannot deal with result of such conversion?

[ngeiswei]

Am I right that issue is if one createsGet link then atomspace code alpha converts parts of the lilnk. But pattern matcher cannot deal with result of such conversion?

@vsbogd, I think it's deeper than that. A scope link should virtually (using @linas terminology) exists in all its alpha converted forms, and so if we ask the pattern matcher to fetch scope links such that one them should be alpha-converted to match the constraints of the query, the pattern matcher should do it on-the-fly. It seems to me the only/best way to fulfill the query provided in that example, the same scope link is matched twice, but with a different variable name in order to match the body conjunct of the conjunction scope link.

[linas]

At this time,

• (cog-exeucte! query) from Automatic alpha-conversion during pattern matching #2070 (comment) returns the empty set.
• (cog-exeucte! q3) from comment Automatic alpha-conversion during pattern matching #2070 (comment) returns the expected answer, plus some extra stuff (unquotes)
• (cog-exeucte! q6) from comment Automatic alpha-conversion during pattern matching #2070 (comment) returns what looks like reasonable stuff, plus extra stuff (unquotes), mostly cause it is not typesd strongly enough.

Not sure what do do here. for now it seems liem q6 is a reasonable work-around. Automated alpha equivalence could be done, I suppose, but I also want to see this is a special and unusual case of #554. Leaving open for now.