Detaljerad information för diarienr 2014-4864  
 
 
Besl. instans: NT
Ämnesområde: Övrigt generellt
Beslutsdat: 2014-10-24
Namn: Abel, Andreas
Titel: Doktor Kön: Man
Univ./Institution: Göteborgs universitet - Dept. of Computer Science and Engineering
Projekttitel: Termineringscertifiering för program och bevis med beroende typer
Project title: Termination Certificates for Dependently-Typed Programs and Proofs via Refinement Types
Värdhögskola: Göteborgs universitet
SCB-klassificering: Datavetenskap (Datalogi), Algebra och logik
Beviljat(SEK): Bidragsform/Finansieringskälla   2015 2016 2017 2018
  Projektbidrag/
Vetenskapsrådet, naturvetenskaplig-teknikvetenskaplig forskning
  900000 900000 900000 900000
Beskrivning: För forskningsfronten framåt inom datorstödd teorembevisning När Fermat 1636 skrev om sin stora sats, ?Jag har ett i sanning underbart bevis för detta påstående, men marginalen är alltför smal för att rymma det? (i sin kopia av boken Arithmetica) så hade han helt klart rätt: marginalen var verkligen för smal för att rymma beviset. Det tog 350 år, och generationer av matematiker, innan beviset blev fullständigt. Vissa bevis är inte bara svåra att hitta men ockå svåra att kontrollera. Ett till synes oskyldigt påstående är Fyrfärgssatsen som säger att det behövs högst fyra färger för att färglägga en karta på ett sådant sätt att inga angränsande regioner har samma färg. Problemet formulerades 1852 men det dröjde till 1976 innan Appel & Haken först lyckades bevisa det. De reducerade problemet till 1936 fall som de sedan använde ett program för att kontrollera. Beviset möttes av skepsis eftersom bevis anses vara en sekvens påståenden direkt sammanlänkade av enkla logisk regler, och inte beroende av datorberäkningar. Det visade sig senare att det finns ett bevis av fyrfärgssatsen som är en ?enkel? påståendekedja, men det beviset är för långt för någon matematiker att kontrollera. År 2005 lyckades Gonthier med hjälp av datorprogrammet Coq konstruera ett sådant bevis. Coq hjälper vid beviskonstruktion och kontrollerar att alla steg är korrekta. Coq följer ?bara? de logiska regler som är inprogrammerade i systemet. Ett matematiskt bevis i Coq ser själv ut som ett datorprogram. Detta är ingen slump; de berömda logikerna Curry & Howard upptäckte att bevis och program har många likheter. I Coq kan man skriva program och bevis i samma språk. Det finns dock en viktig skillnad mellan program och bevis. En oändlig följd av påståenden räknas inte som ett bevis men vissa program kan (och ska) köra i all oändlighet. Bevisassistenter som Coq använder sig av en termineringskontroll som garanterar att varje bevis och program stannar inom ändlig tid. Denna kontroll är en viktig del av Coq: om den är felaktig kan oändliga, ogiltiga bevis accepteras. Förs att vara på den säkra sidan får termineringskontrollen bara acceptera program och bevis vars terminering kan garanteras. En berömd sats inom datavetenskapen, stopproblemet, säger att en perfekt termineringskontroll inte kan implementeras, men vi vill i varje fall komma nära. Vi har som mål att förbättra termineringskontrollen i bevisassistenter. För det första vill vi göra termineringskontrollen intelligentare så att den kan känna igen fler terminerande program. Vi använder oss av en ny teknik som kallas typ-baserad termineringskontroll. Den använder ett programs typ, som är en abstrakt beskrivning av programmets beteende, för att guida termineringskontrollen. Med denna teknik kan man kontrollera program som består av abstrakta byggstenar som kallas högre ordningens funktioner. För det andra kommer den nya termineringskontrollen inte bara att svara ja eller nej, utan kommer att ge en formell motivering till varför programmet verkligen terminerar. Denna motivering är i form av ett termineringsmått och beskriver vilken kvantitet som blir mindre varje gång programmet går igenom en loop. För eller senare blir detta mått noll och då stannar programmet. När termineringsmåttet har hittats är det lätt att verifiera att programmet verkligen terminerar och att svaret var korrekt. Man behöver då inte lita blint på termineringskontrollen (som ofta är ganska komplex). Sammanfattningsvis kommer detta projekt att demonstrera att den nya metoden är korrekt, dvs att om ett giltigt mått hittas så kommer beviset som konstruerats av bevisassistenten att vara korrekt. För att visa detta måste varje bevisregel som används kontrolleras i en så kallad modell av bevisassistenten. Projektet kommer att påverka det dagliga arbetet för datavetare och matematiker som använder bevissassistenter för att kontrollera sina bevis. En bättre termineringskontroll medför att de kommer att kunna skriva sina bevis på ett naturligare sätt. Eftersom även termingsmått produceras kommer de att kunna lita mer på sina bevis och sova bättre om natten. Och eftersom arbetet bygger på en solid modellkonstruktion hoppas vi kunna övertyga fler matematiker att använda bevisassistenter. De kommer inte längre behöva skriva kryptiska anteckningar i marginalen!