Analysis of methods for extraction of programs from non-constructive proofs

The present thesis compares two computational interpretations of
non-constructive proofs: refined A-translation and Gödel's
functional "Dialectica" interpretation. The behaviour of the
extraction methods is evaluated in the light of several case
studies, where the resulting programs are analysed and compared. It
is argued that the two interpretations correspond to specific
backtracking implementations and that programs obtained via the
refined A-translation tend to be simpler, faster and more readable
than programs obtained via Gödel's interpretation. Three layers of
optimisation are suggested in order to produce faster and more
readable programs. First, it is shown that syntactic repetition of
subterms can be reduced by using let-constructions instead of meta
substitutions abd thus obtaining a near linear size bound of
extracted terms. The second improvement allows declaring
syntactically computational parts of the proof as irrelevant and
that this can be used to remove redundant parameters, possibly
improving the efficiency of the program. Finally, a special case of
induction is identified, for which a more efficient recursive
extracted term can be defined. It is shown the outcome of case
distinctions can be memoised, which can result in exponential
improvement of the average time complexity of the extracted
program.