Overlapping and order-independent patterns in type theory

Nooit meer fouten maken

Computerproblemen heeft iedereen wel eens. Voor de meeste mensen is dit enkel een frustrerende vorm van tijdverlies, maar wat moeten we met computers in medische apparatuur, auto's of ruimtevaartuigen? Hier kan zelfs een klein computerfoutje mensenlevens kosten. Om dit te vermijden, moeten we computers zo ontwerpen dat ze weigeren om een programma met fouten erin uit te voeren.

Computers spelen steeds meer een centrale rol in onze samenleving. We vinden ze terug in onze gsm, in onze tv en in onze auto; maar ook in telefooncentrales, medische apparatuur, ruimtevaartuigen en militaire apparatuur. We vertrouwen er dus ook steeds meer op dat deze computers foutloos werken. Om fouten in de software (zogenaamde bugs) te vermijden, wordt deze op voorhand grondig getest. En toch leert de praktijk ons keer op keer dat er altijd fouten in software blijven staan. Twee spectaculaire voorbeelden zijn de explosie van het ruimteschip Ariane 5 in 1996 en de overbestraling door de Cobalt-60 medische bestralingsmachine die in 2001 aan minstens 8 mensen het leven kostte.

Door steeds meer te testen kunnen we dus wel steeds meer fouten vinden, maar helemaal zeker dat er geen fouten meer overblijven, zijn we nooit. Is het dan onmogelijk om software te maken zonder fouten? De enige manier om honderd procent zeker te zijn, is door wiskundig te bewijzen dat het programma correct werkt. Maar wiskundige bewijzen geven is ingewikkeld, en daardoor alleen weggelegd voor specialisten. Bovendien bevatten zelfs de bewijzen van specialisten soms nog fouten, waardoor het hele bewijs waardeloos kan worden. Toch is dit al een stap in de goeie richting.

Om het gemakkelijker te maken om wiskundige bewijzen over programma's te geven, zijn er nieuwe programmeertalen ontworpen. In deze programmeertalen kunnen we niet alleen programma's schrijven, maar ook wiskundige bewijzen over onze programma's. De computer kijkt deze bewijzen dan automatisch na. Als er fouten in staan, weigert de computer om het programma uit te voeren. Door deze strenge controle kunnen we eindelijk zeker zijn dat het programma correct werkt.

De wiskundige theorie waarop deze programmeertalen zijn gebaseerd heet typetheorie en is bedacht in 1971 door de Zweedse wiskundige Per Martin-Löf. In typetheorie worden de types uit klassieke programmeertalen uitgebreid met logische symbolen zoals ∀ (voor alle) en ∃ (er bestaat) om zo eigenschappen van programma's te kunnen formuleren en bewijzen. Jammer genoeg zijn deze programmeertalen momenteel nog niet bruikbaar zonder een grondige kennis van de onderliggende wiskundige theorie. Het is niet realistisch om deze kennis te verwachten van iemand die `gewoon' een correct programma wil schrijven. Dus een belangrijk doel in het huidige onderzoek is om deze talen zo te ontwerpen dat de benodigde kennis tot een minimum wordt beperkt.

Een voorbeeld van een veelgebruikte techniek om programma's te schrijven is gevalsonderscheid. Dit is een manier om aan de computer te zeggen: in dit geval moet je zus doen, in dat geval zo, enzovoort. De technische naam voor gevalsonderscheid is `pattern matching'. Als we iets willen bewijzen over een programma dat pattern matching gebruikt, moeten we dit voor elk geval afzonderlijk bewijzen. Een bewijs over een programma met gevalsonderscheid maakt dus gebruik van hetzelfde gevalsonderscheid!

In huidige programmeertalen gebaseerd op typetheorie ontstaat er een probleem wanneer er meerdere gevallen tegelijkertijd van toepassing zijn. In deze situatie wordt er namelijk gekozen voor het eerste geval dat van toepassing is. De volgorde waarin de gevallen staan beïnvloedt dus de werking van het programma. Dit maakt het moeilijker om het bewijs te geven voor de andere gevallen die ook van toepassing waren.

Stel bijvoorbeeld dat je het controlesysteem voor een raketlancering bent aan het programmeren. Sterk vereenvoudigd zou dit er zo uit kunnen zien:

• Als de ontsnappingssnelheid is bereikt, schakel de motoren uit.
• Als de brandstof van de boosters op is, koppel deze los.
• In alle andere gevallen, ga verder met lancering.

Het is mogelijk dat zowel de ontsnappingssnelheid bereikt is en de brandstof van de boosters op is. In de bestaande programmeertalen worden dan enkel de motoren uitgeschakeld, maar worden de boosters niet losgekoppeld. We kunnen dus niet bewijzen dat de boosters altijd worden losgekoppeld wanneer hun brandstof op is.

Het doel van mijn thesis is om gevalsonderscheid met overlappende gevallen beter te laten werken. Dit doe ik door niet te kiezen voor het eerste geval dat van toepassing is, maar voor alle toepasbare gevallen tegelijk. Het is echter niet realistisch of wenselijk om ook echt alle gevallen tegelijk uit te voeren. In plaats daarvan controleert de computer of het programma samenvloeiend is. Dit wil zeggen dat alle gevallen die van toepassing zijn hetzelfde resultaat geven. Tijdens de uitvoering wordt dus toch het eerste geval gekozen, maar het is nu wel gegarandeerd dat een andere volgorde toch hetzelfde resultaat zou geven.

Programmeertalen waarin we ook bewijzen kunnen geven staan nog ver van het punt waarop ze door iedereen bruikbaar zijn. Hopelijk brengt deze thesis dat punt weer een klein beetje dichterbij. En misschien komt er ooit een dag waarop het even gemakkelijk is om een programma te schrijven, als om te bewijzen dat het correct is.