Generalised higher-order free extensions

这项研究的目的是利用抽象代数的当代技术来转换和验证计算机程序和数据库查询。这个项目不是从一开始就研究特定的编程/查询语言并开发其直接转换，而是考虑抽象地根据代数的自由扩展来转换通用程序的问题。自由扩展用于描述语言的术语/表达式，当通过自由变量或未知的集合扩展时，自由扩展用于描述语言的术语/表达式。因此，通过了解自由扩展的结构，我们可以深入了解如何通过重新排列或计算它们的子表达式来操作表达式，目的是获得等价的、但简化/优化的表达式。这最终提高了程序/查询执行的性能。此外，通过仔细记录在操作表达式时所采取的步骤，我们可以自动地获得已经发生的转换的正确性的证明--即，程序/查询的含义被保留。虽然对于那些由标准通用代数描述的语言已经被很好地理解，但是这个项目的目标是通过扩展可以使用自由扩展来建模的语言构造族来推动我们理解的边界。我们对依赖类型、绑定运算符和微分运算符特别感兴趣。这种抽象方法很有价值，因为它得到了它所解决问题的强抽象特征的支持。因此，作为该项目的一部分开发的工具和技术具有高度的可重用性。尽管如此，该项目旨在开发的方法在编译器构建、增量计算和形式验证方面有许多直接应用。该项目由GitHub通过iCASE学生资助部分资金，因为它在通用静态分析系统CodeQL中具有潜在应用，该系统负责静态检查大量源代码的安全属性。特别是，CodeQL项目对推导和核实关系查询语言的符号区分程序感兴趣，以便支持对其分析进行有效的增量评估。关系表达式的高效求值是CodeQL求值器的核心，对于及时提供关键分析结果至关重要。该系统的增量有可能带来显著的性能改进，使开发人员能够在逐个提交的基础上获得即时反馈。该项目属于EPSRC编程语言和编译器研究领域。

The objective of this research is to leverage contemporary techniques from abstract algebra for the transformation and verification of computer programs and database queries. Rather than investigating specific programming / query languages from the outset and developing direct transformations thereof, this project considers the problem of transforming general programs abstractly in terms of free extensions of algebras.Free extensions are used to characterise the terms / expressions of a language when extended by a collection of free variables or 'unknowns'. Therefore, by understanding the structure of free extensions, we gain insight into how we may manipulate expressions by rearranging or evaluating their sub-expressions, with the aim of obtaining equivalent, yet simplified / optimised, expressions. This ultimately improves the performance of program / query execution. Moreover, by carefully recording the steps taken while manipulating expressions, we can automatically derive proofs of the correctness of the transformations that have taken place - i.e., the meaning of the program / query is preserved.While already well-understood for those languages described by standard universal algebra, this project aims to push the boundaries of our understanding by extending the family of language constructs that can be modelled using free extensions. We are particularly interested in dependent types, binding operators and differential operators.This abstract approach is valuable as it is backed by a strong abstract characterisation of the problem it solves. As such, the tools and techniques developed as part of this project are highly reusable. That said, the methods this project aims to develop have many direct applications in compiler construction, incremental computation and formal verification.This project is partially funded by GitHub through an iCASE studentship due to its potential applications in their general purpose static analysis system 'CodeQL', responsible for statically checking security properties for large volumes of source code. In particular, the CodeQL project is interested in the derivation and verification of procedures for the symbolic differentiation of relational query languages in order to support efficient incremental evaluation of their analyses. Efficient evaluation of relational expressions sits at the heart of the CodeQL evaluator and is essential for providing critical analysis results in a timely fashion. Incrementalising this system has the potential to bring drastic performance improvements, giving developers access to immediate feedback on a commit-by-commit basis.This project falls within the EPSRC programming languages and compilers research area.