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 Dahlqvist), followed by a talk by Edon Kelmendi (details below)

Speaker 1: 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.

Speaker 2: Edon Kelmendi (QMUL)

I will give the proof a classical result by Blondel, Jeandel, Koiran, Portier, from 2003. It is about the emptiness problem for quantum automata, namely the question "is there a word accepted with probability > 50%". There are two proofs:

1. that problem is undecidable,

2. the problem "is there a word accepted with probability >= 50%" is decidable. "