Logical Approaches to Computational Barriers

NdE - Normalization during Extraction

Speaker:
| Mircea-Dan Hernest |

Slot: |
Array, 14:50-15:10, col. 3 |

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.

websites: Arnold Beckmann | 2006-06-28 |