On flowchart theories. I. The deterministic case (Q1093364)

The author develops the notion of a ``\(\Sigma\)-flowchart over T'', where T is a type of iteration theory and where \(\Sigma\) is a ranked set. Intuitively, such a flowchart can be obtained from one of the familiar \(\Sigma\)-flowchart schemes by replacing the go-to functions by morphisms in T. The morphisms in T represent more complicated computations than those possible with the morphisms in Pfn (i.e. partial functions [n]\(\to [p])\). The author argues that T should be a ``strong iteration theory'', namely an iteration theory [defined by \textit{S. L. Bloom}, \textit{C. C. Elgot} and \textit{J. R. Wright}, SIAM J. Comput. 9, 525-540 (1980; Zbl 0461.68047)] which satisfies an additional implication scheme, called the ``functional dagger'' implication introduced by \textit{M. A. Arbib} and \textit{E. G. Manes} in [J. Algebra 62, 203-227 (1980; Zbl 0429.68021)]. Several theorems are proved. First, a natural `syntactic' congruence \(F\equiv_ dF'\) on flowcharts is defined. Roughly, \(F\equiv_ dF'\) if F can be obtained from F' by a series of steps corresponding to identifying equivalent vertices and eliminating inaccessible vertices. It is shown that F and F' are \(\Sigma\)-schemes over T and if \(F\equiv_ dF'\) then F and F' have the same interpretation in all strong iteration theories. More interestingly, it is shown that if F and F' have the same interpretation in T itself, then T must be a strong iteration theory. Most of the examples of iteration theories of interest to the theory of computation are also strong iteration theories. Several axiomatizations of strong iteration theories are given here and it is noted that free iteration theories (i.e. labeled trees of finite index) are also the free strong iteration theories. The main technical result is that when T is a strong iteration theory, the \(\Sigma\)-schemes over T are the coproduct in the category of strong iteration theories of T and the strong iteration theory freely generated by \(\Sigma\). The author proposes the name Elgot theory for strong iteration theories, on the grounds that Elgot made major contributions to the algebraic study of (deterministic) flowcharts and that a strong iteration theory is ``close in spirit'' to Elgot's iterative theories. I think that Elgot might observe that his main interests were in the equational properties of flowchart algorithms. The functorial dagger implication was therefore not a topic of central concern to him, although he certainly knew of it and found it of interest.