Computability in Europe 2006
Logical Approaches to Computational Barriers

Print current page  Print this page

Regular Talk:
NdE - Normalization during Extraction

Speaker: Mircea-Dan Hernest
Slot: Tue, 14:50-15:10, Faraday C (col. 3)

Abstract

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 Valid HTML 4.01! Valid CSS! eXTReMe Tracker hit counters by www.free-counters.net