On the algorithmic structure of Dialectica realisers
Davide Barbarossa, Thomas Powell
TL;DR
The paper tackles the algorithmic structure underlying Gödel's Dialectica interpretation by presenting it as a Hoare-style rule system. It introduces Dialectica triples and a Dialectica Hoare logic to capture forward and backward witnesses for implications, and develops a generalised backpropagation operational semantics, including a Dialectica while loop. This framework clarifies the stateful, program-like behavior of Dialectica realisers and provides a concrete basis for reasoning about iterative and learning-based interpretations of classical proofs. The authors envision future work that leverages this perspective for theoretical advances and practical applications in proof mining and beyond.
Abstract
Gödel's Dialectica interpretation is a fundamental tool for the extraction of computational content from proofs, and plays a central role in today's proof mining program. In the past decades, it has also been studied from the perspective of programming languages, and our contribution is in that direction. Specifically, we present Dialectica as a collection of rules in the style of Hoare logic, where Dialectica is now viewed as a language for specifying procedural programs that come with a forward and backward direction. This viewpoint captures the interesting dynamics of realisers extracted by the Dialectica interpretation, and we illustrate this by defining a generalised backpropagation semantics for a fragment of this language. We envisage this work as providing a base for several future developments, both theoretical and practical, which we outline at the end.