This is a microblog, where I leave mostly banal thoughts and research notes. RSS and Atom feed.

• Sep 12, 2026

  Consider $\text{LARP}$, the set of all languages decidable by LARPing. Consider the GPT-6 Astra oracle $\alpha$. We posit that $\text{LARP}^\alpha$, the languages decidable by LARPing equipped with the Astra oracle, is equal to the universal set $\Omega$. That is, there is no limit to the larp.

  Full text.

• General Recursive Functions

  Sep 09, 2026

  Definition

  A partial function from is a function for some . We write .

  For we write to mean and to mean . “Converges,” “Diverges.”

  Abuse of Notation

  If then we write .

  , .

  Definition

  If we say is total. Write (like usual).

  If we say if

  (Symbol soup for they agree on convergence, and value if converges. Funext for partials.)

  Recursive partial functions

  Some -ary partial functions are “clearly” effectively calculable (you could imagine a computer doing these easily).

  • Composition: if we already have two effectively calculable programs (functions), then composing them is trivial.

  • For , let be . Let be . ( for successor.)

  • For , let be the “-th projection”

  • For , , , let

    Here we say is defined by substitution from .

  Let be the family of partial functions . An additional rule:

  • Recursion: let , . Define by and .

    More generally, for , , , define . For , take , and .

    Here we say that is defined by primitive recursion from and . If , then .

  Example

  is in .

  Proof. Use primitive recursion,

  ⁠ 

  In the proof above, explicitly speaking, we chose . The choice of is also clear. Here , so given , a suitable choice is , since .

  Beyond just satisfying the symbolic constraints we attempt to give an intuitive explanation for why this is a clear choice. We should interpret the -ary function as the familiar for loop. The first parameters constitute the vector , and the argument can be seen as the loop index . We should view as some immutable auxiliary data that the loop can access throughout its iterations. Indeed, notice that is passed unchanged throughout every recursive step of , , and .

  The -ary function can be interpreted as an initial value at , and the -ary function is the loop body. The argument of is some value passed down from the previous iteration of the loop. The way I think about it is that at index of the loop, which is , we can pass on some value to the next iteration . We can therefore access the value passed to us by the previous iteration , which is why .

  Once we digest primitive recursion from the for loop perspective, it becomes more palatable as a “primitive” form of recursion. Essentially, instead of a recursive function (in the colloquial sense) being able to arbitrarily call itself in its body, a primitive recursive function can only obtain the value of in its body, and the base case is guaranteed to be when . In this view, and are merely auxiliary functions to make the formalism work out.

  Now the choice of is clear. For , we just need a for loop to add to , times. We don’t need the initial input , and we don’t need the index . So we use to choose the prior value of the “loop,” and then we add one to it (via the successor function). The initial value of the loop is clearly itself. Now the function defined by primitive recursion can be interpreted as a for loop with an accumulator variable initialized at , at each following iteration adding to the accumulator, running for a total of times. (The first iteration where is initialized is interpreted as , so the loop adds one to a total of times, computing in the end.)

  Primitive recursion for partials: for partial functions , , the function defined by primitive recursion from and is given by

  Just means that when working with partials we need to take care of convergence.

  • Let , . Define by

    If , we’ll put . Notation: .

    We say that is defined from by minimization.

    In the partial case, for , define by

  Definition

  Call a family of partial functions recursively closed if it satisfies all the previous construction axioms.

  Definition

  If , we say is recursive.

  Equivalently, is recursive iff it can be defined from , , , using finitely many applications of substitution, primitive recursion, and minimization.

  Non-mathematical claim: recursive functions are effectively calculable. If you believe in the Church-Turing Thesis, then recursive functions are exactly the functions which can be computed by effective methods (e.g. Python-computation).

  Full text.
• Sep 09, 2026

  I finally set up the microblogging system. Will be putting random things here.

  Full text.

• Deriving the Y-Combinator

  Feb 28, 2026

  Not that Y-combinator.

  Haskell Curry’s “paradoxical” -combinator gives a fixed-point for every single term in the untyped -calculus. (Recall that in the untyped -calculus, as there is no notion of a term having type “function” or “variable,” every term may be regarded being allowed to have terms applied to it, which is in fact the crux of the derivation.)

  Notions

  For our purposes, our untyped -calculus will be a standard -theory, in the equational theoretic sense, in that it consists of the standard rules of the lambda calculus with the -conversion rule.

  By the way

  This tidbit is not really necessary or too interesting, but I thought I’d point it out. The -conversion rule is often called -reduction, but there’s a semantic distinction here. -conversion is defined by a binary relation called , which relates

  Here, is not a distinct term in the lambda calculus but represents substituting all free occurrences of with in the term , while avoiding unintended capture of free variables via -conversion.

  For any relation , we can define the compatible closure, an induced relation denoted . We call it the -reduction. It’s simply the relation itself, along with relating if (reduction on the left), a similar rule for reduction on the right, and reduction under abstraction.

  When studying -calculi, we are usually interested in the -reduction.

  A lambda abstraction is a term of the form . A combinator is a lambda abstraction with no free terms.

  A fixed point of a term is simply any term such that . Additionally, if there exists a combinator such that for any terms and we have , i.e. is a fixed point of , then we say is a fixed-point combinator.

  The Y

  We proceed to derive the -combinator as the proof of this theorem.

  Theorem

  Every term in the simply untyped -calculus has a fixed point, moreover, we can find an explicit formula for such fixed points.

  Let be any term. We basically are trying to solve for some term in the equation

  Since appears in both sides, and it is not clear (nor true) that every term has the same fixed point, it’s pretty obvious our solution is going to contain the term itself . Therefore, we should search for a fixed-point combinator. We can first naively try the combinator that is the term itself. Let be arbitrary (free) and instead write

  This doesn’t actually help us solve the problem at all, but it gives a hint, namely, we see . If only the left side was , then we would be done!

  The key trick is to use self-reference. Write the combinator that gives

  and see that . A fixed point! Now what could be? obviously works. Now just write out and bind and you recover the classical -combinator!

  🎊 🎊 🎊

  Full text.

• The Eckmann-Hilton Argument

  Feb 13, 2026

  The Eckmann-Hilton argument causes many seemingly more complex structures to collapse into simpler ones. For instance, the fundamental group of any topological space is always Abelian.

  Theorem

  Let be a set which is a magma under two unital binary operations, and . Suppose one is a homomorphism for the other. Then and moreover is a commutative monoid under these operations.

  We usually speak of homomorphisms as unary functions compatible with a structure, e.g. with . Binary homomorphisms look like this:

  It seems strange that the and “swap” positions, but this is the binary analog to the notion of the homomorphism being a compatible operation, such that times plus times is the same as plus first times plus .

  By the way

  A set with a unital binary operation is called a unital magma. Unital means that the operation has a unique left and right identity, and a simple argument shows that these identities in fact coincide.

  Proof. The key step is to show that the identities of both operations coincide. Let and be the identities of and respectively, then

  The rest of the proof should follow easily. The setup

  gives that and similar arguments give associativity and commutativity, which show that under the operations is indeed a commutative monoid and concludes the proof. ⁠ 

  Another consequence of Eckmann-Hilton is that a monoid object in the category of monoids Mon is a commutative monoid, in fact this can be taken as a category theoretic formulation of the argument itself.

  Full text.