Support meta-rule in the URE

[ngeiswei]

Overview

A meta-rule, which could also be called a rule schema, is a rule that
produces a rule. It is convenient to have the URE support that as
explained below.

Motivation

Some rules don't fit well within a single BindLink, such as
universal or conditional instantiations. They however fit very well as
meta-rules. What the URE would do is, upon selecting a meta-rule,
generate a rule out of it to build a forward or backward chaining
step.

Example: conditional instantiation

The conditional instantiation rule, as currently implemented looks
like this

Bind
  VariableList
    TypedVariable
      Variable "$X-decl"
      Type "TypedVariable"
    Variable "$P"
    Variable "$Q"
  LocalQuote
    ImplicationScope
      Variable "X-decl"
      Variable "$P"
      Variable "$Q"
  ExecutionOutput
    GroundedSchema "scm: instantiate"
    List
      ImplicationScope
        Variable "X-decl"
        Variable "$P"
        Variable "$Q"

What it does is, upon finding an implication link, calls the schema
instantiate that will generate a new pattern matcher query to find
an $X so that $P is true to some degree and substitute $X in
$Q by the solution of $X, then apply a formula to calculate the TV
of $Q after substitution.

In some ways it already is a meta-rule, but the process of unfolding
it into a rule is obfuscated inside instantiate and the Backward
Chainer is unable to run that process in reverse.

Let's now define it as a meta-rule

Bind
  VariableList
    TypedVariable
      Variable "$X"
      Type "VariableNode"
    TypedVariable
      Variable "$type"
      Type "TypeNode"
    Variable "$P"
    Variable "$Q"
  LocalQuote
    ImplicationScope
      TypedVariable
        Variable "$X"
        Variable "$type"
      Variable "$P"
      Variable "$Q"
  LocalQuote
    Bind
      TypedVariable
        Variable "$X"
        Variable "$type"
      And
        Variable "$X"
        Variable "$P"
      LocalQuote
        ExecutionOutput
          GroundedSchema "scm: implication-full-instantiation-formula"
          List
            Variable "$X"
            Variable "$P"
            Variable "$Q"

What this does is, given an matching implication, generate the rule

    Bind
      TypedVariable
        Variable "$X"
        Variable "$type"
      And
        Variable "$X"
        Variable "$P"
      LocalQuote
        ExecutionOutput
          GroundedSchema "scm: implication-full-instantiation-formula"
          List
            Variable "$X"
            Variable "$P"
            Variable "$Q"

That rule can then be applied to find a term for $X, rewrite $Q
with it and calculate its TV. The resulting rule is much simpler but
more importantly all premises are visible and thus the Backward
Chainer is able to turn them into subsequent targets. Moreover, it
should be able to generate new targets for the meta-rule itself,
because there are also visible, so for instance the implication itself
can be used as target, not just its implicant.

[linas]

Looks reasonable to me.

One theoretical comment. We've long said that ImplcationLinks (ImplicationSvopeLinks) encode "declarative knowledge", while BindLinks are "just like Implication links, except that they're proceedural" So I think it is kind of funny that we are finally creating a "meta-rule" that can convert implication-links to bind-links.

The full table is at the bottom of the page http://wiki.opencog.org/w/Atom_relationships -- perhaps you want to have a meta-rule for each and every one of these?

[linas]

However, this also raises a different question: Perhaps BindLinks and ImplicationScopeLibnks should actually be exactly the same thing? Why do we need to have two "almost the same" links ... maybe just having one would be simpler (in the long run)?

Right now, BindLink has a big complicated init sequence, but maybe we should change it to not do any init at all, until the first time that the pattern matcher is invoked on it? That way, BindLink and ImplicationScope really could be the same type...

[bgoertzel]

ImplicationScopeLink has truth value semantics based on conditional
probability, BindLink does not necessarily do so ...

On Wed, Nov 9, 2016 at 12:05 AM, Linas Vepštas [email protected]
wrote:

However, this also raises a different question: Perhaps BindLinks and
ImplicationScopeLibnks should actually be exactly the same thing? Why do we
need to have two "almost the same" links ... maybe just having one would be
simpler (in the long run)?

Right now, BindLink has a big complicated init sequence, but maybe we
should change it to not do any init at all, until the first time that the
pattern matcher is invoked on it? That way, BindLink and ImplicationScope
really could be the same type...

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
https://github.com/opencog/atomspace/issues/986#issuecomment-259299266,
or mute the thread
https://github.com/notifications/unsubscribe-auth/AFolXL9bsPVxNrdOxKu2693Qh0YPXfKIks5q8Q5fgaJpZM4KsO5A
.

Ben Goertzel, PhD
http://goertzel.org

“I tell my students, when you go to these meetings, see what direction
everyone is headed, so you can go in the opposite direction. Don’t polish
the brass on the bandwagon.” – V. S. Ramachandran

[amebel]

Is meta-rule a means of expanding a macro-rule, so as to make it visible to ure-bc?

[ngeiswei]

@amebel not exactly, although it could. A meta-rule is merely a rule that produces a rule. The URE wouldn't necessarily need to support it, it could just handle that in 2 steps (although it would at least need to add the produced rule in the rule-base) but I feel it's probably better to do the 2 step on the fly. I haven't started coding so I'll see.

[ngeiswei]

@linas yes I completely see the irony and it made me think a bit, as Ben said I think the ImplicationLink is a specialized BindLink with predefined TV formula on the rewriting term.

[linas]

OK. Its OK to leave this as is, but just keep that question active in the back of your mind for the next few years, as it may need to be revisited.

[ngeiswei]

Meta-rules are almost completely supported by the URE, however building inference trees with them is trickier than I thought so what the forward and backward chainers are doing for now is merely turn them into regular rules, see https://github.com/opencog/atomspace/blob/master/opencog/rule-engine/backwardchainer/BackwardChainer.cc#L133 https://github.com/opencog/atomspace/blob/master/opencog/rule-engine/forwardchainer/ForwardChainer.cc#L130, then build inference trees with those regular rules.

The problem comes when going backward because the inference tree looses the process that led to turning the meta-rules into regular rules, and thus looses the premises of the meta-rules!

This makes some forms of backward chaining impossible, for instance:

Given the axioms

(Implication (stv 1 1)
  (Predicate "P")
  (Predicate "Q")

(Implication (stv 1 1)
  (Predicate "Q")
  (Predicate "R")

(Evaluation (stv 1 1)
  (Predicate "P")
  (Concept "a"))

You want to prove R(a). You have at least 2 ways to do that

1. Prove (Implication (Predicate "P") (Predicate "R")), i.e. P->R, using deduction https://github.com/opencog/opencog/blob/master/opencog/pln/rules/term/deduction.scm, then use conditional instantiation https://github.com/opencog/opencog/blob/master/opencog/pln/meta-rules/predicate/conditional-full-instantiation.scm, to obtain R(a) from P(a).
2. Or, chain 2 conditional instantiations, the first one to obtain Q(a) from P(a), and the second one to obtain R(a) from Q(a).

Currently the backward chainer will only be able to prove R(a) the second way, not the first way, because in the first way, by the time the inference is being built, the knowledge of P->R hasn't been built yet, thus the conditional instantiation meta-rule cannot be converted into a regular rule.

After thinking more deeply about it, I've concluded that to solve that we need to have a UnifyLink of some sort to express the notion of unification in Atomese, which is currently only exposed to the C++ code https://github.com/opencog/atomspace/blob/master/opencog/unify/Unify.h but that's pretty foggy at that point, probably the more specialized notion of unification between inference tree premise (or conclusion) with rule conclusion (or rule premise) is enough...

[ngeiswei]

A good example requiring full meta-rule support in the backward chainer can be found here https://github.com/opencog/opencog/tree/master/examples/pln/good-songs

[ngeiswei]

Another example is BackwardChainerUTest::test_induction() that would be re-enabled once meta-rule is supported.

[ngeiswei]

A propotype written by @rTreutlein waiting to be merge can be found in that branch

https://github.com/opencog/ure/tree/rTreutlein-MetaRuleSupport