Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #93110 | |
|---|---|
| Title: | The Synthesis of Efficient Programs |
| Authors: | Evans,R |
| Date: | 1993 |
| Presented: | |
| Keywords: | |
| Abstract: | The aim of this project was the synthesis of efficient (polynomial) time programs. There is a well-developed theory, Bounded Arithmetic, which synthesises all and only the polynomial time functions. The central idea behind Bounded Arithmetic is to use a restricted type of induction, PIND induction. A variant of Bounded Arithmetic was implemented in a system called MUSSEL. In this system we can automatically extract programs from proofs and evaluate the resulting programs. It is shown that all programs synthesisable in MUSSEL are polynomial time. Programs synthesised in MUSSEL are, in general, more efficient than the corresponding Oyster programs, but the proofs are, in general, longer and harder. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}