progress report, April 2012

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

A lot of progress in the past 2 months:

In Clojure, finished parallel version of backward chaining:

http://code.google.com/p/genifer/source/browse/clojure/backward-chaining.clj

In Clojure, new version of unification:

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

The unification is for a new logic which is a typeless "algebraic" logic with only 1 operator, the application (○).

So "John loves Mary" is:

    john ○ loves ○ mary

And an example of unification is:

    john ○ X ○ mary ○ Y    =?    john ○ loves ○ mary ○ obsessively

yielding the substitution:

   { loves / X, obsessively / Y }.

Any combination of atoms and variables on either side is acceptable.  There are more examples in the code.  The power of this seemingly simple logic is similar to higher-order logic.

If pairing (_,_) is added, this logic's power is equivalent to λ-calculus, thus Turing universal.  But pairing is not needed for natural language thanks to a reduction trick.  I'll revise my book soon to explain all this...

Clojure is my current favorite language.  As usual, don't be disappointed if this is not your favorite platform -- we continue to try to be language-agnostic.

=)

--

KY

"The ultimate goal of mathematics is to eliminate any need for intelligent thought" -- Alfred North Whitehead

[Abram Demski]

YKY,

What is the equivalence to lambda calculus when pairing is added?

Without pairing, what is your reason for believing that the representation has a great deal of power? (Is it equivalent to something?)

--Abram

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

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

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

On Mon, Apr 23, 2012 at 1:16 PM, Abram Demski <abram...@gmail.com> wrote:

What is the equivalence to lambda calculus when pairing is added?

Without pairing, what is your reason for believing that the representation has a great deal of power? (Is it equivalent to something?)

The syntax looks almost like first-order logic, but if we change the notation:

   a ○ b ○ c   =   a(b(c))

and you can have a variable

   X = a ○ b

that X is actually a λ term:  λx. a(b(x)).

So it is a monadic higher-order logic.

When we add pairing:

    a ○ (b,c)  =  a(b,c)

it has the power of dyadic HOL.  If we can nest pairs then it is equivalent to HOL.

KY

[Abram Demski]

YKY,

Quick note...

Application and composition are different. Using '○' for composition and (f x) for application, and also using the mathematically common f(x) notation to illustrate:

(f ○ g) = \x. f(g(x))

(f g) = f(g)

So,

   a ○ b ○ c   =   a(b(c))

works fine where '○' is application;

   X = a ○ b

that X is actually a λ term:  λx. a(b(x)).

seems to be assuming that  '○' is composition (as it more often denotes).

I'm not saying this is anything more than a slip-up on your part (it isn't so important for your claim of representational power I suppose).

So, other than that, I'd just suggest you spell out a more careful equivalence to determine the exact representational power.

--Abram

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

On Mon, Apr 23, 2012 at 1:16 PM, Abram Demski <abram...@gmail.com> wrote:

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

On Mon, Apr 23, 2012 at 2:57 PM, Abram Demski <abram...@gmail.com> wrote:

 

Application and composition are different. Using '○' for composition and (f x) for application, and also using the mathematically common f(x) notation to illustrate:

(f ○ g) = \x. f(g(x))

(f g) = f(g)

So,

   a ○ b ○ c   =   a(b(c))

works fine where '○' is application;

   X = a ○ b

that X is actually a λ term:  λx. a(b(x)).

seems to be assuming that  '○' is composition (as it more often denotes).

Ahh... thanks a lot =)   I confused the two, and that's why I found it hard to understand Curien's book where I picked up the idea of some sort of "categorical combinatory logic".

I'll have to rethink a bit...  hopefully the idea still works -- looks like it could.  It only gets better if the foundations are clearer =)

KY

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

OK I think I meant for ○ to be "apply".  From now on I should use another symbol for application, perhaps "♦".

Y ♦ K ♦ Y

Looks pretty good =)

My unify code may be incorrect.  I have to test it thoroughly.  It should be equivalent to Huet's algorithm, when reduced to the untyped and monadic case.

Also, pairing may be required after all, or the logic would be too unexpressive...

KY

[Abram Demski]

YKY,

Well, normally application is (a b).. the operator is the space, if you must have an operator. :)

Would your unification algorithm handle cases like ((a b) (c d)), or just 'linear' cases like you showed: (a (b (c d)))?

You mentioned making additional definitions, like x = (a b). Does that mean equational reasoning is currently handled, or is it a to-do?

--Abram

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

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

On Tue, Apr 24, 2012 at 12:44 AM, Abram Demski <abram...@gmail.com> wrote:

 

Well, normally application is (a b).. the operator is the space, if you must have an operator. :)

That's good too.  In the Clojure code a formula is represented as a list such as:  [ a b X c Y d ... ]

so the operator is indeed the white space.

Would your unification algorithm handle cases like ((a b) (c d)), or just 'linear' cases like you showed: (a (b (c d)))?

The logic is associative:  a(bc) = (ab)c.

So ((ab)(cd)) = (a(b(cd))) = abcd.

This is generally called "don't need parentheses".

You mentioned making additional definitions, like x = (a b). Does that mean equational reasoning is currently handled, or is it a to-do?

To do.  In fact, I'm planning to implement unification modulo a rewrite system R.  The technique is called narrowing, which mingles rewriting and syntactic-unify steps.  R can be a very big rewrite system.

Let me explain my rather unusual idea:

    "John loves Mary obsessively"

would be rendered as:

    john ♦ loves ♦ (mary, obsessively)

because the graphical structure of the sentence is obviously:

                 / obsessively

    john loves

                 \ mary

and this logic formula can be broken down into:

    (1) john loves mary

    (2) john loves obsessively

which is not a coincidence.  It is a genuine feature of the compositionality of meanings.

But a problem arises if we have both:

   (a) John loves Mary obsessively

   (b) John loves Ann perfunctorily

which would result in these 4 formulas after decomposition:

   (i) john loves obsessively

   (ii) john loves mary

   (iii) john loves perfunctorily

   (iv) john loves ann

And (i) and (iii) don't sit well together.  The solution is that we must group {i, ii} and {iii, iv} into separate units.  We could introduce braces into the logic, but that ruins the simplicity of sentential logic.

My solution is to assign tree-structured truth values as contexts to every formula.  Then, using a set of context axioms, I can stipulate that formulas in different contexts don't interfere with each other, unless one context is included in the other context.

With this trick, now we can write:

   "John loves Mary obsessively"

as:

    john loves mary                <tv1>

    john loves obsessively     <tv2>

and thus we can even get rid of (_, _).  In other words, the logic can be purely monadic.

What's more, we can express relations such as:

   x > y

simply as:

   (x > y)

ie, with the application operator:

   x ♦ > ♦ y

That used to be expressed in FOL as:

   R(x,y).

So this monadic logic can be very expressive, no? =)

KY

[Abram Demski]

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

On Tue, Apr 24, 2012 at 12:44 AM, Abram Demski <abram...@gmail.com> wrote:

 

Well, normally application is (a b).. the operator is the space, if you must have an operator. :)

That's good too.  In the Clojure code a formula is represented as a list such as:  [ a b X c Y d ... ]

so the operator is indeed the white space.

Would your unification algorithm handle cases like ((a b) (c d)), or just 'linear' cases like you showed: (a (b (c d)))?

The logic is associative:  a(bc) = (ab)c.

So ((ab)(cd)) = (a(b(cd))) = abcd.

This is generally called "don't need parentheses".

Composition is associative. Application is not associative.

But does this work in the general case? How complicated does the logic within the truth values have to get?

 

 

What's more, we can express relations such as:

   x > y

simply as:

   (x > y)

ie, with the application operator:

   x ♦ > ♦ y

This feeds (> y) to x, which means that x needs to be a function which can take such arguments and return the right thing...

 

That used to be expressed in FOL as:

   R(x,y).

So this monadic logic can be very expressive, no? =)

KY

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

On Tue, Apr 24, 2012 at 2:39 AM, Abram Demski <abram...@gmail.com> wrote:

Composition is associative. Application is not associative.

I see...  this is where I confused application with composition.

 

With this trick, now we can write:

   "John loves Mary obsessively"

as:

    john loves mary                <tv1>

    john loves obsessively     <tv2>

and thus we can even get rid of (_, _).  In other words, the logic can be purely monadic.

But does this work in the general case? How complicated does the logic within the truth values have to get?

In fact I have gotten this idea when analyzing contexts in general.  For example "This is the story of little Red Ridinghood.  She is the prettiest creature ever seen...."  The first sentence creates a context.

All we need is a partial order where some contexts can be compared with a > relation, while some contexts are incomparable.  I think a tree structure can represent the partial order.  I have summarized the axioms in my book, it's there already, but some other parts still needs development...

 

   x ♦ > ♦ y

This feeds (> y) to x, which means that x needs to be a function which can take such arguments and return the right thing...

Again, the problem from confusing application with composition.

I need 2 features that are somewhat contradictory:

1.  associativity, which belongs to composition

2.  x ♦ (a,b) = x(a,b) = (xa, xb)  which works like application

Hmmmmm.......

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

Let's retain composition.

So x ♦ (a,b) is by axiom equal to (x ♦ a, x ♦ b)

That can be regarded as a special axiom about composition with pairs.  Also it's a distributive law.

If a pair (c,d) is not further composed with other symbols, it can be regarded as 2 propositions c, d. 

So

    (x ♦ a, x ♦ b)  = x ♦ a  /\  x ♦ b.

Is that acceptable?

KY

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

You can think of the logic more like an algebra that has 2 operations, both of arity 2:  composition (◦) and pairing (,).

If we change

   ◦  to  *

   ,  to  +

The axioms can be written as:

   a * (b * c) = (a * b) * c

   a * (b + c) = a * b + a * c

That looks very "normal".

KY

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

PS:

§3.5.1 in my book describes inference with contexts.  (I've had a bunch of new ideas recently so the book needs a lot of revision.)

I think it's OK to regard my logic as the "algebra or logic of composition".  It really deals with composition of meanings of natural-language concepts.  For example compound concepts such as:

    social ◦ entrepreneurship

    absolute ◦ monarchy

    spaghetti ◦ Bolognese

are really the same as compositions like:

    john ◦ loves ◦ mary.

What about application?  I think perhaps my logic does not have a native notion of functions but it may be able to emulate them.  Due to the distribution axiom, f ◦ (a,b) cannot emulate f(a,b).  So it may need to introduce new operators.

At this point I realize my logic is tailored to process natural language to the neglect of mathematical logic.  But it may be similar to the way humans do math.  We can try to extend the logic, but its simplicity makes inference algorithms easier to implement, so there is a trade-off.

Maybe the best way is to use multiple theorem provers, so the Genifer logic engine can invoke another crisp logic engine, that may have a formal type system.

KY

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

PS again! =)

I feel bad that my logic is now so narrowly focused on natural language.  I should look at other domains and try to generalize the logic to make it truly universal.  The 2 main domains I want to look at are:

1.  mathematics

-- Unfortunately there is not yet a consensus foundation of mathematics;  category theory is very fascinating to me, but it does not seem to be foundational in a very strict sense

2.  vision (ie, a representation of the 3D or 4D world)

-- I'll take a look at geometric algebras like Clifford algebra.  The goal is to find a formal language that can represent everything in the "physical", ie, spatio-temporal, world.

KY

[William Taysom]

> category theory is very fascinating to me, but it does not seem to be foundational in a very strict sense

What counts as "foundational"? To me it seems category theory is more metaphorical than anything else.

[Matt Mahoney]

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

> I feel bad that my logic is now so narrowly focused on natural language.

Actually, I think that is good. Mathematics is a subset of natural
language, so your logic should handle it as well.

But I wonder if it really does. I think you need a longer example. How
would you translate the text of this email into your logic?

-- Matt Mahoney, mattma...@gmail.com

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

On Tue, Apr 24, 2012 at 9:23 PM, William Taysom <wta...@gmail.com> wrote:

 

What counts as "foundational"?  To me it seems category theory is more metaphorical than anything else.

Foundation of mathematics = a formal system in which all of mathematics can be performed.  "All maths" in a strict sense.  I'm not familiar with that area, but it seems that a consensus solution has not been found.

Category theory is a great conceptual tool.  I'm still learning it... =)

KY

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

On Tue, Apr 24, 2012 at 9:33 PM, Matt Mahoney <mattma...@gmail.com> wrote:

> I feel bad that my logic is now so narrowly focused on natural language.

Actually, I think that is good. Mathematics is a subset of natural
language, so your logic should handle it as well.

But I wonder if it really does. I think you need a longer example. How
would you translate the text of this email into your logic?

I'll do that shortly...

The basic idea is the composition of 2 concepts, which is also directional, so A◦B ≠ B◦A.

Sentences are built up via concepts composed with others, forming compound concepts and so on.  It is usually very easy to inspect a sentence and tell which word (ie concept) is modifying which other.  That will give you a graph with directed links.  From that graph you can translate into the logic.  What you see a branch, use the (,) pairing.

I'll translate the last email, with diagrams.  But I have to do some coding now and meet a business guy tomorrow... =)

KY

[Matt Mahoney]

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

> Sentences are built up via concepts composed with others, forming compound
> concepts and so on.  It is usually very easy to inspect a sentence and tell
> which word (ie concept) is modifying which other.  That will give you a
> graph with directed links.  From that graph you can translate into the
> logic.  What you see a branch, use the (,) pairing.

I understand, so your logic is equivalent to building a parse tree. So
a sequence "X Y" means that Y modifies X. A sequence "X (Y, Z)" means
that Y and Z both modify X. For example:

I ate pizza with pepperoni.

ate
/ \
I pizza
/
with
/
pepperoni

ate (I, pizza with pepperoni)

I ate pizza with a fork

ate
/ | \
I pizza with
/
fork
/
a

ate (I, pizza, with fork a)

I ate pizza with Bob

ate
/ \
I pizza
/
with
|
Bob

ate (I with Bob, pizza)

Is this right?

-- Matt Mahoney, mattma...@gmail.com

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

On Wed, Apr 25, 2012 at 12:11 AM, Matt Mahoney <mattma...@gmail.com> wrote:

 

I understand, so your logic is equivalent to building a parse tree.

Similar, but not exactly the same.  The parse tree tries to express the superficial structure of natural language sentences.  My logic tries to express meanings.

 

So

a sequence "X Y" means that Y modifies X. A sequence "X (Y, Z)" means
that Y and Z both modify X.

Right.  We can also reverse the directions, that's just a convention.  I haven't decided yet.

I ate pizza with pepperoni.

 ate
/     \
I     pizza
    /
  with
 /
pepperoni

But you also need to indicate the directions of the links.  Maybe your convention is "lower in the graph modifies higher"?

I'm still sometimes a bit unsure about who is modifying whom.  For example, "film noir" may be regarded as "film" modified by "noir", which is a kind of film (primary) that has dark themes (the modifier).  But alternatively we can also say it is something dark (primary) that happens to be film (modifier).  The 2nd way is awkward, but I can't see an absolute reason why it cannot be so.

Anyway, your graph then translates to:

     ate (I, pizza with pepperoni)

My version (not necessarily more correct):

                              pepperoni

                             /

                          with

                        / 

I -- ate -- pizza

which is:  I ◦ ate ◦ pizza ◦ with ◦ pepperoni

I ate pizza with a fork

  ate
/    |     \
I pizza  with
           /
        fork
       /
     a

ate (I, pizza, with fork a)

Right.

 

I ate pizza with Bob

  ate
 /   \
 I   pizza
 /
with
|
Bob

 
ate (I with Bob, pizza) 

I'm not sure about this one.  (I ◦ with ◦ bob) seems not a meaningful compound concept.  In my logic, every composition should be meaningful.  In this case I think "with Bob" still modifies "ate".

Thanks to your examples, I realize it may not always be clear who is modifying whom.  I'll think about this more...

KY

[Matt Mahoney]

I was using the convention that the root of the parse tree is at the
top and that the child nodes modify the parent. Usually a sentence is
parsed with the verb at the root, but I could see making the subject
the root too.

Of course the problems with parsing natural language are well known.
Usually we have to know what the sentence means before we can parse
it. Thus, the different parses of the "pizza" example. We know from
our semantic knowledge that "with pepperoni" has to modify "pizza" and
"with a fork" has to modify "ate". We can try all grammatically
correct parses and reject the ones that don't fit the semantic model.
But this does not always work. For example, "pretty little girl's
school" can be parsed 24 different ways, many of which are meaningful.

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

--
-- Matt Mahoney, mattma...@gmail.com