Browse Prior Art Database

OPTIMIZATION AMONG PROVABLY EQUIVALENT PROGRAMS

IP.com Disclosure Number: IPCOM000128257D
Original Publication Date: 1974-Dec-31
Included in the Prior Art Database: 2005-Sep-15
Document File: 9 page(s) / 34K

Publishing Venue

Software Patent Institute

Related People

Paul Young: AUTHOR [+3]

Abstract

We consider the extent to which it Is possible, given a 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.albstract recursion-theoretic complexity theory., but some of our results may be viewed as directly challenging the intuitive interpretation of earlier results In the area.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 15% of the total text.

Page 1 of 9

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

OPTIMIZATION AMONG PROVABLY EQUIVALENT PROGRAMS

Paul Young Computer Sciences and Mathematics Deportment Purdue University Lafayette, Indiana 47907

Abstract. We consider the extent to which it Is possible, given a 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.albstract recursion-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.

1. Motivation'

In, traditional recursion-theoret.1c.s,tudies of com0exity theory, two programs are.rega'rded as equivalent if.they compute the'same function. The efficiency of.,the running time of a program is studied by comparing its' (ultimate, a.ej:oehavior with the running times of all.O'ther programs for the tame function.

It is not very difficult to find programs p,and pl which in fact both compute the same function, which can both be proven to halt on all inputs, yet which can not be proven to compute the same function. Suppose then that one is trying to optimize some class of programs, star.ts with a program p which is known to.compute some desired function, f, and then is~given program pl as a'better program for f. The user must regard the situation as unsatisfactory; off hand, his only method for verifying that the use of.-program pl Is legitimate is: after ha*ing run p' on a given input x, he must then run program p on input x to verify.that p',is correct,on that input,.

In, practice then, it seems clear that if one wants to consider program p as a possible optimization of program p, one first needs a proof that p and p' really perform the same task. (in this paper, w.e.assume that this means that we can prove that programs p and pl really do compute the same function, i.e., p and pl. are provbbly equivalent.)

We limit our attention to programs for total functions, and for the 'purpose of this study we do not question the.usual recursion-theoretic assump-tions that (1) all programs are legitimate objects of study, and (H) Infinite functions and the ultimate behavior of run times on lArge.argument yield useful

1 nsights into computational complexity. our work may be viewed as questioning t he traditional view that any two programs which compute the same function should be regarded as equivalent. If this view is taken seriously, it implies that many results of recursion theoretic complexity theory should be reexamined. In the long run., work such as this may have implications for studies of how one proves equivalence of programs (Floyd, Manna, et.c.), but we make no such explicit claims here.

1 1 Supported by NSF Grant GJ 27127A). Research performed while the author was a vis...