A Program Calculus for Dynamical Systems
Patrick Weigert

Abstract:
We develop a type theory for dynamical systems seen as computational processes. Denotational semantics for dynamical systems are constructed from ‘‘finitary approximations’’ to them, via domain theory. We study the resulting categories of domains, characterise them via certain free constructions, and derive two type theories from them, using techniques from categorical logic. The first theory, obtained from a free construction, is designed to be sound and complete with respect to a finitary fragment of the category; the second is a sound infinitary extension that can express all computable functions. We finish by sketching two applications: a programming language for manipulating dynamical systems, and a logical framework for reasoning about properties of those systems. The work exemplifies a general approach for deriving formal reasoning tools about a computational situation from a suitable category of domains.