Here’s a surprising result. Any program that transforms source code must have an input that behaves the same before and after being transformed. In other words, for this input, called a fixed point, the input and output programs behave exactly the same way.
Sometimes fixed points are easy to find. The code console.log("hello") is an obvious fixed point of a transformation that swaps the characters ‘a’ and ‘z’:
const swapAandZ = (input) => input.replace(/[az]/g, c => c === 'a' ? 'z' : 'a')
const input: string = 'console.log("hello")'
eval(input) === eval(swapAandZ(input))
Some are slightly harder; can you think of a fixed point of “append the source to itself”?
It turns out that while true {...} (or the empty program) are both fixed points.
const double = (source: string) => source + source
const input = "while (true) {console.log('loop');} "
eval(input)
eval(double(input))
But some examples are extremely non-obvious. Can you think of a fixed point of “hash the source and execute that hash”? The program would need to behave exactly the same hashed and unhashed.
const hash = (source: string) => createHash('sha256').update(source).digest('hex');
const input = "some crazy program"
But we’ll prove that in general, any transformation, no matter how crazy, must have a fixed point.
const transform: (source: string) => string;
const input: string;
eval(input) === eval(transform(input))
The technique we’ll use to prove this remarkable truth is diagonalization. To warm up to the technique, we’ll start with two simple examples: the proof that there are more reals than natural numbers, and a proof that a seemingly powerful class of functions, the primitive recursive functions, can’t be complete.
We’ll use that newfound expertise with diagonalization to show the above result, that all code transformation programs have a fixed point. This result is called Rogers’s Theorem.
Rogers’s theorem will then help us understand a terse and opaque piece of math called the Diagonal Lemma. We’ll close by using the Diagonal Lemma for a pair of excellent proofs of Gödel’s Incompleteness Theorem (all theories must be either incomplete or inconsistent) and Tarski’s Undefinability of Truth (theories cannot define an internal notion of truth).
The Diagonalization Trilemma
Diagonalization. Let’s say you have an “evaluation” function f:X×X→Y. You can think of f(3)(5) as selecting the 3rd object from a long list of objects, and evaluating it on 5. [0]
Let’s say you also have a δ:Y→Y with no fixed point. You can think of δ as a “give me something different” function: it changes every y into a different y.
Then there exists a function g:X→Y that isn’t equal to f(k) for any k. In other words, there’s at least one new object g that isn’t equal to f(3) or f(55) or f(574), or any other object f(x) in the original list of objects. (Note that f(55) and g are both functions representing objects.)
Proof. Take g(x) as δ(f(x)(x)). For any k, g=f(k), since g(k)=f(k)(k). ■
Spelling out the proof, if you’re concerned that maybe g=f(234), you can check that at g and f(234) differ at index 234: g(234)=f(234)(234). That’s because g(234) does equal δ(f(234)(234)), which is different from f(234)(234) because δ is the “give me something different” function.
The most important part of this proof is that it establishes a crucial trilemma, which we’ll use for the rest of this post.
Trilemma. For all sets X and Y with a function f:X×X→Y, and a function δ:Y→Y, at least one of the following three things must be true:
- δ:Y→Y has a fixed point.
- There exists some g:X→Y which isn’t found in f(n) for n∈N, but g is obviously the right kind of object, so the list of objects f(n) must not be exhaustive.
- There exists some g:X→Y which isn’t found in f(n) for n∈N, but f(n) obviously lists all the possible objects, so g must actually be a new and different kind of object.
Example: Primitive Recursion
The first objects we’ll look at are the primitive recursive functions. Primitive recursive functions are all the functions made of combinations five functional building blocks: z,s,p,c and ρ. Don’t worry if you haven’t seen them before. The upshot is that you can easily list them, numbering them sequentially:
1 => z() // zero function
2 => s() // +1 function
3 => p()
...
372 => c(s, z) // composition of 0 and +1 (1)
373 => c(s, s) // composition of +1 and +1 (+2)
...
We’ll choose f(i)(j) as the evaluation function, which takes the ith primitive recursive function and computes it on j. For example, evaluating the 373rd function at the value 3:
f(373, 3) => c(s, s)(3) => s(s(3)) => 3 + 1 + 1 => 5
We can easily build a function δ(x)=x+1 that has no fixed point.
So we consult our trilemma, and decide that either (1) δ is broken, (2) the list f(i) isn’t complete, or (3) g is a new kind of object.
δ has no fixed point, and f(n) obviously enumerates all the primitive recursive functions (by definition). So it must be that g(i)=δ(f(i)(i)) is a new kind of object: a non-primitive-recursive (but computable) function.
This might surprise you if you’ve only played with primitive recursive functions for a little bit: they can compute functions like plus, times, isPrime, nthPrime, ifelse, and more. But it turns out that they aren’t Turing complete, since they can’t simulate the eval function.
Example: Reals and Naturals
You might recognize the name diagonalization from a proof you saw in math class. Georg Cantor famously used diagonalization to prove that there are more real numbers than natural numbers. In our trilemma framing, the argument goes like this.
Start with a list of rational numbers.
1 => 0.139042986720983745...
2 => 0.349857294587293845...
3 => 0.239841509204872018...
Our evaluation function f(i)(j) takes the ith real number and then gets its jth decimal digit:
f(3)(3) => 0.23[9]841509204872018... => 9
We can build a function delta = (x) => x == 1 ? 2 : 1 which maps everything (except 1) to 1, and then sends 1 to 2. It definitely has no fixed point.
We find that we’ve eliminated two options from our trilemma. δ has no fixed point. Our new g is definitely a real number, since we can get its decimal digit at any location: the first three are 0.211.... So then it must be (2) to blame–our original list of real numbers couldn’t have been exhaustive.
And so we see that there were more reals than we could list countably.
Example: Church-Turing & Rogers’ Theorem
This time we’re going to list all the JavaScript programs, again alphabetically:
1 => eval('a')
2 => eval('b')
3 => eval('c')
...
10348423 => eval('x => x + x')
Predictably, our evaluation function f(i)(j) takes the ith program in the list and runs it on the input j.
f(10348423)(1) => eval('x => x + x')((eval('a')) => 'aa'
We’re going to use delta = (x) => x + " + 1". Recall that δ operates on the source, so for example
delta(f(10348423)(1)) // => eval('x => x + x')((eval('a')) + 1 => 'aa' + 1 => 'aa1'
But something seems wrong here. Our argument above says that either:
- δ has a fixed point. It doesn’t, right?
- Our list of JavaScript programs isn’t exhaustive. But surely we’ll eventually print out even the longest of JavaScript programs by iterating alphabetically?
- Our newly manufactured JavaScript program, g, has no string representation. But surely every JavaScript program is representable by a string?
Do you see the issue? It turns out that our δ does have a fixed point. In particular, eval("while (true) {}") is a fixed point of δ. If your program loops forever, and you add one to the result, it still loops forever.
Not only that, but all viable δs share this flaw. To build the “change that output” program δ, you need to know whether your original program halts or not. And in general, you can’t know whether it halts or loops, so you can’t build a good δ. [1]
This constitutes a somewhat shocking proof that it’s impossible to build a function δ that takes any program and modifies it to produce a different result. In other words, all programs mapping functions to functions have a fixed point. This result is called Rogers’s Theorem.
There’s a nice immediate corollary: any language allows you either solve the halting problem or build an interpreter for itself. JavaScript allows interpreters but not halting-solvers. Primitive recursive functions allow halting-solvers (all P.R. functions halt), but can’t build their own interpreters. These correspond to the (1) and (3) branches of the trilemma respectively.
We’ve just seen that all programs that map programs to other programs have a fixed point. Next, we’re going to see a very similar result, but this time applied to mathematical theorems. It’s wrapped up in an opaque piece of math called the Diagonal Lemma. But once we understand the Diagonal Lemma, it opens the door to amazingly short demonstrations of Godel’s Theorem and Tarski’s Theorem.
Let’s say you’re working in some proof system, which is basically some laws (“axioms”) plus some deductive rules. Call that system T.
Give me a statement A(x). Then T can prove that there exists a sentence ϕ where ϕ is only true if A(┌ϕ┐) is true, where ┌ϕ┐ is the numerical representation of the bytes in ϕ. Mathematically, we can express the same as follows, with T⊢ read “T proves:”
∀A∃ϕT⊢ϕ⟺A(┌ϕ┐)
So let’s say that we’re dealing with A(x):=x∗2=4. Then there’s a sentence ϕ where strong enough theories can prove that ϕ⟺┌ϕ┐∗2=4. In this case, we can choose ϕ to be the sentence 0=1. Then ┌ϕ┐=3161393, and indeed T can prove that
0=1⟺3161393∗2=4
since both sides are false.
In the domain of programs, we’ve seen that any program you can name that transform programs into other programs has a fixed point. The Diagonal Lemma says something extremely similar for math: any statement you can name that maps the numerical representation of a statement to another statement has a fixed point. And as a bonus, strong enough theories can prove that.
Proof Sketch: Diagonal Lemma
Consider a sufficiently strong theory T and any arbitrary formula A with one free variable. Then there exists a ψ so that T proves that ψ⟺A(┌ψ┐).
The set of formulas with one free variable are enumerable (for example, by printing all strings and then discarding any that have more than one variable symbol):
274 => "x = 1"
...
672 => "x = x"
...
1837501 => "5x = x && 4 = 5"
We’re going to define a function f(s)(s′) which evaluates s on the byte-representation of s′. For example, f(x is prime)(x * x = 100) evaluates to “33823693116354608 is prime” (the string “x*x= 100” in UTF-8 has the decimal representation 33823693116354608). Notice that f maps two formulas with a free variable into a single sentence with no free variables.
Let δ(ϕ)=A(┌ϕ┐).
Now for the trilemma. All the formulas in our system definitely have a written representation, and all written representations with one free variable definitely count as formulas in our system.
So it must be that δ has a fixed point. And that fixed point is exactly what we’re after: some ψ so that ψ and A(┌ψ┐) are logically equivalent. (Notice that we’ve shifted from “output equivalence” to “logical equivalence.”)
So we’ve seen how we can prove this. We’re going to omit the proof that T itself can also prove this, since it’s a bit too hairy for our taste. If you look into it, it basically involves proving that T can construct and prove this same argument inside itself.
Proof Sketch: Gödel’s Incompleteness Theorem
We’ve finally arrived at Gödel’s Incompleteness Theorem. Here’s a quick reminder of the statement.
Gödel’s First Incompleteness Theorem. Any sufficiently powerful theory must be either inconsistent or incomplete.
The core idea is to construct a sentence S like “this sentence is unprovable.” Then if S is provable, it’s wrong (the surrounding theory can prove things that are contradictory; this is called being inconsistent). If T can’t prove S, then S is true (the surrounding theory has truths that it can’t prove; this is called being incomplete).
That’s a slick argument, but are sentences like “this sentence is unprovable” even allowed? How do you express something like “this sentence” formally? The Diagonal Lemma allows us to do just that.
Let A(┌x┐)=∀p, the string p is not a proof of x. In other words, A(┌x┐) = ”x is unprovable”.
Then by the Diagonal Lemma, we can use T to prove that there exists an x with x⟺A(┌x┐), or x⟺ (x is unprovable). And ”x⟺ (x is unprovable)” is exactly “this sentence is unprovable.” So we can build these sentences!
Proof Sketch: Tarski’s Theorem
Here’s a quick reminder of what Tarski’s Theorem says.
Tarski’s Theorem. Any sufficiently powerful theory cannot define its internal notion of truth.
To prove it, we take A(┌x┐) = (x is not true). The Diagonal Lemma guarantees that we can prove the existence of an x such that x⟺ (x is not true). But ”x is true ⟺ x is not true” is obviously contradictory.
The only thing we can point to is our original A, which must have been flawed. It must be that theories cannot define predicates like x is true or x is not true.
Conclusion
I hope you’re convinced that diagonalization is an extremely powerful tool.
From our original diagonalization trilemma, we were able to immediately show that primitive recursive functions aren’t complete, that there are more reals than naturals, and that program-transforming-programs must all have fixed points.
Then we used the same trilemma to construct a new tool, the Diagonal Lemma, and closed out the post by using it to construct the strange sentences required for Gödel and Tarski’s famous theorems.
We’ve kept the math relatively light, leaning on intuition and code where necessary. If you want a more rigorous treatment of this topic, I highly recommend continuing with Yanofsky [0], upon which this post is based.
Notes
[0] Note that we’ll use the curried f(3)(5) and uncurried f(3,5) forms interchangeably in this post.
[1] A delightful corollary: if your language is weak enough that you can solve the halting problem, then it must not be able to build an interpreter for itself. That’s what happens with P.R. functions, which all halt.
Appendix
Gödel Numbers
Gödel numbers are a way of converting formula into numbers. We denote the Gödel number of x as ┌x┐. You can imagine ┌x┐ just interpreting the underlying bytes of x as an integer instead of a string.
const gödel = (s: string): bigint => {
const byteArray = new TextEncoder().encode(s);
const hexString = Array.from(byteArray).map(byte => byte.toString(16).padStart(2, '0')).join('');
return BigInt(`0x${hexString}`);
}
const unGödel = (n: bigint): string => {
const hexString = n.toString(16);
const byteArray = new Uint8Array(hexString.match(/.{1,2}/g)!.map(byte => parseInt(byte, 16)));
return new TextDecoder().decode(byteArray);
}
console.log(gödel("x * 2 = 4"))
console.log(unGödel(2215926989203043065908n))
Diagonalization Proof (no exposition)
Here’s the straight math version of the general diagonalization argument.
Diagonalization. For all sets X and Y with a function f:X×X→Y and a function δ:Y→Y with no fixed point, there exists at least one function g:X→Y such that there exists no k such that f(k)=g.
Proof. Let g(x)=δ(f(x,x)). For any k, g=f(k), since g(k)=f(k)(k).
Acknowledgements
This post (and the primitive recursive post) were prepared as part of my final work for the MIT class Seminar in Logic (18.504). Thanks to Henry Cohn, Lisa Kondrich, and Laker Newhouse for their extensive suggestions, feedback, and help with both this post and the primitive recursive introduction post.
References
[0] Noson S. Yanofsky (2003). A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points*. Bulletin of Symbolic Logic, 9(3), 362–386.*
[1] Garrabrant, S., & Eisenstat, S. (n.d.). Diagonalization fixed point exercises. Retrieved from https://www.lesswrong.com/posts/FZkLa3GRLW97fpknG/diagonalization-fixed-point-exercises
[2] Kelly, K. T. (n.d.). Computability and Learnability.
[3] Primitive recursive function. (2023). Retrieved from https://en.wikipedia.org/wiki/Primitive_recursive_function
[4] Smith, P. (2013). An Introduction to Gödel’s Theorems. Cambridge, England: Cambridge University Press.
[5] Solomon, E. (1958). Unpacking the diagonal lemma. Retrieved from https://math.stackexchange.com/questions/127852/unpacking-the-diagonal-lemma
Once you place it, you’ll see an abstract representation of the MPU 6050 with all its pins.
To figure out what these pins do, you’ll need to take a look at the part’s datasheet (Google is your friend). These tend to be long and verbose; the MPU6050 datasheet is more than 50 pages long. A good place to start is by looking at the pin out table.
This table describes the purpose of each of the pins on the bottom of the MPU6050. Some of these descriptions are self-explanatory; pin 18 is labelled “GND” and is supposed to be connected to ground. We can start by connecting that one in our schematic editor.
Here, we can see that pin 10 (REGOUT) is supposed to be connected to a 0.1uF capacitor and then to GND. Let’s add that to the schematic (recall that 0.1uF = 100nF).
AUX_DA and AUX_CL are another I2C pair for “connecting external sensors,” which we don’t have. We shouldn’t leave them unconnected, since I2C lines need to be kept at 3.3v by default, so we connect them to our 3.3v power through another pair of 4.7k pull-up resistors.
INT is an interrupt pin; the gyroscope can activate it to quickly signal something like “this chip is in free-fall.” We won’t use it.
We therefore choose not to connect EP.
Congratulations! You’ve set up your first chip.
We’ll grab one of these 1117 chips. Digging through its datasheet, we find this wonderful typical operating circuit in Chinese.
We copy that diagram into our schematic as follows.
It’s pretty simple to connect in the schematic. Make sure you put the VBAT connection on the + side of your battery, and the GND connection for the - side.
Phew! That’s a lot of pins to connect.
According to the top of the diagram, VBAT should be connected directly to the battery.
The schematic can be deceiving; although these look like four separate circuits, the V3.3s and GNDs all link together. This is why it doesn’t matter that the 4.7uF capacitor is only graphically attached to the bottom pins; it’s electrically connected to all of them. [3]
According to the STM32F302 datasheet, NRST is active low. This means that the pin should usually be high (at 3.3v). When we push the reset button, it should temporarily drop to ground to restart the board. We’ll do that with the following circuit.
SW1 is a generic pushbutton; when you push, it connects the 1/2 side to the 3/4 side. By default, NRST is held to 3.3v, since it’s connected to V3.3 through that 47k resistor. When SW1 is held, NRST is also connected to ground through a 10k resistor. Since the ground resistor is smaller, the voltage on NRST jumps closer to ground. This gadget is called a 
So usually Boot0 should usually be low, corresponding to main flash memory, but when we hold a button, we’ll set Boot0 high to boot from system memory instead. We won’t worry about the third chart entry, embedded SRAM, for now.
If we want to boot from system memory, we’ll hold down the SW2 button during boot up.
None of our microcontroller pins are labelled “SWDIO”, but we can reference this handy table to see which pin handles that function. In our case, it looks like the PA13 pin handles SWDIO.
We also need to attach SWDCLK, SWO, and NRST. First we’ll put little tags on the relevant pins:
Then we’ll grab a 2x5 pin header with 1.27mm spacing and attach those tags to it, along with power and ground.
We now have the basics of the microcontroller fully configured. All that’s left is to attach inputs and outputs for the IMU and servos.
We connect PA9 and PA10 to the IMU with the same SDA and SCL tags we used back then.
And looking at TIM2, we’re in luck! It can drive four independent PWM channels for our four servos.
Checking the pinout table, we see that TIM2_CH1 corresponds to PA0, TIM2_CH2 to PA1, and so forth.
We connect some labels as usual.
Our servos have a 3x1 female connector with 2.54mm spaced pins. They accept power, ground, and signal on those three lines, and power in the middle. We grab four corresponding male headers from the parts library, and GND, VBAT, and each signal line.
That’s all; the finished schematic should look like this.
A word of congratulations: designing schematics is probably the hardest part of this project, especially for someone with programming background. And designing your first schematic is much harder than your second: when you design your second schematic, you’ll already understand LDOs, SWD, timers, pull-up resistors, etc. Now you’re over the hump!