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

Subject: Re: [boost] De Bruijn Bind (alternate bind syntax) Interest?
From: Larry Evans (cppljevans_at_[hidden])
Date: 2013-06-23 11:40:40

On 09/02/10 16:08, David Sankel wrote:> 2010/9/2 David Sankel
<camior_at_[hidden]>
>
>> 2010/9/2 Dave Abrahams <dave_at_[hidden]>
>>
>> On Thu, Sep 2, 2010 at 11:57 AM, David Sankel <camior_at_[hidden]> 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).