On flowchart theories. I. The deterministic case.

*(English)*Zbl 0628.68018The 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.

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.) |

PDF
BibTeX
XML
Cite

\textit{G. Ştefănescu}, J. Comput. Syst. Sci. 35, 163--191 (1987; Zbl 0628.68018)

Full Text:
DOI

##### References:

[1] | 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 |

[2] | Wagner, E.G.; Wright, J.B.; Goguen, J.A.; Thatcher, J.W., Some fundamentals of order algebraic semantics, (), 153-168 · Zbl 0361.68041 |

[3] | Wright, J.B.; Thatcher, J.W.; Wagner, E.G.; Goguen, J.A., Rational algebraic theories and fixed-point solutions, (), 147-158 |

[4] | Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Notes on algebraic fundamentals for theoretical computer science, (), 83-164 |

[5] | Arbib, M.A.; Manes, E.G., Partially additive categories and flow-diagram semantics, J. algebra, 62, 203-227, (1980) · Zbl 0429.68021 |

[6] | 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) |

[7] | Backus, J.W., From function level semantics to program transformation and optimization, (), 60-91 |

[8] | 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 |

[9] | 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 |

[10] | 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 |

[11] | 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 |

[12] | Bloom, S.L.; Esik, Z., Axiomatizing schemes and their behaviours, J. comput. system sci., 31, 375-393, (1985) · Zbl 0613.68013 |

[13] | Căzănescu, V.E., On context-free trees, Theoret. comput. sci., 41, 33-50, (1985) · Zbl 0603.68084 |

[14] | 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) |

[15] | Courcelle, B., Fundamental properties of infinite trees, Theoret. comput. sci., 25, 95-169, (1983) · Zbl 0521.68013 |

[16] | Elgot, C.C., Algebraic theories and program schemes, () · Zbl 0123.33502 |

[17] | Elgot, C.C., Monadic computation and iterative algebraic theories, (), 175-230 · Zbl 0327.02040 |

[18] | Elgot, C.C.; Elgot, C.C., Erratum and corrigendum, IEEE trans. software eng., IEEE trans. software eng., SE-2, 41-53, (September 1976) |

[19] | Elgot, C.C.; Shepherdson, J.C., An equational axiomatization of the algebra of reducible flowchart schemes, IBM research report RC 8221,, (April 1980) |

[20] | Esik, Z., Identities in iterative and rational theories, comput, Comput. linguistic and comput. language, 14, 183-207, (1980) · Zbl 0466.68010 |

[21] | Esik, Z., Algebras of iteration theories, J. comput. system sci., 27, 291-303, (1983) · Zbl 0532.68011 |

[22] | Esik, Z., Independence of the equational axioms for iteration theories, (1984), draft paper · Zbl 0649.68010 |

[23] | Ginali, S., Regular trees and free iterative theory, J. comput. system sci., 18, 228-242, (1979) · Zbl 0495.68042 |

[24] | Greirach, S., Theory of program structures: schemes, semantics, verification, (1975), Springer-Verlag Berlin/Heidelberg/New York |

[25] | Knuth, D.E.; Floyd, R.W., Notes on avoiding “go to” statements, Inform. process. lett., 1, 23-31, (1971) · Zbl 1260.68047 |

[26] | Kosaraju, S.Rao, Analysis of structured programs, J. comput. system sci., 9, 232-255, (1974) · Zbl 0293.68014 |

[27] | Kotov, V.E., Introduction to the theory of program schemes, (1978), Nauka Novosibirsk, [Russian] |

[28] | Kotov, V.E., Petri nets, (1984), Nauka Moskva, [Russian] · Zbl 0606.68052 |

[29] | Lawvere, F.W., Functorial semantics of algebraic theories, (), 869-872 · Zbl 0119.25901 |

[30] | Lorentz, R.J.; Benson, D.B., Deterministic and nondeterministic flowchart interpretations, J. comput. system. sci., 27, 400-433, (1983) · Zbl 0544.68010 |

[31] | Manes, E.G., Algebraic theories, (1976), Springer-Verlag Berlin/New York · Zbl 0489.18003 |

[32] | Manna, Z., Mathematical theory of computation, (1976), McGraw-Hill New York |

[33] | \scGH. Ştefănescu “On Flowchart Theories,” (I)INCREST Preprint Series in Mathematics Nos. 39/1984 and 7/1985. |

[34] | \scGH. Ştefănescu, “On Flowchart Theories II (Nondeterministic Case),” INCREST Preprint Series in Mathematics No. 32/1985; Theoret. Comput. Sci., in press. |

[35] | Stop, J.E., Denotational semantics: the Scott-strachey approach to programming language theory, (1977), MIT Press Cambridge, MA/London |

[36] | 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.