Idea: Recursive Unification using the Pattern Matcher

From OpenCog
Jump to: navigation, search

Recursive Unification

Instead of performing unification (variable grounding) once, some situations may require multiple passes to fully ground the variables, if the unification candidates themselves contain variables.

Discussed in this e-mail thread.

Currently, the pattern matcher does not automatically perform additional passes over an expression after variables are grounded by their substitutions; that is, it does not perform "recursive" grounding.

The goal is to not write a separate BindLink construct for every "rule" that has been expressed in the AtomSpace within an ImplicationLink, since these "rules" may be numerous and constantly being produced by

to create atomspace implications that contain variables. The pattern matcher can be used for unification when the grounding expression, itself, contains variables.

Example

An experiment to create a naive Modus Ponens procedure that looks for implications with variables in the atomspace and then grounds them to produce the implicands.

So, for example:

(define pln-rule-modus-ponens
(BindLink
    (ImplicationLink
        (ImplicationLink
            (VariableNode "$A")
            (VariableNode "$B")))
        (ExecutionLink
            (GroundedSchemaNode "scm: pln-formula-simple-modus-ponens")
            (ListLink
                (ImplicationLink
                    (VariableNode "$A")
                    (VariableNode "$B"))))))))

(define (pln-formula-simple-modus-ponens AB)
(let
    ((B (gdr AB)))
        (cog-set-tv!
            B
            (pln-formula-simple-modus-ponens-side-effect-free
                AB))))

Given the following unification candidate in the atomspace:

"Smoking causes cancer."

(ImplicationLink (stv 0.6225 1.0)
    (EvaluationLink
        (PredicateNode "smokes")
        (ListLink
            (VariableNode "$X")))
    (EvaluationLink (stv 0.6225 1.0)
        (PredicateNode "cancer")
        (ListLink
            (VariableNode "$X"))))

And the following grounded predicate:

"Frank smokes."

(EvaluationLink (stv 1.0 1.0)
    (PredicateNode "smokes")
    (ListLink
        (ConceptNode "Frank")))

Currently, running the pattern matcher:

(cog-bind pln-rule-modus-ponens)

will produce the following unifier:

(ImplicationLink (stv 0.6225 1.0)
    (EvaluationLink
        (PredicateNode "smokes")
        (ListLink
            (VariableNode "$X")))
    (EvaluationLink (stv 0.6225 1.0)
        (PredicateNode "cancer")
        (ListLink
            (VariableNode "$X"))))

But the desired unifier would actually contain a unification for any nested variables found in the unification candidate:

(ImplicationLink (stv 0.6225 1.0)
    (EvaluationLink
        (PredicateNode "smokes")
        (ListLink
            (ConceptNode "Frank")))
    (EvaluationLink (stv 0.6225 1.0)
        (PredicateNode "cancer")
        (ListLink
            (ConceptNode "Frank"))))

all implications (rules containing variables) would be iterated over, and for each rule, all the possible groundings would be produced with their associated truth values.

Solution

This problem is easily solved: if there are variables in the result, then bindlink should be called again, until there are no more variables in the result.

Exising C++ code in the /opencog/atomutils/FindUtils.h can searc an expression to find one (or more, or all) variables. If any are found, just call the pattern matcher again. It can do this in one of two ways: call the pattern matcher directly, or create a new SatisfactionLink, and invoke that. One may want to delete the SatisfactionLinks when done, so that they don't glom up the AtomSpace. There is a slight performance boost from calling the pattern matcher directly, instead of creating a SatisfactionLink.

See also

  • Higher-order unification is also an interesting topic, but would seem to be a much more complex topic than the specific case of recursive unification presented here.