Dr Noam Zeilberger’s most recently published paper, ‘A theory of linear typings as flows on 3-valent graphs’, grew ‘unexpectedly’ out of research he was doing into a theoretical framework for type systems, which are used in programming languages to reason about the behaviour of computer programs.
‘Basically, this paper is about a surprising connection between graph theory and programming,’ explains the Birmingham Fellow and member of the Theory Group within the School of Computer Science.
The background for this work came about after Noam thought it would be interesting to enumerate programs in a certain fragment of the lambda calculus, a formal system in mathematical logic that is a universal model of computation (like the Turing machine). There are only finitely many programs of a given size, so counting all programs of size n leads to a specific sequence of numbers (that begins 1, 2, 9, 54, 378,…), which Noam decided to look up in the Online Encyclopedia of Integer Sequences (OEIS), a huge database containing more than 300,000 different sequences of numbers that arise in different mathematical contexts (such as the prime numbers, or the Fibonacci series). An academic whose research generates a sequence of numbers can refer to the OEIS to find other contexts in which the sequence arises.
‘I entered the sequence into the OEIS and saw that it was listed, meaning that it had already been studied – but apparently for a completely different reason!’
In fact, it was a sequence that was first figured out in the 1960s by British codebreaker, mathematician and graph theorist Bill Tutte, who – like Alan Turing – worked at Bletchley Park. During the Second World War, Tutte made a game-changing advance in cryptanalysis of the Lorenz cipher, a major Nazi German cipher system which was used for top-secret communications within the Wehrmacht High Command.
Tutte’s original motivation for studying this particular sequence was related to the infamous (and at the time still unproven) Four-Colour Theorem, which states that any map in a plane can be coloured using four colours in such a way that regions sharing a common boundary do not share the same colour. Surprisingly, the sequence that Noam had generated by listing programs of lambda calculus was the same as the one that Tutte had calculated more than 50 years earlier by counting planar maps.
‘This discovery naturally got me wondering: why is there a connection between lambda calculus and graph theory, and how far does it go?’ relates Noam. ‘Well, it turns out that there are more such coincidences, relating various natural families of graphs with natural fragments of lambda calculus. For example, graphs that are 3-valent (meaning that every node has exactly three connections) correspond to programs in lambda calculus that are linear (meaning that every variable in the program is used exactly once). 3-valent graphs are very well-studied in graph theory, including in relation to the Four-Colour Theorem via work going back to the 19th century Scottish mathematician Peter Tait. On the other hand, linear lambda calculus has been used in computer science as a model of resource-bounded computation.’
In earlier work, Noam applied this correspondence to give a reformulation of the Four-Colour Theorem as a statement about a type system for linear lambda calculus. In the most recent paper, which was published earlier this year in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018) and recently won the College’s Paper of the Month award, he further develops the analogy between typing (in lambda calculus) and colouring (of maps).
How important is the new connection Noam has forged between graph theory and programming?
‘The way I think of it is that it’s still very much at the exploratory stage,’ he says. ‘We have found these unexpected connections and we want to see what they mean. For now, I’m interested in transferring ideas between fields.’