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

SHF:Small:RUI：高级数据类型的深度归纳规则

• 批准号: 2203217
• 负责人: Patricia Johann
• 金额: $ 61.31万
• 依托单位: Appalachian State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2203217&HistoricalAwards=false
• 关键词: SHF; Small; RUI; Deep; Induction

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.

一种特别成功的软件验证方法是演绎验证。演绎验证根据软件规范生成数学证明义务，并且当满足这些证明义务时，保证软件实现符合生成它们的规范。生成的义务可以通过手写的数学证明来履行，但现代软件非常复杂，这通常是乏味且容易出错的，甚至是完全不可行的。因此，越来越多的证明是在 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 的新颖“最大函数解释”基于与标准初始代数语义相同的既定原则，并且实际上专门针对标准初始代数语义。对于 ADT 和嵌套类型。因此，它为 ADT、（真正的）嵌套类型、GADT 和 IF 提供了统一的语义，以及用于导出其深层归纳规则的统一方法。实际上，这使得通过保守地扩展目前用于 ADT 的标准归纳技术，而不是开发全新的方法，将 GADT 和 IF 的深度归纳纳入现代证明助手中成为可能。即使将仅针对 ADT 的深度归纳纳入现有的证明助手中，也将显着扩展和改进它们。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。