Alpha-equivalence creates incoming link inconcistencies

[ngeiswei]

Automatic alpha-equivalence of scope links may create inconsistencies. Here's an example

scheme@(guile-user)> (define body-1 (Inheritance (Concept "A") (Variable "$X")))
scheme@(guile-user)> (define sc-1 (Scope body-1))
scheme@(guile-user)> (define ev-1 (Evaluation (Predicate "body-of") (List body-1 sc-1)))
$2 = (EvaluationLink
   (PredicateNode "body-of")
   (ListLink
      (InheritanceLink
         (ConceptNode "A")
         (VariableNode "$X")
      )
      (ScopeLink
         (InheritanceLink
            (ConceptNode "A")
            (VariableNode "$X")
         )
      )
   )
)
scheme@(guile-user)> (define body-2 (Inheritance (Concept "A") (Variable "$Y")))
scheme@(guile-user)> (define sc-2 (Scope body-2))
scheme@(guile-user)> (define ev-2 (Evaluation (Predicate "body-of") (List body-2 sc-2)))
scheme@(guile-user)> ev-2
$4 = (EvaluationLink
   (PredicateNode "body-of")
   (ListLink
      (InheritanceLink
         (ConceptNode "A")
         (VariableNode "$Y")
      )
      (ScopeLink
         (InheritanceLink
            (ConceptNode "A")
            (VariableNode "$X")
         )
      )
   )
)

So it creates a scope, and an evaluation linking the scope to its body, then do the same with an alpha-equivalent scope. Alpha-conversion transforms the second evaluation.

[ngeiswei]

I should add that it is a real world issue for me ATM and that I need to come to an agreement on how to fix this soon.

1. But should atoms within a scope be allowed to have incomings outside of the scope to begin with?
2. If so, should we propagate alpha-conversion to these incomings?
3. What about QuoteLinks?

It seems to me, without having thought of it too deeply that we want to propagate alpha-conversion to the incomings, except if they are quoted. In case they are both quoted and unquoted, then we must keep an un-alpha-converted scope for the quoting incomings.

[ngeiswei]

Let me explain my problem, an inference tree is a scope link. A premise within that inference tree is an atom within that scope link. I need to point to this atom to tell another process that this inference tree has been expanded from this premise. Instead of pointing to it I could indicate its index according to some traversal enumeration, but I prefer to point to it cause then I have direct access to the premise (which allows to easily check whether it follows some pattern, etc).

[linas]

I don't know quite what to say. Off-hand, I don't see any problem, probably because I don't understand what you are trying to say, here.

Syntactically, sc-1 looks just fine, and its clearly identical to sc-2. What is the semantics of sc-1 supposed to be? What does it even mean? How should I think about it? How are you thinking about it?

Semantically, its plain-as-day that the semantics of ev-1 and ev-2 are identical, even though I don't have a clue of what the semantics is supposed to be.

From this and earlier conversations, its clear that you really really like to use scope links for some reason that I cannot make out. Are you sure you should be using them? Are you sure that you don't want to use FreeLink instead? Maybe FreeLink does what you want?

Scope's were meant to be an abstract base class for ForAllLink, ThereExistsLink, LambdaLink, PatternLink all of which have wildly different semantics. ScopeLnk was never meant to be used "naked", precisely because the naked ScopeLink doesn't have any semantics. Its like an abstract base-class in C++, which can't be used because it has undefined virtual methods. The ScopeLink has undefined semantics, other than providing a platform for alpha conversion. Its doesn't do anything else.

If you don't want alpha conversion, then don't use ScopeLink. If you do want alpha conversion, then use it.

If you want something else... don't use ScopeLink. Use the link type that does what you want, or invent one as needed. Perhaps you actually want to use FreeLink instead?

[linas]

I quote:

// A FreeLink is any kind of link that might have free variables in it.
// The FreeLink exists for one purpose: to make visible/explicit all of
// free variables in the link. The primary user is the pattern matcher.
// That is, envision the FreeLink as being at the top of a tree, and
// somewhere in that tree, there might be VariableNodes.  The C++ class
// for this link records the names of those variables, in order of
// traversal.  The goal here is to simply know these variables, so that,
// at the time of evaluation or execution, they are easily located.
//
// The variables are necessarily free: they do NOT have type
// declarations or restrictions associated with them.  This is in sharp
// contrast to ScopeLink, which binds variables by scoping them, and
// then forcing type restrictions to them.
//
// FreeLinks may be open or closed; they are closed terms if they
// have no free variables in them.
//

[linas]

Copying from http://wiki.opencog.org/w/FreeLink

A FreeLink is a type of Link that tracks the locations of VariableNodes in it. It serves as a base type for several link types, including EvaluationLink, DeleteLink, StateLink and FunctionLink. Its primary usefulness is in the C++ implementation of the atomspace, where it serves to cache (memoize) variable locations, for rapid beta-reduction and evaluation/execution.

Note that free variables cannot be typed; that is, it is not legal to use a VariableList to explicitly declare a variable. If you want to declare variables, you need to use a LambdaLink instead.

Note that the implementation correctly handles both the QuoteLink, and any embedded LambdaLinks. That is, quoted variables are not variables at all, they're constants, and so cannot be considered to be "free". Likewise, and bound variables are not free, so any bound variables appearing underneath a nested LambdaLink will not be considered. One the other hand, and free variables inside a nested LambdaLink will be discovered.

[ngeiswei]

@linas in my real problem I use BindLink. The ScopeLink is just to highlight the problem, any type inheriting ScopeLink share this issue.

Do you see that in ev-2, as processed after alpha-conversion, the first argument no longer match the body of the scope? That is contrary to what the user put, it breaks the semantics that the user wanted to express.

[linas]

Do you see that in ev-2, as processed after alpha-conversion, the first argument no longer match the body of the scope?

No. That sentence is built on a false assumption. It doesn't even make sense. There never was a match to begin with. You think that there was a match in ev-1, but there never was one there, either, its purely imagined.

That is contrary to what the user put,

User error.

it breaks the semantics that user wanted to express.

I don't understand what semantics the user wanted to give the thing.

[linas]

Instead of thinking of BindLink, think of integrals: "the body of $ \int_0^\infty f(x) dx $ is f(x)" That is a true statement. But the following is also true: "the body of $ \int_0^\infty f(x) dx $ is f(z)" -- both statements say exactly the same thing, and the x inside ithe integral sign has nothing to do with the x/z outside the integral sign. They are two distinct, unconnected variables. The one inside the integral is scoped. The one outside of the integral is free.

[ngeiswei]

You are saying that body-1 as outgoing argument of sc-1 is different than body-1 as outgoing argument of ev-1. Yeah, I agree with that. The semantics was wrong to begin with. But then how to refer to an atom wrapped in a scope (other than counting its position according to some traversal order)?

[linas]

how to refer to an atom wrapped in a scope

Naively I'd say: you cannot, you must not, you are not supposed to, by definition. Its scoped. Scoping intentionally hides or masks or prevents such references.

Why do you want to reference it?

[linas]

I mean -- even in C++ code, you should not even be "counting its position in some traversal order" -- that seems to be breaking the rules, the definition.

I'm guessing you have a perfectly valid reason for wanting to reference it... why? p.s. its late here I'm going to bed .... will continue tomorrow am.

[linas]

are you trying to do some locus solum style rewriting? meta-rewriting?

[ngeiswei]

I suppose, in a way.

Given an inference tree, a BindLink, I can produce another one by expanding some of its leaf (in this context a premise). This is already coded, in C++, that is how the backward chainer works.

When the backward chainer runs, it records all its expansions in an atomspace, these expansions look like

expand((A, L, R), B)

where A is an inference tree (a BindLink), L is a leaf (a premise) of A, R is a PLN rule, and B is the produced inference tree.

Then a cognitive agent, a meta-learner, go through these expansions to learn control rules to more efficiently guide the backward chainer. It links back to the issue as L is an atom within the scope link (the BindLink) A. The meta-learner needs to be able to open up A, see L and use that to figure out predictive patterns.

[ngeiswei]

If you want to understand more what I'm doing you may read this post http://blog.opencog.org/2017/10/14/inference-meta-learning-part-i/ though I don't think you need to read it to get the issue, you already have.

[linas]

I'm still struggling to understand. However, how about this: instead of storing the BindLink as a whole, how about unpacking it immediately: storing just its variable decl, the body, the conclusion? Just store them in a ListLink? Do you need some of the c++ methods on the BindLink? If I recall, almost all of these are protected methods, so you wouldn't have access to them anyway...

[ngeiswei]

That's a good suggestion. That is actually what I'm doing at the C++ code level (I mean in the backward chainer code). I might do that here too. Thanks.

[ngeiswei]

I can get away without fixing this for now, but I think I'll experiment with QuoteBindLink once I have to.