Man-in-the-Middle (MM) is not only a ubiquitous attack pattern in security, but also an important paradigm of network computation and economics. Recognizing ongoing MM-attacks is an important security task; modeling MM-interactions is an interesting task for semantics of computation. Traced monoidal categories are a natural framework for MM-modelling, as the trace structure provides a tool to hide what happens in the middle. An effective analysis of what has been traced out seems to require an additional property of traces, called normality. We describe a modest model of network computation, based on partially ordered multisets (pomsets), where basic network interactions arise from the monoidal trace structure, and a normal trace structure arises from an iterative, i.e. coalgebraic structure over terms and messages used in computation and communication. The correspondence is established using a convenient monadic description of normally traced monoidal categories.
Game theoretic equilibria are mathematical expressions of rationality. Rational agents are used to model not only humans and their software representatives, but also organisms, populations, species and genes, interacting with each other and with the environment. Rational behaviors are achieved not only through conscious reasoning, but also through spontaneous stabilization at equilibrium points.
Formal theories of rationality are usually guided by informal intuitions, which are acquired by observing some concrete economic, biological, or network processes. Treating such processes as instances of computation, we reconstruct and refine some basic notions of equilibrium and rationality from the some basic structures of computation.
It is, of course, well known that equilibria arise as fixed points; the point is that semantics of computation of fixed points seems to be providing novel methods, algebraic and coalgebraic, for reasoning about them.
Labelled Markov processes (LMPs) are labelled transition systems in
which each transition has an associated probability. In this paper we
present a universal LMP as the spectrum of a commutative C*-algebra
consisting of formal linear combinations of labelled trees. This
yields a simple trace-tree semantics for LMPs that is fully
abstract with respect to probabilistic bisimilarity. We also consider
LMPs with distinguished entry and exit points as stateful stochastic
relations. This allows us to define a category LMP, with
measurable spaces as objects and LMPs as morphisms. Our main result
in this context is to provide a predicate-transformer duality for
LMP that generalises Kozen's duality for the category SRel
of stochastic relations.
We propose a methodology based on testing as a framework to capture the interactions of a machine represented in a denotational
model and the data it manipulates. Using a connection that models ma-
chines on the one hand, and the data they manipulate on the other, test-
ing is used to capture the interactions of each with the objects on the
other side: just as the data that are input into a machine can be viewed
as tests that the machine can be subjected to, the machine can be viewed
as a test that can be used to distinguish data. This approach is based on
generalizing from duality theories that now are common in semantics to
logical connections, which are simply contravariant adjunctions. In the
process, it accomplishes much more than simply moving from one side
of a duality to the other; it faithfully represents the interactions that
embody what is happening as the computation proceeds.
Our basic philosophy is that tests can be used as a basis for modeling
interactions, as well as processes and the data on which they operate. In
more abstract terms, tests can be viewed as formulas of process logics,
and testing semantics connects processes and process logics, and assigns
computational meanings to both.
Labelled Markov processes (LMPs) are probabilistic labelled
transition systems. In this paper we present a `universal' LMP
as the Stone-Gelfand-Naimark dual of a C*-algebra consisting of
formal linear combinations of labelled trees. We characterize the
state space of the universal LMP as the set of homomorphims from
an ordered commutative monoid of labelled trees into the
multiplicative unit interval. This yields a simple semantics for
LMPs which is fully abstract with respect to probabilistic
bisimilarity. We also consider LMPs with entry points and exit
points in the framework of Elgot's iterative theories. We define an
iterative theory of LMPs by specifing its categorical dual: a
category of commutative rings consisting of C*-algebras of trees
and `shapely maps' between them. We find that the basic operations
for composing LMPs have simple definitions in the dual category.
We define the continuum in terms of the final coalgebras of simple
functors: either the functor N×X , mapping the sets X into their
products with the set of natural numbers, or the functor 1+N ×X. This
makes an attractive analogy with the definition of
N itself as the initial algebra of the functor 1+X, which adds a
singleton to each set X. We furthermore characterize Baire space and
Cantor space in terms of these final coalgebras.
The presented coalgebraic approach leads to coinductive definitions of
these infinitary concepts both in the category of sets, and in the
category of posets. We analyze the structural differences that arise,
and conclude with some paradoxical discrepancies between continuity
and constructiveness in this setting.
Abstract Simulations between processes can be
understood in terms of coalgebra homomorphisms, with homomorphisms to
the final coalgebra exactly identifying bisimilar processes. The
elements of the final coalgebra are thus natural representatives of
bisimilarity classes, and a denotational semantics of processes can be
developed in a final-coalgebra-enriched category where arrows are
processes, canonically represented.
In the present paper, we describe a general framework for building
final-coalgebra-enriched categories. Every such category is
constructed from a multivariant functor representing a notion of
process, much like Moggi's categories of computations arising from
monads as notions of computation. The "notion of process" functors are
intended to capture different flavors of processes as dynamically
extended computations. These functors may involve a computational
(co)monad, so that a process category in many cases contains an
associated computational category as a retract. We further discuss
categories of resumptions and of hyperfunctions, which are the main
examples of prcess categories. Very informally, resumptions can be
understood as computations extended in time, whereas hypercomputations
are extended in space.
Abstract The technique of build fusion, also
known as deforestation, removes intermediate results in a
composition involving the "build" of an initial (inductive,
finite) data structure, followed by its consumption. Here we show that
it is analogously possible to do process fusion, removing
intermediate final (coinductive, potentially infinite) data
passing between a producer and a consumer.
The key observation leading to our results is the fact that the
Curry-Howard isomorphism, relating types to propositions, programs to
proofs, and sequential composition to cut, extends to the
correspondence of fusion to cut elimination. this
simple idea gives us logical interpretations of the basic methods of
generic and transformational programming. In the present paper, we
provide a logical analysis of the general form of build
fusion over the inductive data types, regular or nested. The
analysis is based on a novel logical interpretation of parametricity
in terms of the paranatural transformations, introduced in
the paper. We extend it to cover process fusion on
coinductive data types.
The results obtained are truly generic, in the sense of applying to
all coinductive (final) data types, including nested ones, and allow a
far wider range of optimizations than previously possible. By the
standard embedding of initial into final data types, it also applies
to arbitrary intial-final mixtures (e.g., infinitely unfolding trees
of finite lists).
We define the continuum up to order isomorphism (and hence
homeomorphism) as the final coalgebra of the functor capturing the
ordinal product with omega. This makes an attractive analogy with the
definition of the ordinal omega itself as the initial algebra of the
functor prepending the unity, with both definitions made in the
category of posets. The variants of these functors yield respectively
Cantor space (surplus rationals), Baire space (no rationals), and
again the continuum as their final coalgebras.
Coinduction is often seen as a way of implementing infinite
objects. Since real numbers are typical
infinite objects, it may not come as a surprise that calculus, when
presented in a suitable way, is permeated by coinductive reasoning.
What is surprising is that mathematical techniques, recently
developed in the context of computer science, seem to be shedding a
new light on some basic methods of calculus.
We introduce a coinductive formalization of elementary calculus that
can be used as a tool for symbolic computation, and geared towards
computer algebra and theorem proving. So far, we have covered
ordinary differential and difference equations, Taylor series, Laplace
transform and the basics of operator calculus.
We make an initial step towards categorical semantics of guarded
induction. While ordinary induction is usually modelled in
terms of least fixpoints and initial algebras, guarded induction is
based on unique fixpoints of certain operations, called
guarded, on final coalgebras. So far, such operations were
treated syntactically. We analyse
them categorically. Guarded induction appears as couched in
The applications of the presented categorical analysis span across the
gamut of the applications of coinduction, from modelling of
computation to solving differential equations. A subsequent paper will
provide an account of some domain theoretical aspects, which are
presently left implicit.