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.

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.

Technically, the task thus requires combining functionalities of automated software development tools and of runtime environments. Such combinations lead not just to challenging engineering problems, but also to novel theoretical questions. Formal methods are needed, and the standard techniques do not suffice.

As a first contribution in this direction, we present a basic mathematical framework suitable for describing self-adaptive software at a high level of semantical abstraction. A static view leads to a structure akin to the Chu construction. An dynamic view is given by a coalgebraic presentation of adaptive transducers.

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.

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).

The familiar semantic characterization of parametricity in the algebraic case is expressed in terms of the free functor, i.e. using the initial models. In the general case, the initial models may not exist, and the free functor is not available. Various syntactic, semantic and abstract definitions of parametricity have been offered, but their exact relationships are often unclear. Using the methods of categorical model theory, we establish the equivalence of two well known, yet so far unrelated definitions of parametricity, one syntactic, one semantic. Besides providing support for both underlying views, and a way for aligning the systems based on each of them, the offered general analysis and its formalism open up several avenues for future research and applications.

Using the proposed constructions, interaction categories can be built and analysed without fixing a set of axioms for them. They are thus approached via specifications, just like algebras are approached via equations and relations, independantly of the intrinsic characterisation of varieties.

In the present paper, the well-known categorical semantics of the lambda-calculus is generalised to the action calculus. A suitable functional completeness theorem for symmetric monoidal categories is proved: we determine the conditions under which the abstraction is definable. Algebraically, the distinction between the variables and the names boils down to the distinction between the transcendental and the algebraic elements. The former lead to the polynomial extensions, like e.g. the ring Z[x], the latter to the algebraic extensions like Z[i].

Building upon the work of P. Gardner, we introduce action categories, and show that they are related to the static action calculus exacly as cartesian closed categories are related to the lambda-calculus. Natural examples of this structure arise from allegories and cartesian bicategories. On the other hand, the free algebras for any commutative Moggi monad form an action category. The general correspondence of action calculi and Moggi monads will be worked out in a sequel to this work.

In the present paper, we extend this representation to asynchronous processes, namely modulo the weak and the branching bisimulations and congruences. They are shown to correspond to interesting subcategories of the category of labelled irredundant trees. The form of the representatives in the case of the branching bisimilarity suggests possible connections with game theory. An abstract construction of a category of processes in a general setting is presented in the appendix.

The sequel of this paper will address the issues of asynchronicity, preemption, noninterleaving and linear logic in the same setting.

In the present paper, we describe a category of processes modulo strong bisimulations, with the bisimilarity preserving simulations as morphisms, and show that it is equivalent to the category of labelled irredundant trees and the label preserving tree morphisms. The developed representation turns out to be applicable to weaker notions of process as well. They will be studied in the sequel.