de.mpg.escidoc.pubman.appbase.FacesBean
English

# Item

ITEM ACTIONSEXPORT

Released

Report

#### A general technique for automatically optimizing programs through the use of proof plans

##### MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44961

Programming Logics, MPI for Informatics, Max Planck Society;

##### Locator
There are no locators available
##### Fulltext (public)

MPI-I-94-239.pdf
(Any fulltext), 28MB

##### Supplementary Material (public)
There is no public supplementary material available
##### Citation

Green, I.(1994). A general technique for automatically optimizing programs through the use of proof plans (MPI-I-94-239). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-B7BB-8
##### Abstract
The use of {\em proof plans} -- formal patterns of reasoning for theorem proving -- to control the (automatic) synthesis of efficient programs from standard definitional equations is described. A general framework for synthesizing efficient programs, using tools such as higher-order unification, has been developed and holds promise for encapsulating an otherwise diverse, and often ad hoc, range of transformation techniques. A prototype system has been implemented. We illustrate the methodology by a novel means of affecting {\em constraint-based} program optimization through the use of proof plans for mathematical induction. Proof plans are used to control the (automatic) synthesis of functional programs, specified in a standard equational form, {$\cal E$}, by using the proofs as programs principle. The goal is that the program extracted from a constructive proof of the specification is an optimization of that defined solely by {$\cal E$}. Thus the theorem proving process is a form of program optimization allowing for the construction of an efficient, {\em target}, program from the definition of an inefficient, {\em source}, program. The general technique for controlling the syntheses of efficient programs involves using {$\cal E$} to specify the target program and then introducing a new sub-goal into the proof of that specification. Different optimizations are achieved by placing different characterizing restrictions on the form of this new sub-goal and hence on the subsequent proof. Meta-variables and higher-order unification are used in a technique called {\em middle-out reasoning} to circumvent eureka steps concerning, amongst other things, the identification of recursive data-types, and unknown constraint functions. Such problems typically require user intervention.