SCT through the reverse mathematical looking glasses

Silvia Steila, University of Bern. Part of the Logic Seminar Series.

In 2001 Lee, Jones and Ben-Amram introduced the notion of size-change termination (we call MSCT) for first-order functional programs, a sufficient condition for termination.  They proved the SCT criterion: a program is size-change terminating (i.e. MSCT) if and only if it satisfies a certain property (we call ISCT) which can be statically verified from the recursive definition of the program. 

From Lee, Jones and Ben-Amram’s paper we can outline the following three-step argument to prove the termination of a first-order functional program P: 

1) Verify that P is ISCT;

2) Apply the SCT criterion to prove that P is MSCT; 

3) Derive the termination of P from the fact that "every MSCT program terminates".

Since the Ackermann function is ISCT provably in RCA_0, a natural question arises: in which theory can we carry out the above argument?  Specifically, in which theory can we prove the SCT criterion?  Similarly, in which theory can we prove that every MSCT program terminates?  In this talk we focus on the reverse mathematical analysis of such statements.

This work is with Emanuele Frittaion, Florian Pelupessy and Keita Yokoyama.