The geometry of implementation

Abstract

This thesis aims to develop efficient implementation techniques for functional programming languages using novel technology arising from recent work on Linear Logic, the Geometry of Interaction, and Optimal Reductions. The philosophy behind the implementations that we consider is that they should arise naturally from some underlying semantics of the language. We are then in a setting where correctness becomes a triviality, and semantic tools are at hand to assist directly with any optimisations, transformations, etc. that we may apply. In other words our interests are to implement the theory directly, rather than to find a theory that fits the practice; putting an engineering perspective on the theory. We begin in Chapter 1 with general motivations for the use of the semantic tools that we will utilise, in particular the Geometry of Interaction. We go on in Chapter 2 to give basic definitions and background for the ideas used in this thesis. In Chapter 3 we will look at translating the A-calculus in to Linear Logic proof structures which will be the starting point of all our implementations. We then go onto extracting the result from these proof structures. Chapter 4 takes a detailed look at the notions related to the Geometry of Interaction, namely Paths, Labels and Types. Lafont's Interaction nets provide the first implementation of Linear Logic that we shall consider in Chapter 5. We give one very simple implementation of the A-calculus as an interaction net, and work through the proofs of correctness using ideas from Girard's Geometry of Interaction. We address the problem of Levy's theory of optimality too; however, we stress that this is not one of our goals. We are interested in efficient implementations of functional languages from a very practical point of view. An alternative implementation is given in Chapter 6 which is based on data-flow. We show that we can set up a computational interpretation of the Geometry of Interaction that mimics cut-elimination in the A-calculus. This chapter concludes by giving several very simple concrete implementations of this data flow on a standard von-Neumann architecture. More specifically, we give a coding of the Geometry of Interaction in assembly language. We conclude our ideas in Chapter 7 and suggest some further extensions to this work. In particular, we look at Hybrid systems, derived from combinations of the ideas presented in the two previous chapters.