Math and Science from an Extensional Perspective
About a year ago, I had an idea for a relational programming language. I created a simple prototype for it back then, but it was too inefficient for interesting work. Recently, I finished a version of it which is several hundred times faster and more memory efficient. In this post,...
About four months ago, my dad came to my home with a dog in tow. I had met the dog before, when it was a young puppy, but not for over a year. He had a beautiful, iridescent, brown and gray coat that looked a bit purplish in the right...
I’ve talked a lot about pairing functions on this blog. I’ve tried using them in a bunch of different projects, but I’ve frequently made the observation that they are often unexpectedly inefficient. As an example, the simplest paring function is just the bit-interleaving function which pairs two numbers by interleaving...
In an earlier post, I mentioned a potential project where I’d talk about, among other things, logic programming within the lambda calculus a la MiniKanren. As part of that, I’ve started seriously considering the nature of logic programming. MiniKanren takes a very opinionated approach to the subject. Rather than having...
My viewpoint on calculus, specifically differentiation, has changed rather radically recently. I learned about differential forms and how to manipulate them algebraically. They have the following properties; 𝕕c = 0 where c is a constant 𝕕(x + y) = 𝕕x + 𝕕y 𝕕(x y) = 𝕕x y + x 𝕕y...
This post will be a relatively short note on a simple self-interpreter for the lambda calculus I recently made. I’ve been thinking of making an extensive work, perhaps a book, on programming in the lambda calculus. As part of that, I was looking into self-interpretation. If one wants to do...
Approximating Digital Functions Iteration Sums Products A Quadratic Product Recursive Types and Recursion Quicksort, First Pass Defunctionalization Final Quicksort Final Thoughts Introduction I’ve been a bit obsessed with continuous computation recently. Both in the sense of analog computing and the sense of coinduction. I want to write a post about...
ℕ ≅ ℕ × ℕ ℕ ≅ ℕ + ℕ Initial Algebras Initial Algebras Extras Lambda Expressions Peano Expressions Sorted Trees Trees of Bounded Height Final Thoughts Introduction I’ve been researching methods for generating data the past few months and, as part of that, I looked into Godel encodings. In...
A few years ago, a new proof theory called CaTT was described in the paper A Type-Theoretical Definition of Weak ω-Categories It contains what is, in retrospect, the simplest and easiest to reason about presentation of ω-categories anywhere I’m aware of. ω-categories are a somewhat esoteric concept, infinite-dimensional algebraic structures...
This post will be a small note on program specifications. One of my long-term goals is that of a bootstrapping program synthesizer. That is, a program synthesizer that can synthesize better program synthesizers. One important step is specifying, formally, what this means. I’ve recently figured out how to properly formulate...
Introduction Why Not Use Ordinary Compression? Methods for Approximating Kolmogorov Complexity Approximating Conditional Kolmogorov Complexity using CTM Block Decomposition Spit-balling ways to improve DBM and CTM Algorithmic Loss Algorithmic Optimization Final Thoughts Introduction I’ve been researching, for quite some time, the prospect of machine learning on a wider variety of...
I’ve known for a while that dependent types can be defined as initial and final dialgebras. This is a somewhat obscure fact; but an important generalization of the more commonly referenced fact that non-dependent types are initial and final (co)algebras of specific endofunctors. The only thorough source of this fact...
In this post, I will show a nice, clean, organized, schematic, and theoretically well-justified approach to sorting. I’ll implement it in Python because of my target audience, but there’s no significance to the choice beyond that. I’m going to describe and implement Merge Sort and Quicksort via hylomorphisms. That may...
This post consists of some notes on lambda encodings I made a while ago. I figured I’d put them here, since it’s more visible and easier for me to find. The free monoid monad is left adjoint to the forgetful functor (as are all free things). We can define the...
I read a rather fascinating paper recently called “Implicative algebras: a new foundation for realizability and forcing”. I thought this was a good paper, and I need content for this blog, so I figure giving a summary of it would be a good idea. The paper itself, from the very...