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.