Conservative fixpoint functions on a grap

Abstract

In this paper we present a derivation of a general solution for a class of programming problems. In these problems a function over the vertices of a directed graph is to be computed, being defined as a least fixed point of some monotonic operator. If this operator satisfies a certain restriction with respect to its image for a differential change in its argument, it is called conservative, and an elegant general solution may be derived. It is stipulated that a strictly calculational derivation is only possible if the level of abstraction is sufficiently high. To that end a modest extension to the functional calculus is proposed, including partial functions, and a few simple high level programming constructs are introduced. The program scheme obtained is applied to a particular example, for which so far no derivation, other than informal ones, is known to exist. The solutions presented are not new, but the calculational, abstract and compact technique of deriving them is meant to improve and complement the current techniques [KNU77, REY81, REM84]. It is believed to simplify the derivations for a wider algorithm class [EIJ92] than the one treated here.