Programming and Reasoning on Infinite Data Structures

The project investigates infinite objects in formal logic and computation theory.
Although computer (like humans) have a limited memory and can manipulate only finite data structures, mathematics has developed theories to describe and reason about infinite abstract objects. In recent years, the computational and constructive aspects of infinity have been studied by means of new models and techniques. In functional programming languages, it is possible to represent potentially non-well-founded data by finite circular definitions that can be unfolded as needed: these are called "lazy" data types. Programming and reasoning techniques allow users and scientists to manipulate these objects as if they were actually working with infinities, while a solid theoretical basis provides the foundation for their concrete implementation.

The research field is that of type-based proof-assistant technology. Type theory is a collection of formal systems that subsumes formal logic, constructive mathematics, and programming languages. A type theory is at the same time a logical system, a functional programming language, and an environment for the development of formalized mathematics. Types are used to represent both data structures and logical formulas, elements denote both programs and proofs: this is known as the Curry-Howard isomorphism. Modern tools based on type theory use "coinductive" types, families, and predicates to represent potentially infinite data structures and proofs.

Their semantic justification comes from the categorical theory of final coalgebras. The formal requirements for acceptability of these constructions are growing progressively more technical and elaborate. This project (FRIS, from here on) will explore clear semantic principles that will both simplify the implementation and extend its applicability. Two lines of research will be pursued: Study generalizations of the notion of final coalgebra, for example in the line of corecursive algebras or in the context of fibration categories, to give a good mathematical understanding of infinite structures; Apply the method of reflection to coinductive objects, that is, encode inside the system a type of syntactic expressions that are interpreted as potentially infinite objects and then exploit the correspondence between formal manipulation of the codes and mathematical operations on the interpretations.
The final product of FRIS will be a programming/reasoning computer system based on new mathematical principles.

Reflection is a programming and reasoning technique in formal logic: It consists in defining, inside a formal logical system, a model of the syntax of the system itself and of its rules. This allows syntactic manipulations of terms and formulas that were not possible at the base semantic level. Although the perfect correspondence between the base system and the internal representation cannot be proved formally (this fact is the kernel of Gödel's incompleteness theorem), we can still justify many useful syntactic operations by their semantic meaning.
In the specific case of coinductive types, we propose the following strategy: At the foundational level, we want to characterize them semantically as actually infinite structures; at a different level, we will construct a syntactic model that delineates how these objects can be rendered and stored.

Although the investigation of the mathematical properties of infinite computational objects is a rather abstract theoretical subject, there are rich potential applications for it. The impact of the PRIDS project is linked to the improvement of (dependently typed) programming languages. Specifically, we aim to give both more simplicity and power to coinductive types. It will be easier to learn to use them and they will offer more flexibility.

Some specific examples of applications are:

1. I/O: An electronic device is an agent that interacts with its environment. It receives a continuous stream of information from the outside and produces a stream of responses and behaviours. We can usefully see both input and output as never-ending computational objects, that is, elements of coinductive types. The achievemts of PRIDS will have a direct impact on how devices can be programmed and how we can reason about their behaviour.

2. Infinite Games: The formal treatment of game theory is just starting to be developed. Type theory is perfectly suitable for it, since it can easily model games and strategies; it can compute the outcome of a run of the game; and it can support reasoning about the mathematical properties of the game. Games in which termination is not guaranteed from the beginning require potentially infinite notions of run and strategy. These can be provided by coinductive types. Coinductive methods have already proved useful to reason about knowledge states of the players. Reflection can be helpful in this framework: strategies can specify a potentially infinite behavior, but they need to be formulated in a syntactically finite form.

3. General Recursion: Type theory does not directly allow undefined objects and non-terminating computations.
This is necessary to guarantee consistency and decidability of type checking. The drawback is that much of the computational richness of general recursion is lost. General computability needs to be represented indirectly, for example using an inductive termination predicate. It is possible to use coinductive types to model computation traces, thus embedding computability theory in a proof assistant.