There is a quarter-long collaborative class project to describe the lambda busy beaver function. Everything about the project is negotiable, but I will provide starting points and defaults. The quality of your participation in the project will determine a significant part of your grade for the course. Until someone convinces me otherwise, the project will be carried out as a HyperNews discussion, starting with my introductory message.

A busy beaver function maps each integer n to the size of the largest output produced by a program of length at most n. Each general-purpose programming language has its own busy beaver function, but all of them grow faster than every Turing-computable function. Yet, the busy beaver is computable in a certain intuitive sense. There is a machine with a continuously visible output display that produces a finite increasing sequence of integer outputs, the last of which is the value of the busy beaver function. But, the machine never halts, and in general we don't know when it has produced its last output.

The lambda calculus is not a general-purpose programming language in any natural sense that I'm aware of, but it contains an infinite number of general-purpose programming languages, and its output function is semicomputable, so it has a busy beaver function of its own. For the purposes of our lambda busy beaver project, the size of a lambda term is the number of instances of variables. In a straightforward sense, number of instances of variables is not a legitimate program size measure, but in a more sensible sense, it is. Start the discussion by identifying these two senses.

There is probably no completely general, uniform, and reliable characterization of the lambda busy beaver function that's any nicer than its standard definition. But, approximate information can be very interesting, and quite challenging to generate. For some small finite number of inputs, you can derive the busy beaver value and prove it correct. Find as many of those values as you can. Why and in what sense is the number necessarily finite, and what is ``small''?

After exhausting precise busy beaver values, you can give interesting lower bounds on busy beaver values, and perhaps even argue that they are likely to be tight. These lower bounds come from incredibly fast growing total computable functions.

In this project, you will generate a sequence of uniform and elegant techniques for defining very fast growing functions. The fun and interest come from noticing how delicately, suddenly, and nonuniformly you switch from one technique to the next. At first, you will think of the lambda terms as representations of integers (a topic we will address precisely in a few weeks, but which you can attack intuitively from the start). Soon, you will need to switch to thinking of lambda terms as ordinal notations.

Since this is an open collaborative project, those of you who know about ordinal notations and relevant ideas from logic and theory of computation will teach those who don't. When you ask the right questions, I will point you to some useful articles.