Synthesis of moduli of uniform continuity by the Monotone Dialectica Interpretation

We extract on the computer a number of moduli of uniform continuity for the first few elements of a sequence of closed terms t of Gödel’s T of type (N→N)→(N→N). The generic solution may then be quickly inferred by the human. The automated synthesis of such moduli proceeds from a proof of the hereditarily extensional equality (≈) of t to itself, hence a proof in a weakly extensional variant of Berger-Buchholz-Schwichtenberg’s system Z of t ≈(N→N)→(N→N) t. We use an implementation on the machine, in Schwichtenberg’s MinLog proof-system, of a non-literal adaptation to Natural Deduction of Kohlenbach’s monotone functional interpretation. This new version of the Monotone Dialectica produces terms in NbE-normal form by means of a recurrent partial NbE-normalization. Such partial evaluation is strictly necessary