Homotopy Type Theory

点击翻译按钮获取中文摘要

Type theory was originally developed by Russell as a foundation of mathematics which avoids paradoxes such as Russell's paradox. It was further developed by Church and Martin-Löf, amongst others. Unlike Set Theory, which must be used inside a logical framework such as Higher Order Logic, Martin-Löf's type theory (MLTT, or dependent type theory) internalises the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic, which corresponds to the computational model of Church's lambda calculus. One notable advantage of this intuitionistic interpretation is that every term in intensional MLTT can be reduced to a canonical form, and every function is computable, whereas in Set Theory it is possible to define incomputable functions. This makes it possible to develop theorem-proving systems where type checking is decidable.Quotient sets occur widely in mathematics. The current generation of dependently-typed theorem-proving systems do not make it very easy to produceproofs involving quotients. In informal mathematical practice one often describes constructions on quotient sets by saying what to do on a representative of an equality class, leaving the reader to check that it is well defined, that is, respects the equivalence relation. One aim of this research is to find easier ways to produce formal machine-checked proofs involving Quotient Inductive Types (QITs), ideally in a way that fits better with existing informal mathematical practice. It will build on the techniques researched in Steenkamp's Master's project on QITs. More generally it plans to investigate the use of Higher Inductive Types (HITs) in both theorem proving and functional programming. Two open problems in this field are finding a general schema for HITs, and giving a computational interpretation.Many researchers have identified the importance of this field, and the implications for mathematics and formal verification techniques should not beunderstated. One of the goals of the late Voevodsky and others is: "[T]hat, in a not too distant future, mathematicians will be able to verify the correctness of their own papers [...] in a proof assistant and that doing so will become natural even for pure mathematicians (in the same way that most mathematicians now typeset their own papers in TeX)." - Awodey, Pelayo, Warren (2013). The advantages are clear: Big or complex proofs can be tackled with much higher assurance, and anyone with a computer would have the capability of verifying a proof. This would allow fair assessment of research, not biased by name or status, perhaps leading to faster progress and a greater variety of ideas in mathematical research.Another major application of type theory research is in the development of type systems for programming languages, which guarantee certain kinds of error cannot occur. Experience has taught us that weakly typed languages result in bug-ridden, unmaintainable code. This is evidenced by the trend in industry away from weakly-typed languages and the recent development of languages with stronger type systems, such as Swift, Go, TypeScript, and C#. One notable example is Rust, in which the type system guarantees memory safety and thread safety. As the scale and complexity of computer programs continues to increase it is vital that research is carried out in type theory to ensure that future programs are robust, particularly in aerospace, medicine, security, and other high-assurance domains.Existing techniques such as unit tests cannot check for bugs such as "Will this program ever get stuck in an infinite loop?". Formal verification techniques can be used to prove that a program always terminates. Most formal verification techniques require translating the program into a model. This integration of program and proof will increase the adoption of verification tools, and the productivity of software developers using them.