Computation in Refinement Logics for Type Theory

类型论细化逻辑中的计算

• 批准号: 9108062
• 负责人: Robert Constable
• 金额: --
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Continuing grant
• 财政年份: 1991
• 资助国家: 美国
• 起止时间: 1991-10-01 至 1996-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9108062&HistoricalAwards=false
• 关键词: Computation; Refinement; Logics; 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.

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