Gamekeeping for the Zany
Zoo: How to Hunt Busy Beavers, Placid Platypodes* and
other Alliterative Animals
Date and time:
Venue: 10.08.03 (Building 10, Level 8, Room 3)
Abstract:
A common example of a non-computable function is the busy beaver, which is defined in terms of a particular class of Turing machines. For a given number of states, the busy beaver function is the largest number of 1s that can be printed by a machine that halts. This value is only known precisely for n <= 4, but the lower bounds known for n = 5 and n = 6 are already spectacularly large. In this talk we discuss the use of induction methods to show the non-termination of particular classes of machines. These are centred around the generation of inductive conjectures about the execution of the machine and the evaluation of these conjectures on a particular evaluation engine. We describe our experiments for the $n=4$ and $n=5$ cases, and discuss the language required in order to express the appropriate inductive conjectures. A small number of chocolate frogs will be distributed at random points in the talk.
* There is no universally accepted plural for "platypus". This is one possibility; others include "platypuses", "platypode" and "platypus". The once-common "platypi" is now deprecated.
About the speaker:
Dr. James Harland is an A/Professor in the
Seminar Organisation
Seminars are free and open to the general public. No booking is necessary. If you are interested in giving a presentation in this seminar series, or to make suggestions for speakers, please contact Xiaodong Li, the seminar co-ordinator.