Skip to main content
main-content

Über dieses Buch

This monograph contains the results of our joint research over the last ten years on the logic of the fixed point operation. The intended au­ dience consists of graduate students and research scientists interested in mathematical treatments of semantics. We assume the reader has a good mathematical background, although we provide some prelimi­ nary facts in Chapter 1. Written both for graduate students and research scientists in theoret­ ical computer science and mathematics, the book provides a detailed investigation of the properties of the fixed point or iteration operation. Iteration plays a fundamental role in the theory of computation: for example, in the theory of automata, in formal language theory, in the study of formal power series, in the semantics of flowchart algorithms and programming languages, and in circular data type definitions. It is shown that in all structures that have been used as semantical models, the equational properties of the fixed point operation are cap­ tured by the axioms describing iteration theories. These structures include ordered algebras, partial functions, relations, finitary and in­ finitary regular languages, trees, synchronization trees, 2-categories, and others.

Inhaltsverzeichnis

Frontmatter

Introduction

Abstract
Iteration theories arose from an investigation of certain structures which occur in the syntax and semantics of the class of flowchart algorithms. These algorithms derive their name from the fact that they may be described by means of certain labeled directed graphs, the flowcharts. Descriptions by means of a list of labeled instructions are also possible. One example of a flowchart algorithm is the following familiar method to compute the n-th power of a positive integer m.
Stephen L. Bloom, Zoltán Ésik

Chapter 1. Preliminary Facts

Abstract
In this chapter, we establish our notation and review several concepts needed throughout the book. We assume that the reader has some familiarity with basic universal algebra and elementary category theory.
Stephen L. Bloom, Zoltán Ésik

Chapter 2. Varieties and Theories

Abstract
We will review briefly some of the main concepts of standard universal algebra in order to motivate the definition of one of our central concepts: algebraic theories. We will show how theories are related to equational classes of algebras. Most of the facts mentioned in this chapter are well-known in some form.
Stephen L. Bloom, Zoltán Ésik

Chapter 3. Theory Facts

Abstract
In this chapter we collect some technical results about the category TH of theories, as well as document some observations which will be used frequently in later chapters. In the last section, we introduce the concept of a 2-theory.
Stephen L. Bloom, Zoltán Ésik

Chapter 4. Algebras

Abstract
In this chapter, we show how each theory T determines a category T of T-algebras. Each such category is an abstraction of the notion of a variety of ∑-algebras. The category whose objects are the varieties T and whose morphisms are functors which commute with the underlying set functors is shown to be dually isomorphic to the category of theories and theory morphisms.
Stephen L. Bloom, Zoltán Ésik

Chapter 5. Iterative Theories

Abstract
In this chapter, we define both ideal and iterative theories. The main definitions are in Sections 1 and 2. Section 3 has a more technical nature, and most details may be omitted at first reading. However, the results of Section 3 will be applied in later sections.
Stephen L. Bloom, Zoltán Ésik

Chapter 6. Iteration Theories

Abstract
Iteration theories are a generalization of iterative theories. In iteration theories, the dagger operation can be applied to all morphisms f: nn + p, producing a canonical solution of the iteration equation for f. The properties of iteration are captured equationally.
Stephen L. Bloom, Zoltán Ésik

Chapter 7. Iteration Algebras

Abstract
In Chapter 4 we discussed the algebras of an arbitrary theory. This chapter deals with the algebras of (pre)iteration theories. When T is a preiteration theory, not all T-algebras respect the iteration operation. We say that a T-algebra д = (A, α) is a T-iteration algebra whenever the kernel of the theory morphism α: TPow A is a dagger congruence.
Stephen L. Bloom, Zoltán Ésik

Chapter 8. Continuous Theories

Abstract
In the first three sections of this chapter we consider theories whose hom-sets are equipped with a partial order which is compatible with the theory operations; iteration is defined using least fixed points. An ordered theory is a special kind of 2-theory, one in which there is a vertical morphism fg iff f ω g. In Section 4, the connection between initiality and the fixed point properties of iteration is examined in the context of 2-theories. We consider the properties of initial f-algebras, for horizontal morphisms f in a 2-theory. Many properties of iteration theories hold when all such initial algebras exist. In the last section, some of the constructions for ω-continuous ordered theories are generalized to ω-continuous 2-theories. In particular, it is shown how any ω-continuous 2-theory determines an iteration theory.
Stephen L. Bloom, Zoltán Ésik

Chapter 9. Matrix Iteration Theories

Abstract
Matrix theories were discussed in Section 3.5. We proved there that each matrix theory is isomorphic to a matrix theory Mat S , for some semiring S. Hence in this chapter we will consider only these theories. When the matrix theory T = Mat S is a preiteration theory, then one can define a star operation on each hom-set T(n, n) as follows. When A is n × n, the matrix [A 1 n ] is a morphism nn + nin T, and we define A* by the equation
$$ A* = \left[ {A\,1_n } \right]^\dag $$
(1)
Stephen L. Bloom, Zoltán Ésik

Chapter 10. Matricial Iteration Theories

Abstract
Recall the definition of matricial theories from Section 3.5.3. Since each matricial theory can be represented as a theory Matr(S; V) for some semiring module pair (S;V), we will be considering only matricial theories of this sort. A matricial iteration theory is a matricial theory which is simultaneously an iteration theory. We show that when T = Matr(S; V) is a matricial iteration theory, the dagger operation determines and is determined by a star operation on the semiring S and an omega operation ω: SV from the semiring to the module.
Stephen L. Bloom, Zoltán Ésik

Chapter 11. Presentations

Abstract
In this chapter, we define a general notion of presentation, applicable to all Conway or iteration theories. We state and prove a general version of Kleene’s theorem. We then apply presentations to give a necessary and sufficient condition that an iteration theory is the coproduct of an iteration theory and a free iteration theory. This technical result will be used in the axiomatization results of Chapters 12 and 13.
Stephen L. Bloom, Zoltán Ésik

Chapter 12. Flowchart Behaviors

Abstract
This chapter deals with the structures which serve as the standard models for (functorial) flowchart semantics. Recall from Example 11.1.7 that one can identify a flowchart scheme np with a presentation D = (α; a) in a free tree theory ∑tr. (Here α is a partial base morphism and each component of a is the composite of an atomic tree with a partial base morphism.) Thus, if T is any iteration theory and φ: ∑ → T is any function mapping letters in ∑ n to morphisms 1 → n in T, n > 0, φ extends uniquely to both a theory morphism ∑trT and also to a morphism of presentations:
$$ D\varphi : = \left( {\alpha ;a\varphi } \right). $$
Stephen L. Bloom, Zoltán Ésik

Chapter 13. Synchronization Trees

Abstract
Synchronization trees were used by Milner as models of the computation of communicating processes. More accurately, it was the equivalence classes of trees under the relation of bisimulation which were his primary focus. He conjectured that with a different treatment of variables, his work might fit into the framework of iterative theories.
Stephen L. Bloom, Zoltán Ésik

Chapter 14. Floyd-Hoare Logic

Abstract
Suppose that f: QQ is a partial function on a set Q, where we might think of Q as a set of “states” of a machine. If α and β are predicates on Q, i.e. total maps Q → {TRUE, FALSE}, partial correctness assertion {α} f {β}, pca for short, means
$$ \forall q \in Q\left[ {\alpha \left( q \right) = {\text{TRUE}}\, \wedge f\left( q \right){\text{defined}}\, \Rightarrow \beta \left( {f\left( q \right) = {\text{TRUE}}} \right)} \right] $$
.
Stephen L. Bloom, Zoltán Ésik

Backmatter

Weitere Informationen