Theory And Applications of Induction Recursion

计算机擅长在微秒内进行数十亿次数字的加法运算。另一方面，人类擅长抽象思维。哲学、文学、科学和数学的发展就是例证。这些观察结果对编程和编程语言的设计产生了深远的影响。计算机科学中许多研究的主要关注点是最小化人类如何概念化程序和如何在编程语言中实现这些程序之间的差异。为了实现这一点，我们做着人类5000年来一直在做的事情，因为我们试图了解我们周围的世界。也就是说，我们构建数学模型-在这种情况下，是计算的数学模型--然后在编程语言的设计中反映对计算的理解。因此，数学、编程和编程语言的设计之间存在一种共生关系，任何试图切断这种联系的尝试都会削弱每一个组成部分。递归是计算中最基本的数学概念之一。它的重要性在于它给了我们定义计算代理的能力--这些代理可以是递归程序、递归数据类型、递归算法或无数其他结构中的任何一种。递归的最初处理可以追溯到20世纪30年代，当时可计算性的概念是通过一般递归函数理论形式化的。实际上，递归对我们的计算能力和对计算过程的理解的贡献怎么估计都不为过。有没有可能关于递归还有什么基本的东西要说？我们相信是有的。我们的核心观点是：当以递归方式定义函数时，函数的输入通常是预先固定的。但如果他们不是呢？如果当我们递归地构建函数时，我们也归纳地构建其输入，会发生什么呢？以这种方式定义的函数的研究称为归纳递归，该提议旨在发展归纳递归的理论和应用。我们的中心目标是将归纳递归从目前仅为类型理论中相对少数的研究人员所知，转变为编程语言社区中的一种主流技术。这既需要归纳递归的理论发展，让我们有更多的方式去理解它，也需要案例研究和实例来使它更容易为程序员所理解。幸运的是，现在是做这项研究的绝佳时机！数据类型的范畴研究已经发展到了这样一个阶段，即理论工具现在已经到位，可以处理归纳递归。也许更根本的是，Eigram和AGDA形式的依赖类型编程语言已经发展到可以用代码实现我们的想法的阶段，因此归纳递归的好处可以直接提供给程序员，以他们理解的形式。我们可以为他们提供代码以供他们使用！事实上，我们希望更进一步地探索归纳递归可以在多大程度上形成编程语言的基础。总而言之，这项建议采用了理论计算机科学中的最先进的想法，并将致力于将它们直接转化为编程语言中的最先进的技术。这种理论和应用的结合，携手并进，往往是优秀科学的标志！

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!