Free Extensions of 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.