Theory And Applications of Induction Recursion

Computers are good at adding billions of numbers in microseconds. Humans, on the other hand, are good at abstract thinking. This is exemplified by the development of philosophy, literature, science and mathematics. These observations have deep consequences for programming and the design of programming languages. The overarching concern of much research in computer science is to minimize the difference between how humans conceptualise programs and how those programs are implemented in a programming language. To achieve this, we do the same thing humans have been doing for 5000 years as we try to understand the world around us. That is, we construct mathematical models --- in this case, mathematical models of computation - and then reflect that understanding of computation within the design of programming languages. Thus, there is a symbiotic relationship between mathematics, programming, and the design of programming languages, and any attempt to sever this connection will diminish each component. Recursion is one of the most fundamental mathematical concepts in computation. Its importance lies in the ability it gives us to define computational agents in terms of themselves - these could be recursive programs, recursive data types, recursive algorithms or any of a myriad of otherstructures. The original treatments of recursion go back to the 1930s where the concept of computability was formalised via the theory ofgeneral recursive functions. It is virtually impossible to overestimate how recursion has contributed to our ability to computeand to understand the process of computation. Is it possible that there is anything fundamental left to say about recursion? We believe there is. Our central insight is this: when defining a function recursively, the inputs of the function are usually fixed in advance. But what if they are not? What if, as we build up the function recursively, we also build up its inputs inductively? The study of functions defined in this way is called induction recursion and this proposal aims to develop the theory and applications of induction recursion.Our central ambition is to turn induction recursion, which is currently known only to a relatively small number of researchers within type theory, into a mainstream technique within the programming language community. This will require both the theoretical development of induction recursion so as to give us more ways to understand it, but also case studies and examples to make it more accessible to programmers. Fortunately this is an excellent time to do this research! The categorical study of data types has advanced to the stage where the theoretical tools are now in place to tackle inductionrecursion. Perhaps even more fundamentally, dependently typed programming languages in the shape of Epigram and Agda have advancedto the stage where our ideas can be implemented in code and hence the benefits of induction recursion can be made directly available toprogrammers in a form they understand. We can supply them with code to play with! Indeed, we hope to go even further an explore the extent to which induction recursion can form the basis of a programming language. In summary, this proposal takes state of the art ideas in theoretical computer science and will aim to turn them directly into state of the art techniques within programming languages. Such combinations of theory and applications going hand in hand together is often the hall mark of good science!