STRONG EQUIVALENCE

So we shall say that A and B are strongly equivalent - for all interpretations they either both diverge (loop infinitely) or else both converge (halt, terminate) with the same outputs. 

We shall study the question of the strong equivalence of flowcharts at length, and in particular examine when the strong equivalence problem is decidable. We shall see that in the general case it is undecidable and not even partially... 

Strong equivalence requires" that for any interpretation and input either the values of the computations of P and P are both undefined or they are both defined and are equal. Several notions of equivalence nay be defined in a similar way by restricting the set of interpretations. Thus ... 

These equivalence relations are not the sane. Obviously strong equivalence implies recursive equivalence and recursive equivalence implies finite equivalence. None of the reverse inclusions hold. We are already in a position to show that finite equivalence does not imply recursive equivalence. Consider the scheme of P of Example II-3 which halts for all finite interpretations but diverges for some infinite hit recursive interpretations (for the interpretation of P we saw that caused divergence is obviously recursive). We can diagram P as ... 

There are many other possible notions of equivalence, depending on the underlying phenomena one wishes to nodel and study. In our later discussion of block structure and transformations to structured form we shall meet some definitions yet more rigorous than "strong equivalence" - notions of computational equivalence or structure preservation where one demands that not only the end result be the same but that the outputs be obtained in roughly similar ways. One stronger notion is total equivalence which only holds between always halting schemes. 

DEFINITION Scheme P is totally equivalent to scheme P if P and P always halt and P is strongly equivalent to P. ... 

Now we introduce seme "weaker" definitions of equivalence, relaxing some of the demands of strong equivalence. 

DEFINITION A relationship v between schemes is a reasonable equivalence relation if P Q always implies that P is weakly equivalent to Q and if whenever P and Q are strongly equivalent then P Q. ... 

Now weak equivalence, finite equivalence, recursive equivalence and strong equivalence are all reasonable equivalences although the first is not a true equivalence relationship and the last three are. Reasonable equivalences stand between weak and strong - they must hold between schemes that behave identically for all interpretations and must fail between schemes which can be demonstrated to produce different results on the same interpretation. Total equivalence is not a reasonable equivalence because it does not hold for schemes which can diverge, and... 

Notice that if and P2 contain different function or test letters then strong equivalence between and implies a kind of degeneracy, in that certain functions and predicates are not really needed. We need a different type definition of equivalence to handle the case in which different schemes compute the same function under varying interpretations of the functions they do not have in common. 

We shall be particularly concerned with transformations on schemes which preserve strong equivalence. Some of these will be global transformations acting cn the scheme as a unit and others will be local, replacing parts of a scheme with other strongly equivalent subschemes. 

We can characterize strong equivalence in a similar fashion. If s is a consistent path (execution sequence) through P and s is a consistent path (execution sequence) through P (each beginning at START of course) we can apply our algorithm simultaneously to s and s and if s,s is a consistent set of paths - so for all tests T, ... 

By the definition of strong equivalence, (1) implies (2). Evidently (2) implies (3) since I, is a particular free interpretation. 

We can construct given TCP) a tree T CP) - finite or infinite - which in some sense can be considered equivalent to scheme P. If node q on level n in TCP) is labelled with execution sequence s = Ck, ...,k ), replace label s with a label containing the statement or instruction named by k. Thus our new tree T CP) will Mve as labels the instructions of P ordered so that a path through T CP) gives the proper sequence of statements executed by an appropriate computation in P. We can almost consider T CP) to be a scheme strongly equivalent to P. If a node q is now labelled with a test TCu, ...,u ) and Ms two branches to nodes and q labelled with statements r and r, one... 

It is evident that if TCP) is infinite we cannot really "construct" T (P). But if TCP) is finite, we can carry out this process and now T (P) really is a program scheme strongly equivalent to P its graph is a tree. 

THEOREM 3.8 Strong equivalence is decidable for tree program schemes. 

A scheme which is known to be always halting can be effectively transformed into a strongly equivalent tree program scheme. Hence ... 

The flowchart P in Example III-l is obviously not free since it contains infinite paths but no infinite execution sequence. However the strongly equivalent tree program scheme T (P) is clearly free since we have eliminated the useless tests. This situation is general as we now observe. 

THEOREM 3.12 If P is an always halting scheme we can construct a strongly equivalent free tree program scheme. 

We have seen examples of schemes which are not free. There are schemes which are not even strongly equivalent to any free scheme. Such a scheme appears in Example III-2. Intuitively speaking, Example III-2 cannot be "freed" because we must use the two tests as a clock, to see how long it takes to find fn(x) with PCf x)) = 0 and then to run through this cycle again and update x to gnfn(x). To justify this statement formally, we need some additional notation and results. 

This result allows us to conclude that the scheme P in Example III-2 is not strongly equivalent to any free scheme since L(P) = gnfnx n > 1 is not regular. 

A SCHEME NOT STRONGLY EQUIVALENT TO ANY FREE PROGRAM SCHEME... 

---