Programming and Reasoning on Infinite Data Structures

该项目研究形式逻辑和计算理论中的无限对象。虽然计算机（像人类一样）的内存有限，只能处理有限的数据结构，但数学已经发展出了描述和推理无限抽象对象的理论。近年来，通过新的模型和技术研究了无穷大的计算和构造方面。在函数式编程语言中，可以通过有限的循环定义来表示潜在的非良基数据，这些定义可以根据需要展开：这些被称为“惰性”数据类型。程序设计和推理技术使用户和科学家能够像处理无穷大一样处理这些对象，而坚实的理论基础为它们的具体实现提供了基础。类型论是一个形式系统的集合，包含了形式逻辑、构造性数学和编程语言。类型论同时也是一个逻辑系统，一个函数式编程语言，以及一个形式化数学发展的环境。类型用于表示数据结构和逻辑公式，元素表示程序和证明：这被称为Curry-Howard同构。基于类型论的现代工具使用"共归纳"类型、族和谓词来表示潜在无限的数据结构和证明。它们的语义证明来自于最终共代数的范畴理论。对这些结构的可接受性的正式要求正逐渐变得更加技术化和精细化。这个项目（FRIS，从这里开始）将探索清晰的语义原则，这些原则将简化实现并扩展其适用性。两条研究路线将被追求：研究最终余代数概念的推广，例如在余递归代数或纤维化范畴的背景下，以给出对无限结构的良好数学理解;将反射的方法应用于共感对象，即，在系统内部编码一种被解释为潜在无限对象的语法表达式，然后利用FRIS的最终产品将是一个基于新的数学原理的编程/推理计算机系统。反射是形式逻辑中的一种编程和推理技术：它包括在形式逻辑系统中定义系统本身及其规则的语法模型。这允许在基本语义级别不可能的术语和公式的语法操作。虽然基系统和内部表示之间的完美对应不能被形式化地证明（这一事实是哥德尔不完全性定理的核心），我们仍然可以通过它们的语义意义来证明许多有用的句法操作。在共归纳类型的具体情况下，我们提出了以下策略：在基础层次上，我们希望在语义上将它们刻画为实际上的无限结构;在不同的层次上，我们将构造一个语法模型，描述这些对象如何被呈现和存储。

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.