Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

1993 | Buch

Introduction Kapitel lesen Erstes Kapitel lesen

Iteration Theories

The Equational Logic of Iterative Processes

verfasst von: Stephen L. Bloom, Zoltán Ésik

Verlag: Springer Berlin Heidelberg

Buchreihe : Monographs in Theoretical Computer Science. An EATCS Series

Enthalten in: Professional Book Archive

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Ü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: n → n + 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 α: T → Pow 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 f → g 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 n→n + 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 ω: S → V 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 n → p 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 ∑tr → T 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: Q → Q 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
Metadaten
Titel
Iteration Theories
verfasst von
Stephen L. Bloom
Zoltán Ésik
Copyright-Jahr
1993
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-78034-9
Print ISBN
978-3-642-78036-3
DOI
https://doi.org/10.1007/978-3-642-78034-9