Kahn Networks for Exact Real Computation

Michal Konečný, Amin Farjudian


A domain-theoretical denotational framework is provided in which the behaviour of networks can be analysed and studied compositionally. The networks considered here are discrete-time with a global clock and the communication on each channel adheres to some query-response protocol, leading to a form of lazy evaluation. Although the setting is presented in a very general abstract manner (i.e. no language or set of data-types is fixed for the main theory), our motivation and examples focus on exact real number computation. The generality is meant to enable the incorporation of various approaches to exact real computation, e.g. that of Edalat and Potts (2000), Escardo (1997), Bohm and Cartwright (1986), to name a few. Nevertheless, multi-valued computation is not yet included.

Exact computation over real numbers - especially in higher orders - seems to be inherently resource hungry, hence can benefit from distributed computation. This in turn raises the challenge of specifying protocols for passing higher order data through the channels of a network. To enable a semantical view of such communication, we provide tools to define protocols in which queries and responses are modelled in appropriate lattices and domains. Moreover, from such semantics of queries and responses naturally arises a generalisation of the notion of speed of convergence.

Our main aim is to provide tools for compositional reasoning, i.e. we analyse how properties of a composed network can be derived from properties of individual components. We give two results of this nature, one about partial correctness of composed semantics and one about responsiveness (i.e. liveness).

AERN-Net: prototype implementation in Haskell
example query-answer network traces presented as causality trees (produced using AERN-Net): (these interactive views work in recent versions of Firefox, in other browser probably not)
Michal Konečný
Last modified: Tue Dec 9 11:15:40 GMT 2008