Trifonov, Trifon (2012): Analysis of methods for extraction of programs from nonconstructive proofs. Dissertation, LMU München: Faculty of Mathematics, Computer Science and Statistics 

PDF
Trifonov_Trifon.pdf 1MB 
Abstract
The present thesis compares two computational interpretations of nonconstructive proofs: refined Atranslation 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 Atranslation 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 letconstructions 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.
Item Type:  Thesis (Dissertation, LMU Munich) 

Keywords:  program extraction, nonconstructive proofs, Dialectica interpretation, refined Atranslation, infinite pigeonhole principle 
Subjects:  000 Computers, Information and General Reference > 004 Data processing computer science 000 Computers, Information and General Reference 
Faculties:  Faculty of Mathematics, Computer Science and Statistics 
Language:  English 
Date Accepted:  15. February 2012 
1. Referee:  Schwichtenberg, Helmut 
Persistent Identifier (URN):  urn:nbn:de:bvb:19140308 
MD5 Checksum of the PDFfile:  850efb75d2e696166f729179f900a9f7 
Signature of the printed copy:  0001/UMC 20069 
ID Code:  14030 
Deposited On:  20. Feb 2012 14:09 
Last Modified:  16. Oct 2012 08:58 