Synthesis of Moduli of Uniform Continuity by the Monotone Dialectica Interpretation in the Proof-system MinLog
Mircea‐Dan Hernest · Electronic Notes in Theoretical Computer Science · 2007
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.