Programming and Reasoning on Infinite Data Structures

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

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.