The equational logic of fixed points
type: Item
instance of: scholarly article
title: The equational logic of fixed points
zbMATH Open document ID: 0920.03067
DOI: 10.1016/S0304-3975(96)00248-4
author: Stephen L. Bloom
author: Zoltán Ésik
published in: Theoretical Computer Science
publication date: 1998-07-22T00:00:00Z
review text: This is a well-written and extensive survey of the universal algebraic approach to the study of fixed points in mathematics generally, and theoretical computer science more particularly. While no proofs of theorems are presented, there are many references to the current literature (175 bibliographic entries), and many examples are given in detail. The remainder of this review is quoted from the authors' Introduction: ``Most computer scientists realize that just about every aspect of their subject involves fixed points. To list but a few familiar examples, context-free grammars are nothing but a system of fixed-point equations over the semiring of languages; circular data type specifications and recursive program schemes are also explicit fixed-point equations; the semantics of flowchart and higher type languages require the existence of certain fixed points; indeed, a ``recursive solution'' is a special kind of ``fixed point''. An entire industry has developed in order to answer questions such as: In what settings can one find solutions of this or that particular fixed-point equation? (The equation \(D=[D \to D]\) comes to mind.) ``This paper is not concerned with questions of the existence or the construction of fixed points. We are concerned with the properties of fixed-point solutions, especially equational properties. We want to emphasize the fact that there is a complete axiomatization of the valid fixed-point identities, namely the axioms for iteration theories. Knowledge of these identities is useful in deriving properties of fixed points. In fact, we think it is just as useful to computer scientists as the knowledge of rings is for students pondering such equations as \((x+a)(x-a)= x^2-a^2\). The fixed-point calculus, consisting of the axioms for fixed points and standard (many-sorted) equational logic ought to be a part of the standard toolkit of theoreticians. The point of this tutorial is to describe several kinds of models for fixed points, discuss some …
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 18C10
Mathematics Subject Classification ID: 08A70
Mathematics Subject Classification ID: 03D75
Mathematics Subject Classification ID: 08B05
Mathematics Subject Classification ID: 06B35
Mathematics Subject Classification ID: 68Q55
zbMATH DE Number: 1178201
zbMATH Keywords: equational theories
zbMATH Keywords: survey
zbMATH Keywords: universal algebraic approach to the study of fixed points
zbMATH Keywords: properties of fixed-point solutions
zbMATH Keywords: complete axiomatization
zbMATH Keywords: fixed-point identities
zbMATH Keywords: iteration theories
zbMATH Keywords: equational logic
reviewed by: Paul Bankston
describes a project that uses: ALGOL 60
MaRDI profile type: Publication
cites work: Fixed-point calculus
cites work: A Theorem on Partially Ordered Sets, With Applications to Fixed Point Theorems
cites work: A menagerie of non-finitely based process semantics over BPA* – from ready simulation to completed traces
cites work: Q4044767
cites work: Least fixed point of a functor
cites work: Q3996444
cites work: Q4222746
cites work: Solving reflexive domain equations in a category of complete metric spaces
cites work: Representations of distributive lattice-ordered semigroups with binary relations
cites work: Q4138875
cites work: Partially additive categories and flow-diagram semantics
cites work: Q3030266
cites work: Q3900995
cites work: Metric interpretations of infinite trees and semantics of non deterministic recursive programs
cites work: Categorical fixed point calculus
cites work: Regular Algebra Applied to Path-finding Problems
cites work: Process Algebra
cites work: Functorial polymorphism
cites work: Order and metric in the stream semantics of elemental concurrency
cites work: Processes and the denotational semantics of concurrency
cites work: Fixed points in Cartesian closed categories
cites work: Fixed points in free process algebras. I
cites work: Q4890705
cites work: Q4348001
cites work: Q3792231
cites work: Q3663501
cites work: Solutions of the Iteration Equation and Extensions of the Scalar Iteration Operation
cites work: Vector Iteration in Pointed Iterative Theories
cites work: Axiomatizing schemes and their behaviors
cites work: Varieties of Iteration Theories
cites work: Equational logic of circular data type specification
cites work: Equational axioms for regular sets
cites work: Matrix and matricial iteration theories. I
cites work: Matrix and matricial iteration theories. II
cites work: Some quasi-varieties of iteration theories
cites work: Solving polynomial fixed point equations
cites work: SOME EQUATIONAL LAWS OF INITIALITY IN 2CCC’S
cites work: Fixed-point operations on ccc's. I
cites work: Notes on equational theories of relations
cites work: Iteration theories of synchronization trees
cites work: Scalar and vector iteration
cites work: Recursion and iteration in continuous theories: the ''M-construction''
cites work: Une remarque sur les systèmes complets d'identités rationnelles
cites work: Une condition impliquant toutes les identités rationnelles
cites work: A complete system of identities for one-letter rational expressions with multiplicities in the tropical semiring
cites work: Q3485876
cites work: A general result on abstract flowchart schemes with applications to the study of accessibility, reduction and minimization
cites work: Q5515373
cites work: Q5639639
cites work: Fundamental properties of infinite trees
cites work: On some classes of interpretations

The equational logic of fixed points (cites work)
cites work: Q4772711

The equational logic of fixed points (cites work)
cites work: On Kleene algebras

The equational logic of fixed points (cites work)
cites work: Q3694724

The equational logic of fixed points (cites work)
cites work: Q4079524

The equational logic of fixed points (cites work)
cites work: Q4091917

The equational logic of fixed points (cites work)
cites work: Matricial theories

The equational logic of fixed points (cites work)
cites work: Structured Programming With and Without go to Statements

The equational logic of fixed points (cites work)
cites work: Q4165484

The equational logic of fixed points (cites work)
cites work: On the algebraic structure of rooted trees

The equational logic of fixed points (cites work)
cites work: Q3919058

The equational logic of fixed points (cites work)
cites work: Q3957911

The equational logic of fixed points (cites work)
cites work: Algebras of iteration theories

The equational logic of fixed points (cites work)
cites work: Q3702515

The equational logic of fixed points (cites work)
cites work: Independence of the equational axioms for iteration theories

The equational logic of fixed points (cites work)
cites work: Q5203698

The equational logic of fixed points (cites work)
cites work: Completeness of Park induction

The equational logic of fixed points (cites work)
cites work: Equational properties of Kleene algebras of relations with conversion

The equational logic of fixed points (cites work)
cites work: Q4222756

The equational logic of fixed points (cites work)
cites work: Q4375811

The equational logic of fixed points (cites work)
cites work: Q3978971

The equational logic of fixed points (cites work)
cites work: Q3138538

The equational logic of fixed points (cites work)
cites work: Recursion-closed algebraic theories

The equational logic of fixed points (cites work)
cites work: Q3698288

The equational logic of fixed points (cites work)
cites work: Regular trees and the free iterative theory

The equational logic of fixed points (cites work)
cites work: Two Families of Languages Related to ALGOL

The equational logic of fixed points (cites work)
cites work: Initial Algebra Semantics and Continuous Algebras

The equational logic of fixed points (cites work)
cites work: Q3738547

The equational logic of fixed points (cites work)
cites work: Q3201767

The equational logic of fixed points (cites work)
cites work: Q3777424

The equational logic of fixed points (cites work)
cites work: Q3746904

The equational logic of fixed points (cites work)
cites work: Q5517672

The equational logic of fixed points (cites work)
cites work: Q3217622

The equational logic of fixed points (cites work)
cites work: Results on the propositional \(\mu\)-calculus

The equational logic of fixed points (cites work)
cites work: Q3358736

The equational logic of fixed points (cites work)
cites work: A completeness theorem for Kleene algebras and the algebra of regular events

The equational logic of fixed points (cites work)
cites work: Monoides et semi-anneaux complets. (Complete monoids and semirings)

The equational logic of fixed points (cites work)
cites work: Matrix versions of aperiodic $K$-rational identities

The equational logic of fixed points (cites work)
cites work: Complete systems of \(\mathcal B\)-rational identities

The equational logic of fixed points (cites work)
cites work: Models of a \(K\)-rational identity system

The equational logic of fixed points (cites work)
cites work: Q3027187

The equational logic of fixed points (cites work)
cites work: Q4038685

The equational logic of fixed points (cites work)
cites work: Automata and languages generalized to \(\omega\)-continuous semirings

The equational logic of fixed points (cites work)
cites work: Q3704880

The equational logic of fixed points (cites work)
cites work: Q3853827

The equational logic of fixed points (cites work)
cites work: A fixpoint theorem for complete categories

The equational logic of fixed points (cites work)
cites work: FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES

The equational logic of fixed points (cites work)
cites work: Q5622402

The equational logic of fixed points (cites work)
cites work: Algebraic structures for transitive closure

The equational logic of fixed points (cites work)
cites work: Algebraic specification of data types: A synthetic approach

The equational logic of fixed points (cites work)
cites work: Towards a foundation for semantics in complete metric spaces

The equational logic of fixed points (cites work)
cites work: Predicate Transformer Semantics

The equational logic of fixed points (cites work)
cites work: Q3735051

The equational logic of fixed points (cites work)
cites work: Q4124327

The equational logic of fixed points (cites work)
cites work: Chain-complete posets and directed sets with applications

The equational logic of fixed points (cites work)
cites work: Q3750114

The equational logic of fixed points (cites work)
cites work: A complete inference system for a class of regular behaviours

The equational logic of fixed points (cites work)
cites work: A complete axiomatisation for observational congruence of finite-state behaviours

The equational logic of fixed points (cites work)
cites work: Q3734395

The equational logic of fixed points (cites work)
cites work: Q5609367

The equational logic of fixed points (cites work)
cites work: Categorical fixed point semantics

The equational logic of fixed points (cites work)
cites work: A completeness theorem for nondeterministic Kleene algebras

The equational logic of fixed points (cites work)
cites work: Q4116078

The equational logic of fixed points (cites work)
cites work: Q3730012

The equational logic of fixed points (cites work)
cites work: Q5624635

The equational logic of fixed points (cites work)
cites work: Q3907077

The equational logic of fixed points (cites work)
cites work: Scott induction and closure under \(\omega\)-sups

The equational logic of fixed points (cites work)
cites work: Q3920613

The equational logic of fixed points (cites work)
cites work: Q4287490

The equational logic of fixed points (cites work)
cites work: A complete axiomatisation for trace congruence of finite state behaviors

The equational logic of fixed points (cites work)
cites work: Q5596826

The equational logic of fixed points (cites work)
cites work: Q5596827

The equational logic of fixed points (cites work)
cites work: Q4273483

The equational logic of fixed points (cites work)
cites work: Q3777490

The equational logic of fixed points (cites work)
cites work: Two Complete Axiom Systems for the Algebra of Regular Events

The equational logic of fixed points (cites work)
cites work: On regular expressions and regular canonical systems

The equational logic of fixed points (cites work)
cites work: Q4155837

The equational logic of fixed points (cites work)
cites work: Q5636307

The equational logic of fixed points (cites work)
cites work: Data Types as Lattices

The equational logic of fixed points (cites work)
cites work: On a Theorem of R. Jungen

The equational logic of fixed points (cites work)
cites work: Nonaxiomatisability of equivalences over finite state processes

The equational logic of fixed points (cites work)
cites work: A characterization of the least-fixed-point operator by dinaturality

The equational logic of fixed points (cites work)
cites work: The Category-Theoretic Solution of Recursive Domain Equations

The equational logic of fixed points (cites work)
cites work: On flowchart theories. I. The deterministic case

The equational logic of fixed points (cites work)
cites work: On flowchart theories. II: The nondeterministic case

The equational logic of fixed points (cites work)
cites work: Q5751953

The equational logic of fixed points (cites work)
cites work: Q3739181

The equational logic of fixed points (cites work)
cites work: A lattice-theoretical fixpoint theorem and its applications

The equational logic of fixed points (cites work)
cites work: Q4185836

The equational logic of fixed points (cites work)
cites work: Q3877027

The equational logic of fixed points (cites work)
cites work: Unique fixed points vs. least fixed points

The equational logic of fixed points (cites work)
cites work: Q4741696

The equational logic of fixed points (cites work)
cites work: Step bisimulation is pomset equivalence on a parallel language without explicit internal choice

The equational logic of fixed points (cites work)
cites work: Q4404457

The equational logic of fixed points (cites work)
cites work: Fixed-point constructions in order-enriched categories

The equational logic of fixed points (cites work)
cites work: Q3794350

The equational logic of fixed points (cites work)
cites work: Synchronization trees

The equational logic of fixed points (cites work)
cites work: Q3141916

The equational logic of fixed points (cites work)
cites work: Q4134935

The equational logic of fixed points (cites work)
cites work: Q4325268

The equational logic of fixed points (full work available at URL)
full work available at URL: s0304-3975(96)00248-4

The equational logic of fixed points (OpenAlex ID)
OpenAlex ID: W2026410426