Introduction

In the last post in this series, we defined universality of Boolean functions, went through a few proofs that specific sets were universal, and we showed the existence of two arity 2 Sheffer functions NAND and NOR. In this post, we’ll sketch out a proof showing that these are the only binary Sheffer functions.

Determining that a given function can’t be created by compositions of others from a set seems, at least at the outset, difficult. Who are we to say there is not some absurd combination, maybe involving many thousands layers of composition, that does not replicate the function we want? If there is a key fact that I took from the learning I did for this post, it’s that the key to proving that a set fails to be universal lies in the properties of functions that are left invariant by composition. If we can show that there is a property preserved by any combination of functions in our set, but that does not hold for all Boolean functions in general, then we have shown it cannot be universal.

Intro

While reading on nonstandard models of arithmetic, I recalled a fact that had come up once in a class on logic. While a formal language with many connectives is nice to work in, it becomes unwieldy to work on, requiring more inductive cases to be covered in the process of proving whatever fact you’re interested on. Because of this, we chose to work on a very simple language with only the connectives for not (\(\neg\)) and implies (\(\rightarrow\)).

Intro

Assembly is a tough language to write in. It is both excessively verbose and obstruse, which means it requires detailed and clear comments. While writing ROMS for the GameBoy I often found myself frustrated at the amount of comments that I had to write and at how they looked. Proper formatting would improve the readability, but would take time. I thought the problem of formatting text to match some kind of style guide was interesting in its own right, so I diverted and wrote a formatter to be used as a part of my ROM build process.

Intro & Problem Statement

Recently I’ve taken an interest in emulation and home-brew development for the original Nintendo GameBoy. I chose the beloved grey brick as a starting point for emulation for a few reasons:

• Relative simplicity of the system. It certainly didn’t feel simple when I first started looking at it, but compared to consoles of today the GameBoy is very lightweight. In terms of specifications, the GameBoy has an 8-bit CPU, a 16 bit address bus, 8 KB each of Work Ram and Video RAM, and a 160x140 pixel screen. I/O, sound, and LCD screen are all memory mapped, meaning that reads/writes in certain areas of the memory space will give information about or affect these peripherals.
• Strength of the community. The GameBoy home-brew community has been going strong since at least 1995, when the original version of the PanDocs, a collection of technical documentation on the hardware of the GameBoy, was started. The community has done an incredible work of documenting the behaviour of the system and creating tool chains to allow for development on it, such as GDBK2020 or RGBDS. See the appendix for some neat examples.
• GameBoy games were the first video games I owned, and the first really interesting glitches I encountered were on the Pokemon games. Hearing rumours about things like the mew glitch or seeing the garbage displayed when visiting a glitch city piqued my curiosity: what exactly is going on here? What would cause this machine to misbehave in such a way? Starting this project, I felt like I had the tools needed to get a deeper understanding of this phenomena.

Getting way off into the weeds, I decided that I would possibly give coding a GameBoy emulator a try. Grossly oversimplifying, the GB CPU is running the following loop