SHF:Small:RUI: Deep Induction Rules for Advanced Data Types

一个特别成功的软件验证方法是演绎验证。演绎验证从软件规范中生成数学证明义务，并且当这些证明义务得到满足时，保证软件实现符合生成它们的规范。生成的义务可以通过手写的数学证明来解除，但现代软件足够复杂，这通常是乏味和容易出错的，如果不是完全不可行的话。因此，越来越多的证明是在像Agda、Coq、Idris和Lean这样的证明助手中开发的。归纳法是此类证明辅助工具中最重要的证明技术之一。事实上，几乎所有涉及数据类型的非平凡证明都是直接通过归纳证明的，或者依赖于这样的引理。因此，每当一个新的数据类型在Coq中被声明时，一个归纳规则就会自动生成，但是因为它们只遍历数据结构的顶层，而不是所有的层，所以数据类型的一些属性应该服从归纳，但是Coq生成的结构归纳规则无法证明。深度归纳是最近发展起来的结构归纳的一种概括，它确实可以归纳数据结构中存在的所有数据。这个项目的新奇在于，它将深度归纳从Coq通常处理的代数数据类型（ADT）和（真正）嵌套类型扩展到更有表现力的泛化，称为广义ADT（GADT）和归纳族（IF）。因此，该项目的影响是使检测错误和验证程序属性成为可能，这些属性不能仅使用ADT和嵌套类型表示，但可以使用GADT和IF表示。该项目涉及为GADT和IF的深度归纳开发一个原则性的、概念简单的、统一的和全面的框架，包括：i）一个生成一个非常一般的GADT类的文法，包括所有来自文献的文法; ii）一个新的GADT类的内函子初始代数语义，证明了它们的深归纳规则; iii）GADT和IF之间的翻译，其产生类似的语义，从而产生IF的深度归纳规则;以及iv）实现的工具，其直接从GADT和IF的语法生成用于GADT和IF的深度归纳规则，以及证明它们正确的证据。总的来说，该项目应用最先进的理论来改进最先进的验证实践。从理论上讲，内函子初始代数语义是数据类型理论的基石之一，也是导出它们的结构归纳规则的关键。该项目的深度归纳框架的一个特别引人注目的特征是，作为其基础的GADT和IF的新颖的“最大函子解释”基于与ADT和嵌套类型的标准初始代数语义相同的成熟原则，并且专门针对这些原则。因此，它为ADT、（真正的）嵌套类型、GADT和IF提供了统一的语义，以及用于导出其深度归纳规则的统一方法。实际上，这使得有可能通过保守地扩展目前用于ADT的标准归纳技术，而不是通过开发全新的方法，将GADT和IF的深度归纳纳入现代证明助手。即使将ADT的深度归纳纳入现有的证明助手中，也将大大扩展和改进它们。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

A particularly successful approach to software verification is deductive verification. Deductive verification generates mathematical proof obligations from software specifications, and, when these proof obligations are met, software implementations are guaranteed to conform to the specifications from which they were generated. Generated obligations can be discharged by means of hand-written mathematical proofs, but modern software is sufficiently complex that this is often tedious and error-prone, if not outright infeasible. Increasingly, therefore, proofs are developed in proof assistants like Agda, Coq, Idris, and Lean. Induction is one of the most important proof techniques available in such proof assistants. Indeed, almost all non-trivial proofs involving data types are either proved by induction outright or rely on lemmas that are. For this reason, every time a new data type is declared in, say, Coq, an induction rule is automatically generated for it. But because they traverse only the top layer, rather than all of the layers of a data structure, there are some properties of data types that should be amenable to induction but that the structural induction rules generated by Coq cannot prove. Deep induction is a recently developed generalization of structural induction that does indeed induct over all of the data present in data structures. This project's novelty is that it extends deep induction from the algebraic data types (ADTs) and (truly) nested types typically handled by Coq to their more expressive generalizations known as generalized ADTs (GADTs) and inductive families (IFs). The project's impact is thus to make it possible to detect errors and verify program properties that cannot be expressed just using ADTs and nested types, but that can be expressed using GADTs and IFs.The project involves developing a principled, conceptually simple, uniform, and comprehensive framework for deep induction for GADTs and IFs, including: i) a grammar that generates a very general class of GADTs, including all those from the literature; ii) a novel endofunctor initial-algebra-like semantics for GADTs that justifies their deep induction rules; iii) translations between GADTs and IFs that yield similar semantics, and thus deep induction rules, for IFs; and iv) implemented tools that generate deep induction rules for GADTs and IFs, together with witnesses that prove them correct, directly from their syntax. Overall, the project applies state-of-the-art theory to improve state-of-the-art verification practice. Theoretically, endofunctor initial algebra semantics is one of the cornerstones of the theory of data types, and is key to deriving even structural induction rules for them. A particularly compelling feature of the project's framework for deep induction is that the novel "maximally functorial interpretations" of GADTs and IFs that serve as its foundation are based on the same well-established principles as, and indeed specialize to, the standard initial algebra semantics for ADTs and nested types. It thus delivers a uniform semantics for ADTs, (truly) nested types, GADTs, and IFs, as well as a uniform methodology for deriving their deep induction rules. Practically speaking, this makes it possible to incorporate deep induction for GADTs and IFs into modern proof assistants by conservatively extending the standard induction techniques currently in use for ADTs, rather than by developing fundamentally new approaches. Even incorporating deep induction just for ADTs into existing proof assistants will significantly extend and improve them.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.