Computer Science Speaking Skills Talk

— 3:00pm

Location:
In Person - Gates Hillman 8102

Speaker:
EMRE YOLCU , Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://www.cs.cmu.edu/~eyolcu/

An automated approach to the Collatz conjecture

The well-known Collatz conjecture can be seen as being about computation by rephrasing it as the statement that a certain small Turing machine is terminating (i.e., it halts on all inputs). Adopting this view, we explore the Collatz conjecture and its variants through the lens of automated reasoning. We use rewriting systems as our model of computation and reduce Collatz-like problems to termination of string rewriting. This enables us to search systematically for proofs of such problems using the methods developed for automatically proving termination of rewriting.

In the talk, I will describe two different ways of encoding Collatz-like problems into termination of string rewriting: an already-known one using a unary representation of integers and a new one using a mixed binary-ternary representation. When integers are represented in unary, the termination problem that corresponds to the Collatz conjecture (or even its much simpler variants that are trivially true) does not admit proofs via natural matrix interpretations, a method widely used in proving termination of rewriting. Then, to compare, I will show a few instances of nontrivial Collatz-like problems where simply changing the encoding results in the termination problem becoming easy to automatically solve via matrix interpretations.

This talk is based on joint work with Scott Aaronson and Marijn Heule, published in the Journal of Automated Reasoning.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

Add event to Google
Add event to iCal