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

## Basic Bijective Godel Encodings

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

## Omega Categories Made Easy

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

## Program Synthesis Specification

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]

## My (mis)adventures With Algorithmic Machine Learning

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]