ausblenden:
Schlagwörter:
-
Zusammenfassung:
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.
