Classical Dependent Type Theories

经典依赖类型理论

• 批准号: EP/J009113/1
• 负责人: Robin Adams
• 金额: $ 12.56万
• 依托单位: Royal Holloway University of London
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2012
• 资助国家: 英国
• 起止时间: 2012 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FJ009113%2F1
• 关键词: Classical; Dependent; Type; Theories

The job of a mathematician is to prove theorems - that is, to provide a rigorous, logical argument that establishes that a mathematical statement is true. If the proof is correct, then we can be certain that the theorem is true. But how can we be certain that a proof is correct?Proof assistants are computer programs that help the user to formalise a mathematical proof, and check that the proof is correct.They are slowly becoming important for research mathematicians. They have also become very important in the computing industries, for software verification and hardware verification: a formal proof that a product has the properties it is supposed to have, checked by a proof assistant, allows a high degree of confidence in the product.When designing a proof assistant, one must first choose a system of logic. A system of logic consists of a symbolic language in which theorems and proofs may be written, together with a set of rules for deciding which proofs are correct. The systems of logic known as type theories have proven very successful for use in proof assistants.Given a system of logic, we may ask: which proofs can be formalised in this system? Proofs are divided into "constructive proofs" and "classical proofs". Most computer scientists, and the vast majority of mathematicians, accept classical proofs. But proof assistants based on type theory have, so far, only been able to formalise constructive proofs; and this is quite a large constraint on their usefulness.Certain objects, called control operators, may be added to a type theory. When these are added to some simple type theories, the theories now accept classical proofs; this is a very surprising fact, and still not well understood. However, when control operators are added in the same way to more complex type theories (dependent type theories), the theories become inconsistent; that is, it is now possible to "prove" statements that are false.The problem is that there are several different ways in which control operators may be added to a complex type theory; we have several choices as to where we allow a control operator to appear, and how control operators interact with the other features of a type theory. The naive choice - allow them everywhere, and allow all possible forms of interaction - leads to inconsistency. Of the many other possibilities, it is not at all obvious which will be most likely to be fruitful; and investigating their properties one by one would be very time consuming.Systems of logic known as logic-enriched type theories, or LTTs, have also been developed. These are closely related to type theories. They differ in being divided rigidly into two parts: one part - the type-theoretic component - for defining mathematical objects and programs, and one part - the logical component - for stating and proving theorems about the object. We can change the logical part to make it accept classical proofs, without changing the type-theoretic part.However, LTTs are still quite new, and their theoretical properties and suitability for use in a proof assistant is not yet well understood.I believe that work on control operators and work on LTTs can help each other. If we investigate the properties of type theories and classical LTTs, and translations between the two, then we should be able to reuse results and use the insights from one to shed light on the other. In particular, we should find the best way to add control operators to a complex type theory, by choosing the way that makes translation to and from LTTs easiest.I therefore propose to construct several type theories with control operators and several classical LTTs, investigate their theoretical properties and translations between them, and experiment with their use in practice. My aim is to produce one or more systems of logic that keeps all the advantages of type theories; accepts classical proofs; and is practicable for use in a proof assistan

数学家的工作是证明定理 - 也就是说，提供了一个严格的逻辑论点，以确定数学陈述是正确的。如果证明是正确的，那么我们可以确定定理是正确的。但是，我们怎么能确定证明是正确的？证明助手是计算机程序，可以帮助用户形式化数学证明，并检查证明是否正确。他们对研究数学家的逐渐变得重要。它们在计算行业，用于软件验证和硬件验证方面也变得非常重要：正式证明产品具有由证明助手检查的属性，可以对产品具有高度的信心。当设计证明助手时，必须首先选择逻辑系统。逻辑系统由一种符号语言组成，可以写出定理和证据，以及一组确定哪些证据正确的规则。事实证明，被称为类型理论的逻辑系统在证明助理中非常成功。启动了逻辑系统，我们可能会问：在该系统中可以正式化哪些证明？证明被分为“建设性证明”和“古典证明”。大多数计算机科学家和绝大多数数学家都接受古典证据。但是，到目前为止，基于类型理论的证明助手只能正式化建设性的证据。这是对其有用性的很大限制。确定对象（称为控制算子）可能会添加到类型的理论中。当将它们添加到一些简单类型的理论中时，这些理论现在接受经典的证据。这是一个非常令人惊讶的事实，但仍然不太了解。但是，当以更复杂的类型理论（相关类型理论）相同的方式添加控制运算符时，这些理论就变得不一致。也就是说，现在可以“证明”错误的陈述。问题在于，可以将控制操作员添加到复杂的类型理论中有几种不同的方式。对于允许控制操作员出现的位置以及控制操作员如何与类型理论的其他特征互动，我们有几种选择。幼稚的选择 - 允许它们到任何地方，并允许所有可能的互动形式 - 导致不一致。在许多其他可能性中，一点也不明显，最有可能是富有成果的。并且还开发了一个称为逻辑富含逻辑的型理论或LTTS的逻辑系统。这些与类型理论密切相关。它们在严格分为两个部分方面有所不同：一个部分 - 类型理论组件 - 用于定义数学对象和程序，以及一个部分 - 逻辑组件 - 用于说明和证明有关对象的定理。我们可以更改逻辑部分以使其接受经典的证据，而不会更改类型的理论部分。但是，LTTS仍然很新，他们的理论属性和用于证明助手的理论属性和适用性尚不很好地理解。我相信控制操作员的工作和在LTT上的工作可以互相帮助。如果我们研究类型理论和经典LTT的属性，以及两者之间的翻译，那么我们应该能够重复使用结果并使用一个从一个洞察到另一个洞察力。特别是，我们应该通过选择使LTTS翻译和从LTTS进行翻译的方式来找到将控制运算符添加到复杂类型理论的最佳方法。我的目的是生产一种或多种逻辑系统，以保持类型理论的所有优势；接受古典证据；并且在证明辅助方面是可行的