3.jaan, 14:00 ICT-A2 "From infinity to interaction" (Lõpmatusest interaktsioonini)
Tarkvarateaduse instituudi seminaril neljapäeval, 03.01.2019 kell 14:00 esineb Venanzio Capretta (Nottinghami Ülikool, Ühendkuningriik) teemal "From infinity to interaction" (Lõpmatusest interaktsioonini).
Seminar toimub ruumis ICT-A2.
From infinity to interaction
A new paradigm of software development is emerging: the application of mathematical theories of infinite objects to model complex computational systems.
The traditional account of computation conceived programs as maps from an input to an output, working on a finite memory for a finite time. Modern systems do not comply with this narrative: they consist instead of processes that run indefinitely, receive signals and produce responses continuously, operating in an ever-changing environment. A mathematics of infinity is required to give a authentic representation of this domain.
Classical theories of infinity describe abstract entities that exist only in an idealized world. A constructive and computational approach is needed. The modern theory of coalgebras and coinductive types offers a fertile path in this direction. It models infinite entities as the limit unfoldings of structure-generating maps. The generality of the categorical setting allows us to specify a wide spectrum of formal structures.
The most widely used coinductive type is that of streams: infinite sequences of values. They clearly model continuous processes that produce an unending flow of results. Their theory is fairly well understood, although some fundamental properties have been proved only recently: for example the undecidability of pure stream functions and the inconsistency of their continuity in type theory.
Pure streams are not yet sufficient for an appropriate modelling of modern software: they do not take into account interaction with a user or other processes, non-deterministic computations, possible cloning of processes, parallelism or (in the future) quantum phenomena. We must be able to add all these effects to the operation of a stream. The categorical concept of monad is a way to represent them in a functional programming setting. A "monadic stream" is an infinite sequence of events that can trigger any of these effects and more: processes that can interact, duplicate, run in parallel, make random jumps, even enter quantum superpositions.
The theory of monadic streams is in its infancy. We are embarking on a program of study with both theoretical and applicative goals. On the theoretical side, we want a full understanding of the categorical properties of monadic streams. We investigate extension of the notions of productivity, liveness, safety (traditionally formulated for pure streams) in the presence of monadic effects. On the application side, we aim to develop extensive libraries in functional programming (primarily in Haskell) that will give the programmer the power and flexibility to manipulate streams directly in an expressive and sound way. Finally, the convergence of theory and practice will allow us to create formal tools to develop and certify trusted software.