John Tromp: The Binary Lambda Calculus, The Smallest Program Language

We'll discuss the Binary Lambda Calculus (BLC), an extremely simple programming language that is basically lambda calculus written in binary, whose design was motivated by the study of minimal size programs. We'll look at several example programs such as a 4-bit cat and a prime sieve. We'll show how BLC programs are at most a constant longer than those in any other language, how to define several notions of complexity of mathematical objects, and how to prove theorems about them. We'll see how to define a busy beaver function, how to define the uncomputable number known as Chaitin's constant, and how to win obfuscation contests. John Tromp is a Dutch computer scientist. He formerly worked for Dutch Centre for Mathematics and Computer Science. Tromp discovered the number of legal states of the board game Go, and co-authored with Bill Taylor the Tromp-Taylor Rules, which they call "the logical rules of Go". Paper on the Binary Lambda Calculus: http://tromp.github.io/cl/LC.pdf And check out John's LC & CL Playground: http://tromp.github.io/cl/cl.html John's Homepage is here for his other explorations: https://tromp.github.io