Free Extensions of Second-Order Algebras

知道什么时候两个程序在行为上是等价的，这对于代码生成和优化编译器是很有用的。不幸的是，在通用编程语言中，不可能确定任意一对程序的行为等价。编译器将程序简化为一个中间表示（IR），在那里它们可以应用局部等价来优化表达式。Frex项目已经生成了一个框架，用于统一一些数据类型（如整数和列表）的ir处理。我将通过开发Frex^2来扩展这项工作，它将允许对更复杂的代数表达式的ir进行统一处理。Frex项目产生了一个结果，我称之为Frex^1：一阶代数的自由扩展。这些数据结构和算法采用有限的程序项集并产生规范化的结果。这样就可以产生一个新的表达式，它在行为上是相等的，而且效率更高。Frex^1由数据结构和归一化算法组成。该算法可以接受由一阶代数运算、变量和静态值组成的程序项，并产生数据结构的值。一阶代数可以表达诸如整数运算、列表运算和矩阵乘法等表达式语言。**二阶代数现代编程语言的功能，I/O，模式匹配和全局状态。所有这些都构成二阶代数，其中的操作可以在其参数中绑定变量。例如，lambda演算是一个具有两种操作的二阶代数：抽象，在其唯一参数中绑定变量以创建匿名函数；不绑定两个参数中的任何一个变量的应用程序，将值应用于函数。Frex^2将Frex^1在一阶代数上的结构推广到二阶代数上的结构。*工作计划我将在三个主要阶段进行工作：-发展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的潜在效率。** AlgorithmsI将研究编译器中使用的归一化计算算法是如何为其底层演算实现Frex^2的。这将需要为标准形式的Frex^2实现数据结构和算法。然后我就可以机械地证明这些结构是等价的。我还将提供一个证明合成框架，给定合适的Frex^2可以为程序片段构造相等证明。这种框架在依赖类型的编程语言中非常有用，因为语言中的类型可能取决于两个嵌入式程序片段的相等性。** application现代优化编译器产生不同形式的ir用于应用不同的优化。我将调查ir在多大程度上是Frex^2的实现，并尝试创建一个框架来创建不同优化的Frex^2。我将演示如何使用Frex^2而不是显式ir来生成更简洁的代码。我还将运行一套基准测试来评估使用Frex^2与等效ir的性能差异。

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.