# zbMATH — the first resource for mathematics

On flowchart theories. I. The deterministic case. (English) Zbl 0628.68018
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 S. L. Bloom, C. C. Elgot and 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 M. A. Arbib and 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.
Reviewer: S.Bloom

##### MSC:
 68Q60 Specification and verification (program logics, model checking, etc.)
##### Keywords:
flowchart schemes; iteration theories
Full Text:
##### References:
  Goguen, J.A.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Initial algebra semantics and continuous algebras, J. assoc. comput. Mach., 24, 68-95, (1977) · Zbl 0359.68018  Wagner, E.G.; Wright, J.B.; Goguen, J.A.; Thatcher, J.W., Some fundamentals of order algebraic semantics, (), 153-168 · Zbl 0361.68041  Wright, J.B.; Thatcher, J.W.; Wagner, E.G.; Goguen, J.A., Rational algebraic theories and fixed-point solutions, (), 147-158  Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Notes on algebraic fundamentals for theoretical computer science, (), 83-164  Arbib, M.A.; Manes, E.G., Partially additive categories and flow-diagram semantics, J. algebra, 62, 203-227, (1980) · Zbl 0429.68021  Backus, J.W., Can programming be liberated from the von Neumann style? A functional style and its algebra of program, Comm. ACM, 21, 61341, (1978)  Backus, J.W., From function level semantics to program transformation and optimization, (), 60-91  Bloom, S.L.; Elgot, C.C., The existence and construction of free iterative theories, J. comput. system sci., 12, 305-318, (1976) · Zbl 0333.68017  Bloom, S.L.; Elgot, C.C.; Tindell, R., On the algebraic structure of rooted trees, J. comput. system sci., 16, 362-399, (1978) · Zbl 0389.68007  Bloom, S.L.; Elgot, C.C.; Wright, J.B., Solutions of the iteration equations and extensions of the scalar iteration operation, SIAM J. comput., 9, 25-45, (1980) · Zbl 0454.18011  Bloom, S.L.; Elgot, C.C.; Wright, J.B., Vector iteration in pointed iterative theories, SIAM J. comput., 9, 525-540, (1980) · Zbl 0461.68047  Bloom, S.L.; Esik, Z., Axiomatizing schemes and their behaviours, J. comput. system sci., 31, 375-393, (1985) · Zbl 0613.68013  Căzănescu, V.E., On context-free trees, Theoret. comput. sci., 41, 33-50, (1985) · Zbl 0603.68084  Căzănescu, V.E.; Ungureanu, C., Again on advice on structuring compilers and proving them correct, INCREST preprint series in mathematics no. 75, (1982)  Courcelle, B., Fundamental properties of infinite trees, Theoret. comput. sci., 25, 95-169, (1983) · Zbl 0521.68013  Elgot, C.C., Algebraic theories and program schemes, () · Zbl 0123.33502  Elgot, C.C., Monadic computation and iterative algebraic theories, (), 175-230 · Zbl 0327.02040  Elgot, C.C.; Elgot, C.C., Erratum and corrigendum, IEEE trans. software eng., IEEE trans. software eng., SE-2, 41-53, (September 1976)  Elgot, C.C.; Shepherdson, J.C., An equational axiomatization of the algebra of reducible flowchart schemes, IBM research report RC 8221,, (April 1980)  Esik, Z., Identities in iterative and rational theories, comput, Comput. linguistic and comput. language, 14, 183-207, (1980) · Zbl 0466.68010  Esik, Z., Algebras of iteration theories, J. comput. system sci., 27, 291-303, (1983) · Zbl 0532.68011  Esik, Z., Independence of the equational axioms for iteration theories, (1984), draft paper · Zbl 0649.68010  Ginali, S., Regular trees and free iterative theory, J. comput. system sci., 18, 228-242, (1979) · Zbl 0495.68042  Greirach, S., Theory of program structures: schemes, semantics, verification, (1975), Springer-Verlag Berlin/Heidelberg/New York  Knuth, D.E.; Floyd, R.W., Notes on avoiding “go to” statements, Inform. process. lett., 1, 23-31, (1971) · Zbl 1260.68047  Kosaraju, S.Rao, Analysis of structured programs, J. comput. system sci., 9, 232-255, (1974) · Zbl 0293.68014  Kotov, V.E., Introduction to the theory of program schemes, (1978), Nauka Novosibirsk, [Russian]  Kotov, V.E., Petri nets, (1984), Nauka Moskva, [Russian] · Zbl 0606.68052  Lawvere, F.W., Functorial semantics of algebraic theories, (), 869-872 · Zbl 0119.25901  Lorentz, R.J.; Benson, D.B., Deterministic and nondeterministic flowchart interpretations, J. comput. system. sci., 27, 400-433, (1983) · Zbl 0544.68010  Manes, E.G., Algebraic theories, (1976), Springer-Verlag Berlin/New York · Zbl 0489.18003  Manna, Z., Mathematical theory of computation, (1976), McGraw-Hill New York  \scGH. Ştefănescu “On Flowchart Theories,” (I)INCREST Preprint Series in Mathematics Nos. 39/1984 and 7/1985.  \scGH. Ştefănescu, “On Flowchart Theories II (Nondeterministic Case),” INCREST Preprint Series in Mathematics No. 32/1985; Theoret. Comput. Sci., in press.  Stop, J.E., Denotational semantics: the Scott-strachey approach to programming language theory, (1977), MIT Press Cambridge, MA/London  Troeger, D.R., Metric iteration theories, Fund. inform., 5, 187-216, (1982) · Zbl 0504.68020
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.