Program equivalence

Program equivalence --- эквивалентность программ.

When a program calculates some function (as is usually the case), there is a natural and most general definition of equivalence: two programs, which have a common set of arguments are functionally equivalent, if their functions are the same.

However, an unavoidable obstacle in developing a general theory is the following negative result in the theory of algorithms. Some property of a program is said to be internal, if it takes place for all programs functionally equivalent to it. Rice has proved that for any internal property of a program, there is no algorithm which would recognize those programs which possess the given property (naturally, the class of programs should be reasonably meaningful, for instance, it should compute any recursive function).

The principal way of narrowing the concept of equivalence of programs is to compare not only the values of the functions evaluated by programs, but also some history of computation during the execution. Formally the concept of history is introduced as follows. In addition to the universal algorithm of program execution, another algorithm is introduced which, in accordance with the program and a set of its input data, constructs some object. The latter is called the history of the program realization and contains some information about its execution. The history may comprise any number of details, but the result of the program execution has to be recovered by it in a single-valued way. Hence, programs with coincident histories automatically have coincident results. A special case of a history is the program itself (an identical tracing algorithm). This history, naturally, is the most detailed one, because we can get any information from the program by applying to it the universal algorithm of execution. The equivalence based on this history appears to be the narrowest: the program is equivalent only to itself.