3 ms·
Very possible. It just feels like something from that general area, and I wanted to point it out. I played around with fitting this in to the Curry-Howard corr
by colah3 11y ago
Very possible. It just feels like something from that general area, and I wanted to point it out.
I played around with fitting this in to the Curry-Howard correspondence. For a moment, let's set aside neural networks and just talk about the probability distributions they operate on.
In Curry-Howard, one interprets values of a type as proofs of a theorem. Perhaps we could similarly interpret a samples of a distribution as verifying the distribution. This might lead to a kind of fuzzy logic version of Curry-Howard.
I'm not sure if this actually works or can be formalized -- I've only put a tiny bit of thought into it.
- tel 11y agoI've been idly chasing that idea for some time. There's some great literature out there on categories of distributions and (conditional) random variables as arrows between them. That would be a good place to start looking more deeply! (God I wish I had the time to look into this myself!)
- eli_gottlieb 11y agoThere are some linguistics papers going into a notion of probabilistic type theory. It's definitely an interesting area to think about. After all, Homotopy Type Theory has been teaching us that types are spaces, with topological structure. So hypothetically, how would you construct probability measures over those spaces? Could you then take points/proofs/programs as samples? What would the samples tell you about the overall measure? What would it all mean? Well, the probability monad already gives us a way to compute with distributions, and thus do probabilistic programming, but I'm not sure that really tells us anything type-theoretical, since the distributions are all over preexisting data types.