Wij knutselen een wiskundig kladblok

Situering

• Formele logica:
  • formaliseer een stukje wiskunde, bv. een module die formele bewijzen van stellingen over grafen, ... formeel kan controleren. (Voor dit onderwerp is het nog een beetje vroeg; de rest van het systeem moet eerst wat stabieler worden.)
  • ontwikkel een automatische bewijs-generator. Kijk bijvoorbeeld eens goed naar de source van gandalf (down op 26-jul-2000) en port naar Java ...
  • Implementeer een aantal algoritmen uit de cursus (normaalvormen, ...) (Voor dit onderwerp is het nog een beetje vroeg; de rest van het systeem moet eerst wat stabieler worden.)
• Formele talen:
  • Welke talen kan je parsen met een real-time parser zoals die uit het programma? Wat zijn de beperkingen, hoe zijn ze te omzeilen? Kunnen we een tool bouwen à la yacc of lex om automatisch nieuwe talen te kunnen parsen gegeven een formele grammatica ervan? (Zie ook http://coleweb.dc.fi.udc.es/cole/publications.html i.v.m. incremental parsers)
  • Onderzoek reguliere expressies voor syntaxbomen. Klassieke reguliere expressies beschrijven strings; aangezien SICECAS alles voorstelt als een syntaxboom zouden we zoekopdrachten als ``geef alle bewijsregels waar onder het integraalteken de sinus van de integratievariabele in het kwadraat'' willen kunnen gebruiken. Het liefst willen we zulke zoekopdrachten op een min of meer gebruikersvriendelijke manier kunnen opstellen. Maak (of zoek of er al bestaan) een reguliere-expressie-achtige taal die zulke query's over bomen kan beschrijven; bestudeer eventueel de werking van bestaande reguliere expressie-talen (zie Apocalypse 5 voor een uitvoerige uitleg over reguliere expressies in Perl 6) om de abstracte eigenschappen ervan te vinden en over te zetten naar bomen. Naast zoeken van patronen is ook vervangen ervan nuttig (denk bijvoorbeeld aan herschrijfregels van tableaus).
• Parallelle algoritmen: Java is de ideale taal om over verschillende soorten computers via netwerk het rekenwerk te verdelen. Onderzoek welke van de gebruikte algoritmen geparallelliseerd kunnen worden en steek een systeem in elkaar om het werk te distribueren.
  Een extra probleem dat je kan bestuderen is: hoe kan je er zeker van zijn dat een client niet liegt? Zie hiervoor opcode authentication van distributed.net (lokale kopie)); anti-cheat client algoritme in sommige Quake clients(???), processtree, Internet Cheating, Project JXTA, The Search for E.T. Yields Earthly Cheats, Incentives for Sharing in Peer-to-Peer Networks, Uncheatable Distributed Computations, Distributed Computing with Payout. (Zie ook Mosix in verband met adaptive load balancing algoritmes) Een computeralgebrasysteem dat iets soortgelijks doet is ParGAP.
• Applicatie-ontwerp: Om te vermijden dat bij het aanpassen van het programma oude bugs weer `boven water' komen, heb ik een testprogrammaatje gemaakt dat alle oude bugs automatisch controleert (regressie-test met een mooi woord). Het zou interessant zijn om programma's (of eventueel de virtuele machine) automatisch zo te instrumenteren dat we kunnen controleren of alle mogelijke paden in de code wel degelijk bereikt worden, en zo nee, welke niet bereikt worden.
  Op kortere termijn zou eens uitgezocht moeten worden hoe je GUI's het best test (en dan vooral in combinatie met JUnit). Nadeel van JUnit is dat het (mijn versie toch) vanuit de AWT thread zijn tests lanceert, wat een en ander schijnt te bemoeilijken.
• Computeralgebra: implementeer je favoriete stuk wiskunde, bijvoorbeeld
  • Groebnerbasissen
  • Galois-theorie
  • Infinitesimale analyse
  • Feynmann-diagrammen (er is blijkbaar ook vraag naar ergens op de S9) (Zie ook xloops)
  • Constructiemeetkunde: een module in de stijl van het interactief met grafen werken die toelaat meetkundige passer-en-liniaal-constructies te maken
  (Voor dit onderwerp is het nog een beetje vroeg; de rest van het systeem moet eerst wat stabieler worden.)

Doelpubliek

Benodigde voorkennis

Caveat Emptor

Referenties

Laatst aangepast op 27 mei 2002