Overlapping and order-independent patterns in type theory

Jesper Cockx
Persbericht

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.

Bibliografie

A. Abel, and T. Altenkirch: A predicative analysis of structural recursion. Journal of Functional Programming 12.1, 2002. 1-41. L. Bachmair, and D. A. Plaisted, Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation 1.4, 1985. 329-349. T. Coquand, Pattern matching with dependent types. Proceedings of the 1992 workshop on types for proofs and programs, Bastad, Sweden, ed. B. Nordstrom et al., 1992. 66-79. Available at www.cse.chalmers.se/research/group/logic/Types/proc92.ps (accessed 3 June, 2013). P. Dybjer, Inductive families. Formal Aspects of Computing 6.4, 1994. 440-465. H. Goguen, A typed operational semantics for type theory. PhD thesis, University of Edinburgh, 1994. G. Gonthier, Engineering mathematics: the odd order theorem proof. Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Rome, Italy. New York: ACM, 2013. 1-2. H. Goguen, C. McBride, and J. McKinna, Eliminating dependent pattern matching. Algebra, Meaning, and Computation, ed. K. Futatsugi et al. (Lecture Notes in Computer Science, 4060). Berlin/Heidelberg: Springer, 2006. 521-540. A. Graf, Left-to-right tree pattern matching. Proceedings of the 4th international conference on rewriting techniques and applications, Como, Italy, ed. R.V. Book (Lecture Notes in Computer Science, 488). Berlin/Heidelberg: Springer, 1991. 323-334. C. S. Lee, N. D. Jones, and A. M. Ben-Amram, The size-change principle for program termination. ACM SIGPLAN Notices 36.3, 2001. 81-92. Z. Luo, Computation and reasoning: a type theory for computer science (International Series of Monographs on Computer Science, 11). New York/Oxford: Oxford University Press, Inc., 1994. C. McBride, Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh, 2000. C. McBride, H. Goguen, and J. McKinna, A few constructions on constructors. Types for Proofs and Programs, ed. J.-C. Filliatre et al. (Lecture Notes in Computer Science, 3839). Berlin/Heidelberg: Springer, 2006. 186-200. C. McBride, and J. McKinna, The view from the left. Journal of Functional Programming 14.1, 2004. 69-111. B. Nordstrom, K. Petersson, and J. M. Smith, Programming in Martin-Lof 's type theory (International Series of Monographs on Computer Science, 7). New York/Oxford: Oxford University Press, Inc., 1990. U. Norell, Towards a practical programming language based on dependent type theory. PhD Thesis, Chalmers University of Technology, 2007. E. Rijke, Homotopy type theory. Master Thesis, Utrecht University, 2012. M. Sozeau, Equations: A dependent pattern-matching compiler. Proceedings of the first international conference on interactive theorem proving, Edinburgh, UK, ed. M. Kaufmann et al. (Lecture Notes in Computer Science, 6172). Berlin/Heidelberg: Springer, 2010. 419-434. S. Thompson, Type theory and functional programming. Computing Laboratory, University of Kent, 1999. Available at http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ (accessed 3 June, 2013). D. Vytiniotis, T. Coquand, and D. Wahlstedt, Stop when you are Almost-Full. Proceedings of the third international conference on interactive theorem proving, Princeton, NJ, USA, ed. L. Beringer and A. Felty (Lecture Notes in Computer Science, 7406). Berlin/Heidelberg: Springer, 2012. 250-265. H. Xi, Dependently typed pattern matching. Journal of Universal Computer Science 9.8, 2003. 851-872.

Universiteit of Hogeschool
Wiskunde
Publicatiejaar
2013
Share this on: