Information Technology (Council of Physical Sciences)
100 %
Ortelius classification: Informatics
Panel
European Reserach Council (ERC)
Department or equivalent
Department of Programming Languages Compilers (Eötvös Loránd University)
Starting date
2018-04-01
Closing date
2018-07-31
Funding (in million HUF)
2.329
FTE (full time equivalent)
0.33
state
closed project
Summary in Hungarian
A kutatás összefoglalója, célkitűzései szakemberek számára Itt írja le a kutatás fő célkitűzéseit a témában jártas szakember számára. A függő típuselmélet egy olyan programozási nyelv, melyben egy program típusa matematikai állításnak, az adott típusú program pedig az állítás bizonyításának tekinthető. A Martin-Löf típuselmélet egyenlőség típusával lehet kifejezni két program egyenlőségét. Az egyenlőség egy induktívan megadott típus, melynek hiányossága, hogy az ugyanahhoz a bemenethez ugyanazt a kimenetet rendelő programok illetve a logikailag ekvivalens állítások nem egyenlőek. Ezeket a tulajdonságokat axiómaként hozzávehetjük a típuselmélethez, de akkor az ezeket az axiómákat tartalmazó programok végrehajtása elakad. Kutatásunk célja a Martin-Löf típuselmélet kiegészítése a fenti tulajdonságokkal úgy, hogy a programok végrehajthatók maradjanak. Ehhez a típuselmélet setoid modellje adja az inspirációt, melyben egy típust egy halmazzal és egy azon értelmezett ekvivalencia-relációval értelmezünk. Az így kapott setoid típuselmélet a homotópia-típuselmélet alsó szintjének egy implementációja.
Mi a kutatás alapkérdése? Ebben a részben írja le röviden, hogy mi a kutatás segítségével megválaszolni kívánt probléma, mi a kutatás kiinduló hipotézise, milyen kérdéseket válaszolnak meg a kísérletek. A setoid modell megmutatja, hogy a típuselmélet konzisztensen kiegészíthető a pontonként egyenlő függvények egyenlőségével és a logikailag ekvivalens állítások egyenlőségével. A kutatás alapkérdése, hogy ez a modell hogyan alakítható kényelmesen használható szintaxissá. A setoid típuselméletben az egyenlőséget nem induktív típusként, hanem a típus szerkezete szerinti rekurzióval adjuk meg. Például párok egyenlősége egyenlőségek párja lesz, függvények egyenlősége pontonkénti egyenlőség lesz, induktív típusok elemeinek egyenlősége egy újabb induktív típus. A szintaxis megadásán túl a setoid típuselmélet konzisztenciáját és esetleg a programok végrehajthatóságát is szeretnénk bizonyítani. A fentieket az Agda vagy Coq tételbizonyító rendszerben tervezzük formalizálni.
Mi a kutatás jelentősége? Röviden írja le, milyen új perspektívát nyitnak az alapkutatásban az elért eredmények, milyen társadalmi hasznosíthatóságnak teremtik meg a tudományos alapját. Mutassa be, hogy a megpályázott kutatási területen lévő hazai és a nemzetközi versenytársaihoz képest melyek az egyediségei és erősségei a pályázatának! Becslések szerint a szoftverekben található hibák évente ezermilliárd dollárban mérhető kárt okoznak a világgazdaságnak. A hibák egyik leghatékonyabb megelőzése a programok futás előtti típusellenőrzése. Az olyan fejlett típusrendszerű programozási nyelvekkel, mint amilyen a típuselmélet, tetszőlegesen precíz módon specifikálható egy program, így ezzel a futás idejű hibák (szoftver oldalról) teljesen kiszűrhetővé válnak. Egyik feltétele annak, hogy a típuselméletből a gyakorlatban használható programozási nyelv legyen, az egyenlőség kényelmes használata. A setoid típuselmélet ezt oldaná meg azokra a típusokra, melyek halmazok (melyek egyenlőségeinek egyenlőségei triviálisak). Általánosabb, de bonyolultabb megoldás a kubikális típuselmélet, mely magasabb egyenlőségeket is kezel. A setoid típuselmélet előnye ehhez képest, hogy nem szükséges a szintaxist geometriai objektumokkal kiegészíteni. A jövő függő típusokkal rendelkező progamozási nyelveinek alapja lehet a setoid típuselmélet.
A kutatás összefoglalója, célkitűzései laikusok számára Ebben a fejezetben írja le a kutatás fő célkitűzéseit alapműveltséggel rendelkező laikusok számára. Ez az összefoglaló a döntéshozók, a média, illetve az érdeklődők tájékoztatása szempontjából különösen fontos az NKFI Hivatal számára. Napjainkban számítógépes programok irányítanak erőműveket, repülőket, vasúti vágányrendszereket, orvosi készükékeket. Fontos, hogy ezek a programok helyesen legyenek megírva: ne fordulhasson például elő, hogy két vonat ugyanazon a vágányon halad egymással szemben. A hibák egy része megtalálható úgy, hogy a programot egymás után sokszor futtatjuk nem éles üzemben, és vizsgáljuk, hogy megfelelően működik -e. Ezzel még nem kapunk kapunk garanciát a helyes működésre, hiszen lehet, hogy egy programhiba csak bizonyos körülmények között jön elő. Biztosan csak a program helyességének matematikai bizonyításával tudjuk kizárni a hibákat. A típuselmélet egy olyan számítógépes nyelv, melyben programokat és a programokról bizonyításokat egyszerre lehet írni. Kutatásunk célja, hogy kényelmesebbé tegyük a típuselméletben való programozást azáltal, hogy az ugyanazt a kimenetet adó programokat a bizonyításokban egyenlőnek tekinthessük.
Summary
Summary of the research and its aims for experts Describe the major aims of the research for experts. Dependent type theory is a programming language in which the type of a program can be seen as a mathematical proposition and a program can be seen as the proof of the corresponding type. Martin-Löf type theory is equipped with an equality type which expresses equality of two programs. This type is inductively defined and has the deficiency that programs which provide the same output for the same input cannot be proven equal. Also, logically equivalent propositions are not equal. If we add these properties as axioms to type theory, we lose the ability of running all programs. The goal of our project is to extend type theory with rules which add these properties while retaining computation. Our inspiration is the setoid model of type theory in which a type is interpreted by a set and an equivalence relation representing its equality. Setoid type theory would be an implementation of the lowest (set-level) of homotopy type theory.
What is the major research question? Describe here briefly the problem to be solved by the research, the starting hypothesis, and the questions addressed by the experiments. The setoid model proves that type theory can be consistently extended with equality of pointwise equal functions and equality of logically equivalent propositions. The main question of our research is whether this model can be translated into an easy to use syntax. In setoid type theory, equality is not an inductive type, but it is defined by structural recursion on types. For example, equality of pairs is a pair of equalities, equality of functions is pointwise equality, equality of elements of inductive types is another inductive type. Equality would be defined as a logical relation extended by coercion and coherence components. In addition to defining a syntax, we are planning to prove consistency of setoid type theory and maybe normalisation. We would formalise the above constructions in the proof assistant Agda or Coq.
What is the significance of the research? Describe the new perspectives opened by the results achieved, including the scientific basics of potential societal applications. Please describe the unique strengths of your proposal in comparison to your domestic and international competitors in the given field. It is estimated that software bugs cost more than one thousand billion US dollars a year for the world economy. One of the most effective way of preventing bugs is type checking before running the program. Programming languages with more advanced type systems can catch more bugs. Type theory is a programming language with a type system capable of specifying program behaviour with arbitrary precision. This allows very strong guarantees for the absence of runtime errors. One problem which prevents type theory of becoming a practically usable language is the treatment of equality. Setoid type theory would make the usage of equality more convenient for types which are sets (where equalities of equalities are trivial). A more general solution to the same problem is given by cubical type theory which however has a complex syntax. The advantage of setoid type theory is that it is not necessary to extend the syntax with geometric objects as done in cubical type theory.
Summary and aims of the research for the public Describe here the major aims of the research for an audience with average background information. This summary is especially important for NRDI Office in order to inform decision-makers, media, and others. In today's industry, computer programs control power plants, airplanes, railway track systems and medical devices. It is important that these programs are correct: for example, it should be guaranteed that two trains can never go in each others direction on the same track. It is possible to discover some of the program errors by repeatedly running the program in a testing environment and checking if it is behaving correctly. This however does not give a guarantee for the absence of errors as some errors only come out in certain special circumstances. It is only possible to make sure that there are no errors by mathematically proving the correctness of the program. Type theory is a computer language in which one can write programs and mathematical proofs about programs and the same time. The goal of our research is to make type theory more convenient to use: to add the possibility to treat programs which have the same output as equal.
Final report
Results in Hungarian
A kutatás során azt vizsgáltuk, hogy a típuselmélet setoid modellje megadható-e szintaktikus átírásként (a programfordítás egy lépéseként). Agdában formalizáltuk a setoid modellt, és a modellbe való kiértékelést alakítottuk át szintaktikus átírássá. Hogy az átírás környezetből környezetet hozzon létre, az indexelt családok és projekciók közötti ekvivalenciát használtuk fel. A szintaktikus átírás szintaxissá alakításából megkaptunk egy setoid típuselméletet. Ahhoz, hogy az identitás típus ugyanabban a környezetben legyen, mint az eredeti típus, a függvény típust kiegészítettük egy új eliminátorral, a kongruenciával. A nyitott állítás-univerzum modellezéséhez nem elég a setoid modell, úgy tűnik, hogy egy globuláris modellre van szükség. Agdában formalizáltuk a globuláris modell fő komponenseit. Munkánk eredményeképpen jobban értjük a modellek és szintaktikus átírások kapcsolatát, és egy általános módszert kapunk modellek átírássá alakításává.
Results in English
We investigated whether the setoid model of type theory can be turned into a syntactic translation (a step of the program compilation process). We fully formalised the setoid model in Agda and turned the interpretation into this model into a syntactic translation. To achieve that a context is mapped to a context by the translation we used the indexed family -- display map equivalence. Furthermore, we defined a setoid type theory by turning the recursive definition of the syntactic translation into equalities in the syntax. We added a new congruence eliminator to the function space in setoid type theory. This was needed to achieve that the identity type is in the same context as the original type. To model an open universe of propositions, it seems that we need a globular variant of the setoid model. We formalised the main components of the globular type model of type theory in Agda. As a result of our work, we understand the relationship between syntactic translations and models better and we developed a general method to obtain syntactic translations from models.
