In my previous post, I described an approach for extending multi-stage programming (MSP) to infinity and beyond. We start with a simple computing “machine” M such as the lambda calculus. Each machine M[a] has a successor machine M[a+1] which is capable of building and reasoning about programs from M[a], yielding towers of nested machines. From there, we note that MSP itself can’t be implemented in any such finite M[n], but must exist in some limit machine M[ω], yielding transfinite towers of machines M[a] for each ordinal a.
In Part 1 I attempted to give some intuition for the process of iterating reflection to infinity and beyond: any time we can iterate reflection infinitely, we can reflect on this infinite process. In this post, I’ll be formalizing this notion in a simple programming language, and I recommend reading that last post before this one. Code is linked at the bottom.
My last two posts were about ordinals and pure lists, and they got a combined whopping 11 claps, so I’m selling out and writing a post about both. In particular, this post is about a data structure I discovered for lists of transfinite length. A repo is linked at the bottom.
Let’s say we’ve defined a function f from ordinals to ordinals and want to plot it like we might plot a function from integers to integers. We want to line up our ordinals on the x- and y-axes, and plot a point at (x, f(x)) for each ordinal x. Well where should we actually put those ordinals on the axes? This simple question is the topic of this post.