Computation in Refinement Logics for Type Theory

计算机科学关注的是在“信息空间”中构建抽象结构。在其他领域有如此多的应用，是因为这些结构是如此通用，因为计算机硬件可以实现它们。计算机科学家研究控制信息处理的规律，他们创造工具来帮助建立结构、测试和理解它们。到目前为止，提供的最强大的工具包括编程语言和环境。但现在，这一领域正在研究如何将这些环境扩展到更强大、更通用的工具，即问题解决环境。这项建议是关于一类这样的系统的数学基础。这里研究的这类系统的特点是它与逻辑的关系。人们已经发现，某种形式逻辑为函数式编程语言和问题求解环境提供了基础。这个想法是，构造性的数学证明可以解释为函数式程序。这一概念现在已经研究了十多年，并在实践中得到了检验。结果鼓励了更深入的研究，因为这些系统建议的编程方法似乎比普通编程更可靠，也更强大。它能够利用定理证明、逻辑编程和严格的编程方法的结果。这项工作涉及如何将这些要素结合在一起的细节。这一领域的发现可能会极大地改变人们编程和解决某些精确问题的方式。这一领域目前是英国、法国、瑞典、德国和美国共同努力的焦点。研究人员认为，正在测试的这类系统很快就会在计算机科学实验室之外得到广泛应用。这项研究解决了在实现这一目标之前必须解决的一些核心理论问题。特别是，它涉及到这些系统可以由它们的用户(反思)扩充的某些方式，以及在系统的目标导向的问题解决(或等价的程序开发)的过程中关于解决问题的决定可以被推迟的方式。延期的想法集中在使用一种特殊的变量，称为逻辑变量。这项调查的结果将加深对计算机科学和逻辑的其他部分中逻辑变量的各种使用和反映之间的关系的理解，并将在下一代问题解决环境的设计中使用。

Computer science is concerned with building abstract structure in "information space". There are so many applications in other fields because these structures are so general and because computer hardware can realize them. Computer Scientist study the laws that govern the processing of information, and they create tools to assist in the task of building structures, testing and understanding them. Among the most powerful tools provided so far are programming languages and environments. But the field is now converging on ways to extend these environments to more powerful and general tools, called problem solving environments. This proposal is about the mathematical basis for one class of such system. The class of systems studied here is characterized by its relationship to logic. It has been discovered that a certain kind of formal logic provides a basis for both functional programming languages and problem solving environments. The idea is that constructive mathematical proofs can be interpreted as functional programs. This notion has now been studied for over a decade and tested in practice. Results have encouraged a much deeper study because the programming method suggested by these systems seems to be more reliable than ordinary programming and much more powerful. It is able to draw on results from theorem proving, logic programming and rigorous programming methodology. This work is concerned with details of how to bring these elements together. It is possible that the discoveries made in this area will significantly change the way people program and the way they solve certain kinds of precise problems. The area is currently the focus of a concerted effort in Britain, France, Sweden, Germany, and the U.S. Researchers feel that soon systems of the kind being tested will be widely used beyond the computer science laboratory. This research addresses some of the central theoretical problems that must be solved before that can happen. In particular it is concerned with certain ways that these systems can be augmented by their users (reflection) and with ways that decisions about solving a problem can be postponed in the process of systematic goal-directed problem-solving (or equivalently program development). The idea for postponement centers on the use of a special kind of variable called a logic variable. Results from this investigation will deepen understanding of the relationship between various uses of logic variables and reflection in other parts of computer science and logic and find use in the design of the next generation of problem solving environments.