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.

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.

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

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.

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.