On the algorithmic structure of Dialectica realisers

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.