De Bruijn Index notation

[HalosGhost]

lci is already incredibly wonderful. But, adding some support for the De Bruijn Index notation could lead to some amazing things. Below is a list of things I would love to see lci be able to do:

• provide a built-in (but still user-callable) function which would convert a function in Church notation to its De Bruijn Index notation

• provide a built-in (but still user-callable) function which would convert a function in De Bruijn Index notation to a version of the same function in Church notation

• provide a built-in (but still user-callable) function which would test two functions for α-equivalence (via De Bruijn index notation)

• perhaps leveraging the above, it may be possible to replace the final results of β-reducing any term with the first α-equivalent name in the namespace

For example (imagining that the following definition exists in the current namespace: I = \x.x;):

lci> \x.x

I
(0 reductions, 0.00s CPU)

In my opinion, this would be wonderfully useful! Thoughts?