Events

Date: 1 May 2026   Time: 15:00 - 17:00     

Location: Room 4.24. Peter Landin Building, Mile End. E1 4NS Map 

This week Theory meeting will have an invited speaker (hosted by Fred), details below.

Speaker: Reuben Rowe (Royal Holloway)

Title: Algorithms for Checking Infinite Descent

Abstract:

The (PSPACE-complete) Infinite Descent property underpins the trace-based validation of cyclic derivations that capture inductive and coinductive reasoning, as well as the size-change approach to proving program termination. In the literature, we find a couple of different algorithms described for deciding Infinite Descent: a dynamic programming algorithm incorporating a fixed-point saturation (e.g. as suggested in the size-change termination paper by Lee, Jones, and Ben-Amram), and an encoding via containment of omega automata (e.g. in Brotherston's thesis).

In this talk I will describe work in which we have developed an alternative automata-theoretic encoding and an optimisation of the dynamic programming algorithm that takes into account some specific symmetries present in the Infinite Descent problem. I will also describe some more efficient, but approximate (i.e. incomplete) approaches for checking Infinite Descent that we have developed. I will comment on the relative tradeoffs in the (runtime) complexity of the decision procedures, and report on an experimental evaluation of our implementations of these algorithms within the Cyclist theorem prover framework. Interestingly, we found the approximate methods to provide good coverage in practice. I will also mention some work on formalising these criteria for Infinite Descent within the Isabelle theorem prover.