progress: narrowing completed

[YKY (Yan King Yin, 甄景贤)]

First version of narrowing completed... that was quite a lot of work =)

http://code.google.com/p/genifer/source/browse/clojure/genifer/src/genifer/narrowing.clj

Narrowing is just a more sophisticated form of unification modulo a set of equations.

Apparently when both the term and the rewrite rule have multiple variables, it is prone to infinite loops.  For example, to unify by narrowing:

    X loves Y

with the (actually unrelated) rewrite rule:

    W gives Z the creeps = W disgusts Z

there is a substitution:

    X loves /W

    gives Z the creeps /Y

so that the result of rewriting is the unexpected:

     X loves disgusts Z

and it can infinitely lengthen via the same rewrite:

     X loves disgusts disgusts disgusts.......

My temporary solution is to limit rewrite rules to have at most 1 variable.

I guess the problem has to do with the rewrite system's confluence property, which I'll look into later.  For now, I'm happy that basic narrowing is working.

Next I'll add 2 inductive learning methods...

KY

[Abram Demski]

YKY,

Apparently when both the term and the rewrite rule have multiple variables, it is prone to infinite loops.  For example, to unify by narrowing:

    X loves Y

with the (actually unrelated) rewrite rule:

    W gives Z the creeps = W disgusts Z

there is a substitution:

    X loves /W

    gives Z the creeps /Y

so that the result of rewriting is the unexpected:

     X loves disgusts Z

How is this in any way correct (even before the infinite loop problem)?

Shouldn't the rewrite rule just fail to apply here?

--
Abram Demski
http://lo-tho.blogspot.com/

[YKY (Yan King Yin, 甄景贤)]

On Wed, May 9, 2012 at 6:00 AM, Abram Demski <abram...@gmail.com> wrote:

 

Apparently when both the term and the rewrite rule have multiple variables, it is prone to infinite loops.  For example, to unify by narrowing:

    X loves Y

with the (actually unrelated) rewrite rule:

    W gives Z the creeps = W disgusts Z

there is a substitution:

    X loves /W

    gives Z the creeps /Y

so that the result of rewriting is the unexpected:

     X loves disgusts Z

How is this in any way correct (even before the infinite loop problem)?

Shouldn't the rewrite rule just fail to apply here?

Yes it should fail...  I was playing around with some rules (I found "W gives Z the creeps" to be a common English phrase on Google), but unexpectedly it produced the above rewrite step.

I guess the natural reason for this is that X, Y, W and Z are supposed to be people, but "X loves" is not a person.  So it's the semantic information that resolves it.

Without built-in types, I can add separate clauses saying X, Y, ... are people.  Another solution which seems feasible is to have rules like:

    someone gives another person the creeps...

where explicit variables are eliminated, and substitution proceeds by rewriting of equals -- for example with:

    john gives mary the creeps....

using the rewrite rule (or equation, if not oriented):

   john = someone

   mary = a person.

Narrowing seems to be a quite powerful mechanism...

KY

[YKY (Yan King Yin, 甄景贤)]

PS:

It appears that one can use rewrite rules to perform inference involving quantification, for example:

     All man are mortal

can be rewritten in some way to give:

     Socrates is mortal

but I've decided against this usage because it doesn't follow the original principle, namely that the rewrite system is a set of equations relating similar concepts.  The use of it to perform quantified inference is somewhat of an abuse.

So, rewriting is for similarity of concepts, and variables and quantifications are still needed for generalizing and learning...

KY

[Abram Demski]

If equations are understood to work both ways, then clearly this is an abuse, yes.

--Abram

[YKY (Yan King Yin, 甄景贤)]

I just implemented some Clojure functions for context management.  All the contexts are stored in a big tree structure.

What I discovered is that contexts cannot deal with the problem of compound sentences, so the logic really needs to have 2 operations:  composition and pairing.  Their axioms look like addition and multiplication:

Multiplication is not commutative:

    a*b != b*a

Addition is commutative:

    a+b = b+a

Both + and * are associative, which means that sums or products never need parentheses.

There is the distribution law:

    a(b+c) = ab+ac

What is special about + is that it is different from AND or OR.

    a+b |= a

    a+b |= b

However,

    a, b ! |= a+b

In words:  addition creates pairs (or tuples) that imply the individuals, but individuals cannot imply arbitrary pairs.

So,

    john gives mary the ball

    john gives kevin $1

implies:

    john gives the ball

    john gives to mary

    john gives to kevin

    john gives $1

but these do not imply:

    john gives the ball to kevin

    john gives $1 to mary

I'll try to incorporate the new axioms into the Clojure code...

Also, I've been discussing with others to build a Javascript GUI for entering natural language sentences visually...

KY

[Ivan Vodišek]

May I be free to draw a parallel I was inspired to by you?

>What is special about + is that it is different from AND or OR.

>    a+b |= a

>    a+b |= b

>However,

>    a, b ! |= a+b

This strongly reminds me of induction / reverse induction, although it's somewhat different from it

a+b+<something else> |= x

When we say x we are not sure does it imply back a, b, <something else>, or some combination of thees. It would have to be at least one of thees, but <something else> is unknown.  

2012/5/14 YKY (Yan King Yin, 甄景贤) <generic.in...@gmail.com>

[james northrup]

so far you've got something that looks like sparql test queries.

[YKY (Yan King Yin, 甄景贤)]

On Wed, May 16, 2012 at 1:35 AM, james northrup <northru...@gmail.com> wrote:

so far you've got something that looks like sparql test queries.

* and + may look isomorphic to AND and OR, but

   a*b != b*a

whereas

   a AND b = b AND a.

That makes the logic subtly different from Boolean algebra...  otherwise we'd be able to use database query optimizers to answer queries in Gen logic.

In fact, Genifer's * and + can co-exist with Boolean algebra, resulting in a logic with totally 4 operations.

KY