On the algorithmic structure of Dialectica realisers
Davide Barbarossa, Thomas Powell

TL;DR
This paper reinterprets G"odel's Dialectica interpretation as a rule-based programming language with forward and backward semantics, facilitating understanding of its computational content and paving the way for future theoretical and practical advances.
Contribution
It introduces a novel rule-based, programming language perspective on Dialectica, capturing the dynamics of realisers with a forward-backward semantics framework.
Findings
Dialectica interpreted as a rule-based language with procedural semantics
Defined a generalized backpropagation semantics for a fragment of the language
Provides a foundation for future theoretical and practical developments
Abstract
G\"odel'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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
