Definable operations in general algebras, and the theory of automata and flowcharts

  • Hans Bekić
Selected Papers Language Definition
Part of the Lecture Notes in Computer Science book series (LNCS, volume 177)


We study the class of operations definable from the given operations of an algebra of sets by union, composition, and fixed points; we obtain two theorems on definable operations that give us as special case the regular-equals-recognisable theorem of generalised finite automata theory. Definable operations arise also as the operations computable by charts; by translating into predicate logic, we obtain Manna's formulas for termination and correctness of flowcharts.


Normal Form Complete Lattice Predicate Logic Free Algebra Spontaneous Move 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    J. W. de Bakker, D. Scott: A theory of programs. — IBM Seminar Vienna, August 1969 (unpublished).Google Scholar
  2. [2]
    M. R. Bird: Binary relations and flow-diagrams. — Memorandum No.11, Sept. 1969, Computer and Logic Research Group, University of Swansea.Google Scholar
  3. [3]
    R. M. Burstall, P. Landin: Programs and their proofs: an algebraic approach. — Machine Intelligence 4, (B. Meltzer, D. Michie Eds.), Edinburgh University Press 1969.Google Scholar
  4. [4]
    P. M. Cohn: Universal algebra. — Harper Row. New York — London 1965.Google Scholar
  5. [5]
    S. Eilenberg, J. B. Wright: Automata in general algebras. — Information and Control 11, 4, Oct. 1967.CrossRefMathSciNetGoogle Scholar
  6. [6]
    G. Grätzer: Universal algebra. — Van Nostrand, Princetown — London 1969.Google Scholar
  7. [7]
    P. Landin: The mechanical evaluation of expressions. — Comp. Journal Jan. 1964.Google Scholar
  8. [8]
    P. Landin: Minimal subalgebras and direct products — a scenario for the theory of computation. — Machine Intelligence 5.Google Scholar
  9. [9]
    Z. Manna: Properties of programs and the first order predicate calculus. — JACM 16, 2, April 1969.CrossRefGoogle Scholar
  10. [10]
    Z. Manna: The correctness of programs. — J. Comp.Syst. Sciences 3, 1969.Google Scholar
  11. [11]
    Z. Manna: The correctness of nondeterministic programs. — A. I. Memo No.95, Stanford University, 1969.Google Scholar
  12. [12]
    Z. Manna, A. Pnueli: Formalisation of properties of recursively defined functions. — A. I. Memo No.82, Stanford 1969.Google Scholar
  13. [13]
    D. Park: Some metatheorems for program equivalence proofs. — Machine Intelligence 5.Google Scholar
  14. [14]
    A. Tarski: A lattice-theoretic fixpoint theorem and its applications. — Pacific J. Math. 5, p. 285–309, 1955.zbMATHMathSciNetGoogle Scholar
  15. [15]
    J. W. Thatcher, J. B. Wright: Generalised finite automata theory with an application to a decision problem of second-order logic. — Math. Syst. Theory, 2, 1, 1968.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Hans Bekić
    • 1
  1. 1.IBM LaboratoryVienna

Personalised recommendations