NEAL-TYPE · Non-extensional and linear models for Dependent Type Theory
6РП — Действия „Мария Кюри“
- Период
- 2006-10-18 → 2008-10-17
- Финансиране от ЕС
- 159 684 €
- Участници
- 1
- Схема
- EIF
Линиите свързват координатора с партньорите.
Накратко на български
Връзката между теорията на зависимите типове и многомерната теория на категориите се изследва чрез превръщане на математическите доказателства в компютърни програми. Това помага да се разбере доколко компютърът може да изпълнява сложни математически доказателства.
Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.
Резултати накратко
Final Activity Report Summary - NEAL-TYPE (Non-extensional and linear models for Dependent Type Theory)
This project has established, for the first time, a link between two previously unconnected areas of mathematics: dependent type theory and higher-dimensional category theory. Dependent type theory is a branch of mathematics which deals with the following question: to what extent can the proofs that mathematicians work with be carried out by a computer? It does so by considering a mathematical statement as a specification for computer programs, and a proof of that statement as an implementation of the corresponding specification. For example, here is a typical mathematical statement: 'There exist infinitely many primes.' Through the lens of dependent type theory, this is translated into the following specification: 'A program which, when you give it a number, computes another number which is larger than the input and is prime.' From this perspective, a proof that there are infinitely many primes is just a program implementing this specification. On the other hand, higher-dimensional category theory is a kind of meta-mathematics. Let us first note that the objects which are studied in pure mathematics generally represent real-world phenomena. For example, the collection of ways in which you can rotate a Rubik's cube is represented by the mathematical notion of a 'group', which is defined to be any collection of operations which can be composed together and also undone; whilst the everyday notion of a shape is captured by the mathematical notion of 'topological space'. Category theory is a little different, because the notion of 'category' does not represent real-world phenomena, but instead mathematical ones. Informally, a category is a kind of mathematical universe. Higher-dimensional categories are a special kind of mathematical universe particularly suitable for representing mathematical objects which 'look like topological spaces'. Intuitively, it is clear that there is a mathematical universe which is 'the universe of dependent type theory', or 'the universe of mathematics as done by a computer', and so we should expect to be able to build a category which represents this universe. This is indeed the case; but the novelty of this project has been to show that what we obtain is not only a category but also a higher-dimensional category. On the one hand, this tells us something about dependent type theory: that its objects of study in some sense 'look like topological spaces'. On the other, it tells us something about higher-dimensional category theory, by allowing us to talk about it using the language of intensional type theory.
Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз
Цел на проекта
The proposed programme of research will develop a comprehensive theory of models for two extensions of classical dependent type theory: dependent type theory with non-extensional equality, and linear dependent type theory.It will do this by altering the existing theory of models for dependent types in two fundamental ways: firstly, by shifting from one-dimensional to higher-dimensional categories, and secondly, by shifting from cartesian structures to monoidal strucures.It will then look for applications for this generalised theory in, amongst other areas, categorical logic, homotopy theory and quantum computing This programme will be implemented by the Fellow working in close collaboration with members of the host organisation; the Fellow will bring skill s and experience in the area of higher-dimensional category theory, enriched category theory, and linear logic; the host organisation, skills and experience in dependent type theory.This project fits tightly with the objectives of the Specific Programme o f the EIF and the broader Human Resources and Mobility Work Programme, by providing the Fellow with an opportunity to undergo training through research, thereby diversifying his technical expertise from higher-dimensional category theory to the complementary area of dependent type theory and its applications in theoretical computer science.By providing him with the opportunity to relocate from the UK to Uppsala, Sweden, it will allow this training to take place in the location most suitable for his needs, namely at an internationally recognised centre of excellence in dependent type theory.Moreover, by promoting a cross-fertilisation of the still distinct disciplines of categorical logic and dependent type theory, it will lead to the development of a new area of research and the creation of European centres of excellence in this new area, thereby increasing Europe and competitiveness and attractiveness to researchers in the field.
Оригинален текст от CORDIS (на английски).
Участници
- UPPSALA UNIVERSITET · UPPSALAКоординаторШвеция
Връзки
Данни: CORDIS, © Европейски съюз