Behavior of Term.abstract with DB

[robblanco]

Suppose a term g DB(1) ?X with g: i -> i -> i and ?X : i. My intuition and the expectation set by the documentation in Term is that an operation like abstract "?X" ity (g DB(1) ?X) will yield x\ g DB(2) x, but I have seen this call capture DB's indiscriminately, resulting in a term of the form x\ g x x, which the code seems to corroborate.

If this is the desired behavior, I think it should be clarified somewhere. However, doesn't this mean that working with abstractions absolutely requires falling back to painstaking work with DB indexes, exclusively?

Edit: corrected typo in DB indexes of example, in bold.

[chaudhuri]

I just went over the function and its uses and I think it is doing the "correct" thing, as I told you in person earlier. The comment needs to be updated.

[robblanco]

I have taken a look at the code. The problem occurs in those DB subterms that the recursive function does not see as protected by a binder. For example:

abstract "X" ty (`1 (g (y\ h `1 X))) -> x\ `1 (g (y\ h `1 `2) -> x\ x (g (y\ y x))

So there is a capture at the top that was not envisioned by the method. I would expect these "unprotected DBs" to be incremented to account for the new lambda (if this is allowed, the method needs to be corrected). If it is not allowed, it should produce an error or risk insidious changes.

My argument in favor of the correction: if this sort of clean symbolic abstraction is ruled out, term manipulation must rely on DB arithmetic, which is cumbersome and more error prone. I would much rather know that I can work freely with variables inside a term and abstract them out safely later.

Edit: fixed typo.

[chaudhuri]

I agree with your proposal.

[robblanco]

Shall I make the changes in a local branch? I think this would involve only incrementing DB indexes until we descend inside a Lam node, below which DB's are left untouched, as they are now. abstract is only used in a couple of places in the code, so it should be easy to test.

[chaudhuri]

Yes, try it and submit a PR. Thanks.

[robblanco]

See #83. This doesn't break any tests, although the test case that would exercise this new functionality also doesn't exactly fit in any of the existing sub-categories, I think.

On a side note, it seems funny that the public abstract passes the initial index 1 to the local abstract. I would consider this part of the initial call to aux, as I have done with the new parameter.

Also noteworthy is the fact that the type parameter, as well as the term as a parameter for the tester, are not used at all.

Edit: re-worded this to clarify no new tests are included in the branch (yet?).

[robblanco]

I just added the example above as a test.

[chaudhuri]

Merged. Thanks.