A coinductive approach to digital computation

Ulrich Berger


We present digit spaces and their coinductively defined morphisms as an abstract approach to digital computation. A digit space is a set X together with a set D of functions, from X to X. The elements of D are called digits. A standard example of a digit system is the compact real interval I = [-1,1] together with the functions av_i : I -> I (i = -1,0,1) defined by av_i(x) = (x+i)/2. This digit space corresponds to the well-known binary signed digit representation of real numbers in [-1,1] which has been extensively studied in exact real number computation, type theory and domain theory.

Our approach contains two novelties:

1. We define coinductively a set of morphisms between digit spaces which, in the standard cases, coincides with the set of uniformly continuous functions.

2. We use the proof-theoretic technique of program extraction to automatically synthesise from constructive proofs lazy algorithms for these morphisms.

We show how constructive analysis and corresponding certified algorithms can be developed in this approach.

Structures similar to digit spaces are known as iterated function systems in the theory of dynamical systems and fractals. Since our theory has different goals we chose a different name.

Thursday 16th October 2008, 14:00
Robert Recorde Room
Department of Computer Science