Approximating Digital Functions Iteration Sums Products A Quadratic Product Recursive Types and Recursion Quicksort, First Pass Defunctionalization Final Quicksort Final Thoughts [Read More]

ℕ ≅ ℕ × ℕ ℕ ≅ ℕ + ℕ Initial Algebras Initial Algebras Extras Lambda Expressions Peano Expressions Sorted Trees Trees of Bounded Height Final Thoughts [Read More]

A few years ago, a new proof theory called CaTT was described in the paper A Type-Theoretical Definition of Weak ω-Categories [Read More]

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... [Read More]

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 [Read More]