Re: [boost] De Bruijn Bind (alternate bind syntax) Interest?

On Sun, Jun 23, 2013 at 9:40 AM, Larry Evans wrote:

On 09/02/10 16:08, David Sankel wrote:> 2010/9/2 David Sankel

...

...

2010/9/2 Dave Abrahams

On Thu, Sep 2, 2010 at 11:57 AM, David Sankel wrote:

...

...

Hello all,

I've been working on an alternate bind syntax based on De Bruijn indices[1]. The syntax is very simple, yet the terms are very powerful.

Here is an example of a function const that takes in an argument c and returns another function that, for all input, returns c:

//λx.λy.x = λλ1 with De Bruijn indices.

Not according to the page you linked below. What am I missing?

[1] http://en.wikipedia.org/wiki/De_Bruijn_index

Sorry about that. The wikipedia page uses 1-indexed indices where I'm

using

...

...

0-indexed indices. So, increment 1 on all my examples to get the wikipedia syntax.

I'm beginning to think it is better to use 1-indexing instead of 0-indexing all around. It will be both compatible with the Wikipedia page and familiar to boost bind/lambda users.

Funny thing is, I started with 1-indexing but changed it to 0-indexing for the fallacious reasoning of the arrrrgh function that Dave A mentioned.

Hi David,

I looked at the web page mentioned in your first post to this thread and could not understand the flip example:

For flip, I'm introducing subscripts on abstractions (λ) to indicate the number of arguments. For the variables (1,2,etc.) I use a subscript to indicate which argument of the abstraction it refers to.

flip = λx.λ(y,z).x(z,y) = λ₁λ₂1(1₁, 2₀)

which seems to have a 0 for the subscript of 2. and 1 for the subscript of 1. That's consistent with the argument indices starting at 0 (1₁ corresponds z {the 2nd argument in the argument list, (z,y)}, and 2₀ corresponds to y {the 1st argument in the argument list, (z,y)}); however, subscrited numbers should be the same since both y and z are bound by the same lamba, the nearest one corresponding to number 1. Hence, shouldn't the above be:

flip = λx.λ(y,z).x(z,y) = λ₁λ₂2₀(1₁, 1₀)

? Also, since the abstraction indices seem to start at 1, shouldn't the argument indices also start at 1? I think that would make the notation more consistent, and would result in:

flip = λx.λ(y,z).x(z,y) = λ₁λ₂2_1(1_2, 1_1)

(where a subscript of I have been replaced with _I).

You are correct on both accounts. I fixed the README at de-bruijn-bind's new home on github. https://github.com/camio/de-bruijn-bind Thanks for the bug report! -- David