Proving Termination and Non-Termination of Busy Beaver Machines
(or how to use an otter to catch a beaver to chase a platypus)
Date and time: 11.30am - 12.30pm, Friday 20 November, 2009
Venue: 10.08.03 (Building 10, Level 8, Room 3)
Abstract:
The busy beaver problem is to find the maximum number of 1's that can be printed by an n-state Turing machine of a particular type. A critical step in the solution of this problem is to determine whether or not a given n-state Turing machine halts on a blank input. Previous work has shown how non-termination can be detected by using induction methods based on an analysis of a given length of the execution trace of the machine. In this paper we investigate an important heuristic which significantly improves the performance of this method, particularly for the more difficult cases. This heuristic, which we call the /observant otter,/ is based on the detection of patterns earlier in the execution trace. We describe our implementation of this method and report various experimental results based on it. We also discuss some issues of decidability that arise from this research, some investigation of two-dimensional busy beaver machines, connections to universal Turing
machines, and some potential areas of investigation for machine learning techniques.
About the speaker:
James Harland is an Associate Professor in Computational Logic in the School of Computer Science and IT at RMIT. He obtained his PhD from the University of Edinburgh in 1991, and has been a lecturer at RMIT since 1994. His research interests include agent programming, automated reasoning, logic programming and busy beaver machines.
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.