We present a methodology for improving the implementation of the
NbE
(Normalization by Evaluation) normalization algorithm in
call-by-value functional programming languages like
SCHEME. Such optimizations are meant
to heavily
(at least from an empirical, observational viewpoint) decrease
the run-time complexity of the NbE-normalization of long
sequences of nested term applications
(t_n .. (t_2 (t_1 t_0))..). A situation of this
kind occurs for example in the case of the extraction of a modulus of uniform continuity for a
closed term t of Goedel's
T of type
(nat=>nat)=>(nat=>nat). The
aforementioned extraction is by means of an author's adaptation of
Kohlenbach's
Monotone Dialectica
Interpretation
(for the more efficient synthesis of majorants
in NbE-normal form)
and proceeds from a proof of the hereditarily extensional equality of
t to itself. This example was implemented in the
MINLOG proof-system, hence a
machine
DEMOnstration will be
available for the NdE
optimization of the call-by-value NbE-normalization.