Free Extensions of Second-Order Algebras

二阶代数的自由扩展

• 批准号: 2741288
• 金额: --
• 依托单位: University of Edinburgh
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2022
• 资助国家: 英国
• 起止时间: 2022 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2741288
• 关键词: Free; Extensions; Second; Order; Algebras

Knowing when two programs are behaviourally equivalent is useful in code generation and optimising compilers. It is unfortunately impossible to determine behavioural equivalence for an arbitrary pair of programs in general purpose programming languages. Compilers reduce programs into an intermediate representation (IR), where they can apply local equivalences to optimise expressions. The Frex project has produced a framework for unifying the treatment of IRs for some data types, like integers and lists. I will extend this work by developing Frex^2, which will allow for a unified treatment for the IRs of more complex algebraic expressions.* Background** Frex^1The Frex project has produced a result I will call Frex^1: free extensions of first-order algebra. These are data structures and algorithms that take a limited set of program terms and produce a normalised result. A new expression can then be produced that is both behaviourally equivalent and more efficient.A Frex^1 consists of a data structure and a normalisation algorithm. This algorithm can take program terms consisting of first-order algebraic operations, variables, and static values, and produce a value of the data structure. First-order algebras can express expression languages such as arithmetic on integers, operations on lists, and matrix multiplications.** Second-Order AlgebraModern programming languages feature functions, I/O, pattern matching and global state. All of these constitute second-order algebras, where operations can bind variables in their arguments. For instance, the lambda calculus is a second-order algebra with two operations: abstraction which binds a variable in its sole argument to create an anonymous function; and application which does not bind variables in either of two arguments, applying a value to a function.Frex^2 will generalise the structures from Frex^1 over first-order algebras into structures over second-order algebras.* Work PlanI will perform work in three main phases:- Development of the mathematical theory of Frex^2- Design and implementation of Frex^2 for some algebras- Applying Frex^2 to compiler infrastructure** TheoryIt is well understood that second-order algebras subsume first-order algebras. I will investigate whether Frex^2 subsume Frex^1 in the same way. I will also look at combining Frex^2 for a calculus with Frex^1 for base types to form a new Frex^2.Another recent development in the area is Frex^Gen. These are multi-sorted Frex^1, with variables whose sorts depend on other variables. For example, functions whose domain or codomain depend on variables. Frex^Gen likely subsumes Frex^2, but features a large technical overhead unnecessary for Frex^2. I will explore both the relationship between and the potential efficiencies of using Frex^2 over Frex^Gen.** AlgorithmsI will investigate how normalisation by evaluation algorithms used in compilers are the implementation of a Frex^2 for their underlying calculi. This will require implementing data structures and algorithms for the standard-form of the Frex^2. I can then produce mechanised proofs that the structures are equivalent.I will also provide a proof synthesis framework that given a suitable Frex^2 can construct equality proofs for program fragments. Such a framework is useful in dependently-typed programming languages, where types in the language can depend on the equality of two embedded program fragments.** ApplicationModern optimising compilers produce IRs in different forms for applying different optimisations. I will investigate the extent to which IRs are implementations of a Frex^2, and attempt to produce a framework for creating a Frex^2 for different optimisations.I will demonstrate how using Frex^2 instead of explicit IRs can leads to more succinct code. I will also run a suite of benchmarks to evaluate the performance difference of using Frex^2 over equivalent IRs.

知道两个程序在行为上是否等价，对于代码生成和优化编译器是很有用的。不幸的是，在通用编程语言中，不可能确定任意一对程序的行为等价性。编译器将程序简化为中间表示（IR），在那里他们可以应用局部等价来优化表达式。Frex项目已经产生了一个框架，用于统一某些数据类型（如整数和列表）的IR处理。我将通过开发Frex ^2来扩展这项工作，它将允许对更复杂的代数表达式的IR进行统一处理。Frex项目产生了一个我称之为Frex的结果：一阶代数的自由扩张。这些是数据结构和算法，它们采用有限的程序术语集并产生规范化的结果。这样就可以产生一个新的表达式，它在行为上是等价的，而且效率更高。该算法可以采用由一阶代数运算、变量和静态值组成的程序项，并产生数据结构的值。一阶代数可以表达表达式语言，如整数运算、列表运算和矩阵乘法。二阶代数现代编程语言具有函数，I/O，模式匹配和全局状态。所有这些都构成了二阶代数，其中运算可以在其参数中绑定变量。例如，lambda演算是一个具有两个操作的二阶代数：抽象操作，将一个变量绑定在其唯一的参数中以创建一个匿名函数;应用操作，不将变量绑定在两个参数中的任何一个中，将一个值应用于函数。工作计划我将在三个主要阶段进行工作：-开发Frex^2的数学理论-为一些代数设计和实现Frex^2-将Frex^2应用于编译器基础设施 ** 理论众所周知，二阶代数从属于一阶代数。我将研究Frex^2是否以同样的方式从属于Frex^1。我还将研究如何将微积分中的Frex^2与基本类型中的Frex^1结合起来，形成一种新的Frex^2。该领域的另一个最新发展是Frex^Gen。这是一种多排序的Frex^1，其变量的排序依赖于其他变量。例如，定义域或上定义域依赖于变量的函数。Frex^Gen很可能包含了Frex ^2，但它的特点是大量的技术开销，这对Frex ^2来说是不必要的。我将探讨使用Frex ^2和Frex^Gen之间的关系以及使用Frex ^2和Frex^Gen的潜在效率。我将研究编译器中使用的求值算法的规范化是如何实现其底层演算的Frex^2的。这就需要实现Frex^2标准格式的数据结构和算法。然后我就可以给出结构等价的机械化证明，我还将提供一个证明合成框架，在给定一个合适的Frex ^2的情况下，该框架可以为程序片段构造等式证明。这样的框架在依赖类型编程语言中很有用，其中语言中的类型可以依赖于两个嵌入程序片段的相等性。应用现代优化编译器以不同的形式产生IR，用于应用不同的优化。我将研究IR在多大程度上是Frex^2的实现，并试图为不同的优化创建一个Frex^2的框架，我将演示如何使用Frex^2而不是显式IR来产生更简洁的代码。我还将运行一套基准测试，以评估使用Frex^2与使用等效IR相比的性能差异。