An Equational Axiomatization of the Algebra of Reducible Flowchart Schemes

Calvin C. Elgot and John C. Shepherdson
Additional contact information
Calvin C. Elgot: IBM Thomas J. Watson Research Center, Mathematical Sciences Department
John C. Shepherdson: University of Bristol, Department of Mathematics

A chapter in Selected Papers, 1982, pp 361-409 from Springer

Abstract: Abstract The flowchart schemes called “reducible” are of interest because (1) they schematize programs without “go to” statements; (2) for every flowchart scheme there is a reducible one which is step-by-step equivalent to it; (3) they manipulate readily. The reducible flowchart schemes admit both graph-theoretic and algebraic descriptions. A flowchart scheme F with n begins and p exits is reducible iff both (a) for every vertex v there is a begin-path (i.e. a path from a begin vertex) which ends in v (b) for every closed path C there is a vertex vC of C such that every begin path to a vertex of C meets vC. Algebraically: F is reducible iff it can be built up from atomic flowchart schemes (which may be thought of as corresponding to single instructions) and surjective trivial flowchart schemes (which may be thought of as redirecting flow of control) by means of composition (∘), separated pairing (+), and scalar iteration (†). Dropping † yields the accessible, acyclic flowchart schemes. The equational axioms referred to in the title relate ≈-identified (i.e. isomorphism-identified) flowchart schemes by these three operations. The structure freely generated by the set Γ of atomic flowchart schemes is Γ Red, the theory (or multi-sorted algebra) of reducible flowchart schemes. The axioms involving only + and ∘ yield ΓAc, the theory of accessible, acyclic flowchart schemes. Semantical domains which may be used to interpret Γ Red also satisfy these axioms. The set of equational statements true for Γ Red (which are also logical consequences of the axioms) determine a congruence on the algebra of expressions built out of Γ, Sur, +, ∘ and † whose quotient is another description of Γ Red. Thus the expressions built up using these three operations provide an alternative notation for reducible flowchart programs; the purpose of the axioms is to determine when two expressions represent the same schematic program. A similar statement holds for ΓAc.

Keywords: Normal Factorization; Flow Theory; Component Flow; External Edge; Left Factor (search for similar items in EconPapers)
Date: 1982
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-1-4613-8177-8_12

Ordering information: This item can be ordered from
http://www.springer.com/9781461381778

DOI: 10.1007/978-1-4613-8177-8_12

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().