Definable operations in general algebras, and the theory of automata and flowcharts
- 165 Downloads
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.
KeywordsNormal Form Complete Lattice Predicate Logic Free Algebra Spontaneous Move
Unable to display preview. Download preview PDF.
- J. W. de Bakker, D. Scott: A theory of programs. — IBM Seminar Vienna, August 1969 (unpublished).Google Scholar
- M. R. Bird: Binary relations and flow-diagrams. — Memorandum No.11, Sept. 1969, Computer and Logic Research Group, University of Swansea.Google Scholar
- 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
- P. M. Cohn: Universal algebra. — Harper Row. New York — London 1965.Google Scholar
- G. Grätzer: Universal algebra. — Van Nostrand, Princetown — London 1969.Google Scholar
- P. Landin: The mechanical evaluation of expressions. — Comp. Journal Jan. 1964.Google Scholar
- P. Landin: Minimal subalgebras and direct products — a scenario for the theory of computation. — Machine Intelligence 5.Google Scholar
- Z. Manna: The correctness of programs. — J. Comp.Syst. Sciences 3, 1969.Google Scholar
- Z. Manna: The correctness of nondeterministic programs. — A. I. Memo No.95, Stanford University, 1969.Google Scholar
- Z. Manna, A. Pnueli: Formalisation of properties of recursively defined functions. — A. I. Memo No.82, Stanford 1969.Google Scholar
- D. Park: Some metatheorems for program equivalence proofs. — Machine Intelligence 5.Google Scholar