Department of Computer Science, University of Oxford, UK
Here’s a blog of things I’ve found interesting in computer science. I’ve tried to write this blog largely as a way to write about ideas and concepts I've been playing around with recently, as well as a way to sharpen up my mathematical writing. Hopefully it lets me do both of those things!
Posts
Here’s what I've been up to. Click the titles of the posts to go to their respective pages.
Semënov arithmetic, the extension of Presburger arithmetic by the exponentiation function $x \mapsto 2^{\abs{x}}$, is decidable. That gives us good reason to be interested in knowing what the theory can define and express; if we have a problem that only requires those sets to be defined, then we know that that problem is decidable as well. So we're interested in knowing the sorts of sets that can be defined in Semënov arithmetic, and in particular the sorts of sets it can define that can't be defined in just Presburger arithmetic.
When talking about regular languages, we talk about regular expressions, which are convenient languages for defining and specifying particular regular languages. These regular expressions are built up from /atoms/ of the empty string $\emptystring$ and single letters $a, b, c, \dots$ of an alphabet $\alphabet$, /disjunctions/ of regular expressions $E + F$, /concatenations/ of regular expressions $EF$, and /the Kleene star/ $E^*$. These atoms and operations define all the regular languages.
Propositional logic is an altogether easier logic than first-order logic. In propositional logic, we only have to deal with propositional variables, which are either true or false, and Boolean combinations of those propositional variables. There are no quantifiers to introduce horrible complexity or undecidability to propositional logic, and everything has a finite sort of character. Propositional logic is a neat little logic.
In an earlier blog post , on modelling arithmetic in set theory, we looked at modelling the natural numbers in set theory, using some of the basic axioms of set theory to get there. Interestingly, though, we can go the other way, and model set theory from within the natural numbers. Using some tricks with the binary expansions of natural numbers, we get what's called the /Ackermann interpretation of set theory/, where the basic axioms of set theory come out true. Given that we only need these basic axioms to start talking about the natural numbers, this is quite a surprising result!
It's a standard result that all Büchi automata recognise precisely finite unions of languages of the form $U \cdot V^\omega$, where $U$ and $V$ are both regular languages; we call such recognised languages /$\omega$-regular expressions/. Büchi himself proved the result in \cite{Buchi-1960b}, Lemma 10. It's a nice result to have, particularly because of its simplicitly, as well as how well it captures the intuition of what a run on a Büchi automaton looks like.
In computer science, we like to show that things are decidable, and indeed the method to show that a problem is decidable is easy enough; simply give an algorithm that decides your problem. But we would also like to show that some things are undecidable (generally so we can stop trying to find algorithms for them).
I've been reading up around Büchi automata (BAs) recently, as well as their cousins (Muller, Rabin, Streett and parity automata, amongst others), and have been wondering what similar automata exist that may or may not be equivalent to Büchi automata. So here's a catalogue of some automata I've thought up as of late.
When doing mathematics, you might wonder what it is that makes mathematical statements true. It's true that $2 + 2 = 4$, sure, but what makes it true is unclear. Ask a mathematician, and they may heartily tell you that it follows from the axioms. But, if that's the case, what is it that makes the axioms true?
