CompositionLink throws exception

[linas]

I tried to encode ComposeLinkUTest::test_execute_2() in scheme, to see what happens. I believe the intended encoding is this:

(define f1 (Project (Number 0)))
(define f2 (Lambda 
   (VariableList (Variable "X") (Variable "Y") (Variable "Z"))
   (Inheritance (Variable "Y")(Variable "Z")) ))

(define g (Lambda (Evaluation (Variable "X") (Variable "Y"))))

(define c (Compose g (List f1 f2)))

(cog-execute! c)

This throws an exception: "cog-execute!" "Not executable: ProjectLink"

[linas]

I'm also trying to figure out what ProjectLink is supposed to do. The standard definition is here: https://en.wikipedia.org/wiki/Projection_(mathematics) but I can't quite square what you are doing with that...

For a while I thought you were trying to do this:

;; f1a is the identity combinator, it does nothing.
(define f1a (Lambda (Variable "W") (Variable "W")))
(cog-execute! (Compose g (List f1a f2)))

but this blows up. I was trying to paste the identity into position zero of g and f2 into position 1 of g. But that would imply that (Compose g (List f1a f2)) takes four args: W X Y and Z. Right? That is, I expect to get

(Lambda 
    (VariableList (Variable "W")(Variable "X")(Variable "Y")(Variable "Z"))
    (Evaluation (Variable "W") (Inheritance (Variable "Y")(Variable "Z"))))

[linas]

Now I'm trying "projection by hand" and "injection by hand" So for example:

(define inject (Lambda (VariableList (Variable "S")(Variable "T"))
   (List (Concept "junk") (Variable "S")(Variable "T"))))
(define r (Compose f2 inject))
(cog-execute! r)

I expect to get this:

(Lambda (VariableList (Variable "S")(Variable "T"))
   (Inheritance (Variable "S")(Variable "T")))

but instead I get a throw.

I can also try an eta-converted version:

(define inject-eta    (List (Concept "junk") (Variable "S")(Variable "T")))
(cog-execute! (Compose f2 inject-eta))

but that also throws.

By-the-way, PutLink fails on the first example, although I just fixed that.

[linas]

OK, so pull req #1492 enables must/most of this to work with PutLink. I'm still stumped about ProjectionLink; I think you mean "injection" not "projection". Injection is a technique to start with a function that has high arity, and create a function with low arity, which seems to be what you are trying to do. So, the following works:

(use-modules (opencog) (opencog exec))

(define f3 (Lambda
   (VariableList (Variable "X") (Variable "Y") (Variable "Z"))
   (Inheritance (Variable "Y")(Variable "Z")) ))

(define inject    
   (Lambda (VariableList  (Variable "S")(Variable "T"))
      (List (Concept "junk") (Variable "S")(Variable "T"))))

(define g (Lambda (Evaluation (Variable "X") (Variable "Y"))))
(define ident (Lambda (Variable "X") (Variable "X")))  ; the identity function.
(cog-execute! (Put g (List ident (Put f3 inject)) ))

To understand what is going on, notice that f3 takes 3 arguments, while inject takes two arguments, and returns 3. Thus (cog-execute! (Put f3 inject)) returns a function that takes two arguments.

Next, (List ident (Put f3 inject)) is a cartesian product: a pair, a total of two things. Since g is expecting exactly two things, this "fits" right into g. Thus, doing the above gives:

(LambdaLink
     (VariableList
         (VariableNode "X")
         (VariableNode "S")
         (VariableNode "T"))
   (EvaluationLink
        (VariableNode "X")
        (InheritanceLink
             (VariableNode "S")
             (VariableNode "T"))))

which is the result that the ComposeLink unit test is looking for. This also works with a "bare-naked", eta-reduced form of inject viz:

(define inject    
      (List (Concept "junk") (Variable "S")(Variable "T")))

I humbly suggest that perhaps PutLink can do mostly everything you want ComposeLink to do, module my not understanding the need for ProjectionLink

[ngeiswei]

ComposeLink semantics is explained in https://wiki.opencog.org/w/ComposeLink#Semantics

In particular look at

g(f1(x1,...,xm),...,fn(x1,...,xm))

each fi typically have the same variable declaration (but I generalize that to say that the resulting vardecl just need to be their "intersection"). This is the same definition as the one used here https://en.wikipedia.org/wiki/Primitive_recursive_function.

This allows to specialize g by linking some of it's variables (I don't know if combining PutLinks allows that due to automatic alpha-conversion). Here's what I mean:

Let g be

(Lambda
  (VariableList X Y W Z)
  (And
    (Inheritance X Y)
    (Inheritance W Z)))

Question: How to turn it into

(Lambda
  (VariableList X Y Z)
  (And
    (Inheritance X Y)
    (Inheritance Y Z)))

?

In the latter W has been replaced by Y.

With ComposeLink I can do

(ComposeLink
  g
  (List
    (Lambda (VariableList X Y Z) X)   <- f1
    (Lambda (VariableList X Y Z) Y)   <- f2
    (Lambda (VariableList X Y Z) Y)   <- f3
    (Lambda (VariableList X Y Z) Z)))  <- f4

The names of the variables in f1 to f4 doesn't matter, the linkage between Y and W will be preserved no matter what. Is it still true if I use PutLink?

Now I can simplify this using ProjectLink (which implements projection, as explained here https://wiki.opencog.org/w/ProjectLink#Semantics , BTW, with the exception of https://en.wikipedia.org/wiki/Injective_function I don't know what is "Injection", I guess what you mean based on the examples and the very term, but I can't find its formal definition anywhere)

(ComposeLink
  g
  (List
    (Project 0)
    (Project 1)
    (Project 1)
    (Project 2)))

Perhaps the source of the confusion about ProjectLink is that the arity is missing, instead I should probably have defined

(Project i n)

as being equivalent to

f(x0,...xi,...,x(n-1))=xi

But I realized while implementing it that the arity would never be used (in my cases anyway), so I decided to drop it.

[linas]

OK, function composition is defined the same way the world-over; its not any different for primitive recursive functions.

The whole point of lambda calculus is that it is a model for function composition. The grand realization 100 years ago or so, was that (almost) everything in math is function composition, in the end. Church simply had the guts to push this to the extreme. So of course, composition and beta-reduction are exactly "the same thing", at this level. There's no difference.

Your question: "Can I turn g into injected form?" and the answer is, of course, "yes". Although it does exhibit a bug in my code; fixing now.

Next: ListLink in atomese is the "cartesian product": https://en.wikipedia.org/wiki/Cartesian_product so (List A B) is the same as a product of two things.

Next: (Lambda (VariableList X Y Z) X) is a function taking 3 arguments as input, and returning one.

Thus:

  (List
    (Lambda (VariableList X Y Z) X) 
    (Lambda (VariableList X Y Z) Y))

is a function taking six arguments, and returning two. It is EXACTLY the same function as

  (List
    (Lambda (VariableList X Y Z) X) 
    (Lambda (VariableList R S T) S))

Scoping in atomese works exactly the same way as scoping in all other branches of math. There's nothing magical about alpha-renaming; it's simply giving a name to an operation that everyone does subconsciously, without even thinking about it. Because its done subconsciously, its often done wrong, and that's why it's given an explicit name.

To be clear:

  (List
    (Lambda (VariableList X Y Z) X)   <- f1
    (Lambda (VariableList X Y Z) Y)   <- f2
    (Lambda (VariableList X Y Z) Y)   <- f3
    (Lambda (VariableList X Y Z) Z))  <- f4

is a function taking twelve arguments, returning 4. Your subconscious is fooling you into thinking that all those X's and Y's are the same, because you happened to write the same symbol for each. The are not; they are all different.

An injection is this: https://en.wikipedia.org/wiki/Injective_function

In certain branches of math, e.g. homology, it is extremely common to want to start with a function having, say, 6 arguments, and to somehow end up with a function having only 5, and the common way of doing this is to insert some constant (e.g. 0 or 1) for the n'th location. This is always denoted by the letter i subscript n, so that

i_k(x0, ... ,xm) = (x0, ... x_{k-1}, 0, x_k, ... x_m)

injects a zero into the k'th position. This is standard, common notation and terminology for this.

The other very common way of altering the number of arguments is to just duplicate an argument (this is what you are doing), and this goes under various names: comultiplication or coproduct or diagonal morphism https://en.wikipedia.org/wiki/Diagonal_morphism or diagonal functor https://en.wikipedia.org/wiki/Diagonal_functor -- these all take just one object, and create two of them out of it. its called a diagonal because it resembles a diagonal matrix in linear algebra: a diagonal matrix M is a matrix where M_ii = f_i and all other M_ij are zero.

When you defined your ComposeLink, you defined it with a big diagonal implicit in it. To make it explict, instead of having it be invisible, its this:

g(f1(x1,...,xm), ... ,fn(x1,...,xm)) = 

(g \circ (f1, ... , fn) \circ Delta_nm) (x1, ..., xm)

where \circ denotes function composition and Delta_nm can be visualized as the (n,m)-tensor having 1 on the diagonal, and zero everywhere else. Symbolically,

Delta_nm(x1,...,xm) = ((x1,...,xm), (x1,...,xm), ... , (x1,...,xm))  
                                ^^^ repeated n times ^^^

Recall that an ordinary m-dimensional matrix from linear algebra is just a (2,m)-tensor. a (3,m)-tensor would be a cube of numbers, and a (4,m)-tensor would be a hypercube of numbers. Visualize a hypercube in n dimensions, with m splats along each edge, and put a 1 on the (one and only unique) diagonal, and a zero elsewhere. Start with an ordinary cube: it has one diagonal running from the (111) corner to the (mmm) corner.

Diagonals are super-duper easy in lambda-calculus, the above gymnastics simplifies greatly. Here is what you are trying to do with ComposeLink. It almost works (there's a stupid bug in the code - it might be fixed by the time you read this - so git pull and recompile):

(use-modules (opencog) (opencog exec))
(define X (Variable "X"))
(define Y (Variable "Y"))
(define Z (Variable "Z"))
(define W (Variable "W"))

(define g (Lambda
  (VariableList X Y W Z)
  (And
    (Inheritance X Y)
    (Inheritance W Z))))    ;; this is the same g you define above.

(define f  (Lambda (VariableList X Y Z) (List X Y Y Z)))

(cog-execute! (Put g f))   ;; this gives what you want.

Notice that the function f takes three arguments, but returns four. It duplicates the middle argument. There are other, more complicated ways to write this, involving more mental gymnastics and diagonal injections. (The diagonal is always an injection) I will add all the gymnastic versions to the unit test when I get them all debugged.

[linas]

I now understand why you invented projection: it is to undo the diagonal. Look at https://en.wikipedia.org/wiki/Diagonal_morphism more closely, and notice that what the diagonal does, the projection un-does. If you click through on the link to "canonical projection morphism", its clear that ProjectionLink and the standard math definition for projection is the same thing, and that's good. But the reason you invented ProjectionLink was to undo the invisible diagonal in ComposeLink.

PutLink doesn't have a diagonal in it, so doesn't need projection. I suppose we could invent DiagonalLink and then we would have that (ComposeLink g f) == (PutLink g f (DiagonalLink m)) and also that (DiagonalLink m (ProjectionLink k)) would be some kind of fancy no-op. Well, not a no-op, but a shuffle or something like that.

[linas]

OK, #1494 fixes the bugs that got revealed above. This now works correctly:

(use-modules (opencog) (opencog exec))
(define X (Variable "X"))
(define Y (Variable "Y"))
(define Z (Variable "Z"))
(define W (Variable "W"))

(define g (Lambda
  (VariableList X Y W Z)
  (And
    (Inheritance X Y)
    (Inheritance W Z))))    ;; this is the same g you define above.

(define f  (Lambda (VariableList X Y Z) (List X Y Y Z)))
(cog-execute! (Put g f))   ;; this gives what you want.

(define h (List X Y Y Z))
(cog-execute! (Put g h))   ;; this also gives what you want.

This seems to be what you were trying to do with project:

(define pf
   (Lambda (VariableList X Y Z) 
      (List 
         (Select 1 (List X Y Z))
         (Select 2 (List X Y Z))
         (Select 2 (List X Y Z))
         (Select 3 (List X Y Z))
)))

The Select link doesn't exist, but if it did, it would pick out the n'th entry out of a list. Select corresponds very closely to the "standard" definition of projection. In the above, Select is a function that takes three arguments, and returns 1. The pf is then a function that takes three arguments, and returns four, and so, pf could be composed with the earlier g.

A lot of my confusion was due to the fact that the primitive-recursive crowd uses a totally bizzarro definition of multi-variate so-called "composition" which is... perhaps convenient for their purposes, but is totally not how composition is normally done. When you wrote this:

g(f1(x1,...,xm),...,fn(x1,...,xm))

I should have spotted the trouble immediately:In general, its impossible to assume f1 has the same arity as f2 has the same arity as f3 -- this is kind-of never the case. In general, f1 will take m arguments, f2 will take k arguments, f3 will take r arguments, and the concept that they all have the same arity is .. unusual, to say the least. I'm not sure where such a definition comes from, or how its useful. I can't say that I've ever spotted such a beast before. It feels very linear-algebraic, but in linear algebra, you just have matrices.

[ngeiswei]

OK, I like it!

I think it would be good to update https://wiki.opencog.org/w/ListLink to make the Cartesian Product semantics explicit. By that logic I suppose

(List (Set a1 ... an) (Set b1 ... bm))

should be equivalent to

(Set (List a1 b1) (list a1 b2) ... (List an bm))

right?

Weirder, it also follows that

(List (Set) (Set a b c))

is equivalent to

(Set)

But I don't think it would cause major problems.

Do you prefer to update the wiki yourself, or to defer to me?

I'll will start converting my code to use PutLink instead of ComposeLink and ProjectLink, then, if all go well I'll remove them.

Thanks for going into great details about it, it helped.

[linas]

By that logic I suppose

(List (Set a1 ... an) (Set b1 ... bm))

should be equivalent to

(Set (List a1 b1) (list a1 b2) ... (List an bm))

Possibly. That depends on what theory you wish to apply.

1) The idea the cartesian product distributes over (countable) sets in this way is kind-of part of the definition of the cartesian product, and its "well-known" that this gives you exactly simply-typed lambda calc and nothing more nor less. So the above is consistent with an interpretation of SetLink in lambda-calc. A famous counter-example is the tensor product, which does not allow this equivalence, and does not give you lambda-calc, but instead gives you linear logic. Atomese is not lambda-calc, we want it to be freer (as in "free theory") ...

2) You are assuming (endowing) the SetLink with the so-called "discrete topology" which is very very natural for finite sets, but is certainly not the only possible topology for finite sets. The famous counterexample is called https://en.wikipedia.org/wiki/Sierpi%C5%84ski_space Sierpiński space - given the set S = {a,b} let its topology be {{a,b}, a, 0} -- this is the statement that a is a member of S but b is not. That is (MemberLink a S) is true, but (MemberLink b S) is false.

3) For infinite sets, the discrete topology, being the finest possible, is very very sick and nasty and unusable: recall it gives things like the Banach-Tarski paradox. Your distributivity rule has a name, its called the "cylinder set topology" and commonly describes fractals (but not manifolds).

4) "Equivalence" is a "relation": recall the formal definition of "relation" and the formal definition of "equivalence relation". Just because so thing A can be converted into a B by some equivalence relation, does not mean that we always want to automatically perform that conversion every time we trip over it. Very often, the order in which such equivalence-rewrites is performed is important, and gives inequivalent results (viz "confluent" vs "strongly normalizing")

5) So, now that we are viewing "equivalence" as a kind-of rewrite-rule, where "A is equivalent to B" means that "A can be re-written as B" - we have to ask: what kinds of equivalences do we want to hard-code as C++ in the atomspace, and which ones do we want to encode as rules in the rule-engine? So far, we've been super-sloppy, sometimes coding in C++, but often punting.

6) Recall the formal definition of a "theory": (well, let me mangle it slightly) its more-or-less a set of URE rules, plus the set of all possible things that the forward chainer could ever find, in infinite runtime.

7) Recall the definition of a "free theory": https://en.wikipedia.org/wiki/Uninterpreted_function (this particular wikipedia article is a turdball. Oh well)

The "free theory" is what we would get if we took atomese, removed all of the C++-backed atoms, removed the URE, removed PLN. -- the free theory is the set of all possible atoms (FooLink (BarNode "x") (ZapNode "y")) and there is "no interpretation", no meaning, no semantics for FooLink, BarNode, ZapNode (they are "uninterpreted") and thus two different atoms are always inequivalent unless they are the same atom. There are no equivalence relations that say "A is equivalent to B" except for the trivial equivalence "A is equal to A".

As far as possible, we should strive to keep atomese "as free as possible", and only add equivalences where they seem to really make sense for some important reason. The important ones then become the C++-backed atoms that cog-execute! can run. That is, cog-execute! applies equivalences in a certain kind of order.

If an equivalence is desirable, but is not coded in C++, then it could be coded as a URE rule, and then the forward chainer applies equivalences in a certain kind of order. That is, in a certain abstract sense, the forward chainer does exactly the same thing that cog-execute! does, except more slowly. (and possibly in a different order.)

We haven't much discussed reduction order: besides lazy evaluation, there is also head-evaluation, normal evaluation, all kids of different styles of evaluation, and cog-execute! hard-codes a certain nasty ugly variant, and I have no idea which one the forward-chainer hard-codes. See, for example, Coq, which defines a number of different reduction strategies - we could/should do the same for the forward chainer.

[linas]

Closing, this won't go anywhere.