OPTIHIZATION AHONG PROVABLY EqUIVALENT PROGRAHS

Abstract. We consider the extent to which it's possible, given 8 program p for computing a function, f, to Find an optimal program p ' which also computes f and is either provably equivalent to p or else provably an optimal program. Our methods and problems come chiefly from abstract recurslon-theoretic complexity theory, but some of our results may be viewed as directly challenging the intuitive interpretatIon of earlier results In the area. Key words and phrases: abstract complexity, theory, prOVing equivalence or correctness of programs