The Method of Explicit Scheduler

In this chapter we present an alternative method for proving termination of GC programs under various fairness assumptions. The presentation is based on [AO 83] and [APS 84]. The main idea of this approach is the following: reduce the fair-termination problem of GC programs to ordinary (nondeterministic) termination of GC _R programs, an augmentation of GC with random assignments. A similar idea is mentioned also in [B 82] and [PA 81].The reduction method is such that it uses random-assignment (of natural numbers) to explicitly represent the fair scheduler within the program. Once this transformation is carried out, the resulting nondeterministic program will have a variant decreasing along every direction whenever the original program is fairly terminating. Finally, the effect of the transformation is simulated within a proof rule, which now serves for proving properties of the original, untransformed, program.