文档介绍：Preface
The #-calculus is basically an algebra of monotonic functions over -
plete lattice, whose basic constructors are position and least
and greatest fixed point operators. In some sense, the #-calculus naturally
extends the concept of an inductive definition, mon in mathemat-
ical practice. An object defined by induction, typically a set, is obtained as
a least fixed point of some monotonic operator, usually over a powerset lat-
tice. For example, the set of theorems of a formal theory is the least fixed
point of the consequence operator. For some concepts, however, the use of
co-induction, . of greatest fixed points is more appropriate. For example,
a maximal dense-in-itself subspace of a topological space can be defined as
the greatest fixed point of the derivative operator. In the #-calculus, both
least and greatest fixed points are considered, but, more importantly, their
occurrences can be nested and mutually dependent. The alternation between
the least and greatest fixed-point operators is a source of a sharp expres-
sive power of the #-calculus and gives rise to a proper hierarchy, just as the
alternation of quantifiers is the basis of strength of first-order logic.
The #-calculus emerged from numerous works of logicians puter
scientists and its use has mon in the works about verification
puter programs because it provides a simple way of expressing and
checking their behavioural properties. In the literature, the most popular
reference is perhaps the modal #-calculus introduced by Kozen [55]; let us also
mention prior works by Scott and de Bakker [88], Moschovakis [64], Emerson
and Clarke [36], Park [80], and Pratt [82]. Indeed, there is a wide variety of
phenomena that can be modeled in the #-calculus, from finite automata and
regular expressions, to alternating automata on infinite trees or, even more
generally, infinite games with finitely presentable winning conditions.
From a point of view p