Wouldn't the binary lambda calculus (BLC) encoding also suffice as a (relatively) compact map to these functions? To convert the encoding to a bigint, you'd just need to prepend a 1 and convert the binary string to decimal as normal.
I can’t speak to the practical nature of my encoding, but I wanted it to be air tight and to only encode closed terms. For my latest scheme, 0 maps to the identity function and 1 maps to the identity function calling itself.
I just got caught up in the idea of compactly representing all sorts of recursive data types as integers to create an airtight bijection.
That took me down the rabbit hole where I wanted to explore how I could use balanced pairing functions to map to data types instances restricted by constraints. For example, maybe you want to map the integers to the set of terms that can be simply typed, or some other constraint.
The way I see it is if you can come up with ways to declaratively and efficiently select subsets of these bijections, one could reduce some problems to brute force, by shrinking the search space. (Something the Alloy modeling language does)
That’s when I came across this repo and associated paper titled Fair Enumeration Combinators and learned about the SciFe library Scala library.
https://github.com/ikuraj/SciFe
But practically speaking, I suspect you’re right about BLC being a good practical candidate for an index.
Again, great post!