School of Computer Science
University of Nottingham
Thursday, 27 October 2016, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: Streams are infinite sequences of values. They inhabit a frontier region of constructive mathematics and computer science: they cannot be represented fully inside human minds and computer memories, but they are omnipresent as input, output and interactive behaviour.
Brouwer formulated the notion of "choice sequence", a progression of values that is not generated by an effective rule, but rather by a creative subject. Alternatively, they may model repeated measurement of physical phenomena or interactive input from a non-predictable user.
If the streams themselves are not computable, functions on them, realized as programs, must be effective. From this requirement, Brouwer concluded that a Continuity Principle must hold: all functions on streams of natural numbers are continuous. This means that the value of a function on a specific stream only depends on a finite initial segment.
The principle seems to be justifiable in a computational view and is certainly true from the meta-theoretical standpoint. We may be tempted to add it in a formulation of the foundations of constructive mathematics. However, recently Martín Escardó discovered that if we add the Continuity Principle to Constructive Type Theory, we obtain a contradiction. I will discuss the paradox and the possible avenues of repair. One way is to weaken the principle, using an existential quantifier that does not provide a witness.
I suggest a different solution. In the original formulation, we consider functions on the internal type of streams, encoded as functions from natural numbers to natural numbers. But this type does not capture the idea of an unpredictable sequence not subject to rule and possibly coming from an outside source.
I propose that "monadic streams" are a better model: these are sequences in which a monadic action must be executed to obtain the next element and the continuation. A monadic action is any of a wide class of enriched structures and modes of value presentation. Monadic programming has been very successful in modelling interaction and side effects in functional programming.
I propose a version of the Continuity Principle for monadic streams. This has great potential not only as a foundational theory but in practical applications. Monadic streams have already been successfully used in functional reactive programming and game implementation. The principle applies to functions on monadic streams that are polymorphic in the monad and natural on it. They are a reasonable description of mappings on sequences that do not depend on how the sequence is generated. I will prove that these functions are always continuous.
A different representation of continuous functions consists in their tabulation as well-founded trees. A function is a tree, branching on the type of stream elements, with leaves labelled by result type elements: the input stream is used as a path that we follow to reach a leaf that contains the output result. This perfectly captures the notion of continuity. However, it is not in general provable that every continuous function can be tabulated in this way. In a recent paper with Tarmo Uustalu, we proved that this follows from Bar Recursion, a computational version of another of Brouwer's non-standard constructive principles, Bar Induction.
Using monadic streams we can actually construct a tabulating tree by a specific monadic instantiation. Under what condition this leads to a one-to-one correspondence is an interesting open problem.