3 ms·

I’m glad I came across someone else who’s interested in the idea of having a large compendium of well tested functions. I’ve been tinkering with an idea where

by steego 3y ago

I’m glad I came across someone else who’s interested in the idea of having a large compendium of well tested functions. I’ve been tinkering with an idea where we could compactly map the set of these functions to the set of integers so they’re enumerable in such a way that small integers always correspond with small functions. https://gist.github.com/sgoguen/46200419194eb29b82079b0804e58c34 https://gist.github.com/sgoguen/46200419194eb29b82079b0804e5... A few years ago, I read a paper by Matthew Szudzik about the Rosenberg Strong pairing function and how one could use it to enumerate instances of binary trees such that you will never produce a tree of N+1 level until you’ve exhausted all trees of N. Relating it to Unison, I always thought encoding to big integers might be an interesting complement their big idea.

marvinborner 3y ago
Fascinating. I also like the idea of such a compendium. 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.
- steego 3y ago
  Honestly, I’ve been meaning to check out BLC encoding some and I really appreciate you posting this. It’s a great read! 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 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!
  - marvinborner 3y ago
    Thanks for the great references! I must say that I had never thought of such enumeration before. I'll be thinking about its potential use for a while.

by steego 3y ago

marvinborner 3y ago

Fascinating. I also like the idea of such a compendium. 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.

steego 3y ago
Honestly, I’ve been meaning to check out BLC encoding some and I really appreciate you posting this. It’s a great read! 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 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!
- marvinborner 3y ago
  Thanks for the great references! I must say that I had never thought of such enumeration before. I'll be thinking about its potential use for a while.