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?
lciis 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 seelcibe 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;):In my opinion, this would be wonderfully useful! Thoughts?