Beweren en bewijzen/de zuilen/Artefacten/6. Domeintheorie
literatuur
|
Een voorbeeld
Terug naar onze deurbel uit Beweren en bewijzen/de zuilen/Artefacten/4. Structuur. Daar was de kabel als volgt gespecificeerd:
Kabel: Dan en slechts dan als er een spanning op contact B staat, staat er een spanning op contact C.
In de tijd van de Koude Oorlog was het een belangrijke vooruitgang dat de Amerikaanse president een deurbel naar het kremlin had om daar te signaleren dat de atoomraketten die op weg naar Moskou zijn, per ongeluk en zonder kwade bijbedoelingen gelanceerd werden. We zullen het nu niet hebben over het nut van zo'n transcontinentale deurbel in een groter geheel. De focus blijft de bel zelf.
De specificatie van de kabel en daarmee de hele correctheidsstelling uit Beweren en bewijzen/de zuilen/Artefacten/4. Structuur voldoet hier niet, omdat ze iets vereenvoudigt dat op zo'n grote afstand niet meer vereenvoudigd mag worden: de snelheid van de stroom in de kabel en de elektrische weerstand. Het duurt even, voordat een signaal uit Washington Moskou bereikt. Als het überhaupt nog waarneembaar aankomt, want het wordt met oplopende afstand steeds zwakker.
Hier is aanvullende theorie en domeinkennis nodig: de dikte van kabels, de specifieke weerstand van koper, de specifieke capaciteit van zo'n kabel, de snelheid van licht in koper, en in het verlengde daarvan misschien ook wat extra wiskunde. (In dit geval valt de wiskunde overigens mee omdat de belangrijkste effecten lineair zijn.)
|
voorbeelden voor specificaties van algemene kabels |
Modelleerkeuzes
Welke domeinkennis en -theorie voor een correctheidsvraagstuk nodig is hangt van de focus af. In de praktijk zal je vaak een beroep moeten doen op een domeinexpert. Alleen al bij iets zo elementair als de tijd zijn er verschillende keuzemogelijkheden:
- Soms kunnen we van de tijd abstraheren, omdat we alleen over één moment praten: Alles gebeurt "op het moment waarop"; het is niet nodig om verschillende momenten en duraties aan elkaar te praten.
- Soms kunnen we vereenvoudigen en gerust doen alsof bepaalde handelingen geen tijd kosten.
- Soms kunnen we de tijd modelleren m.b.v. natuurlijke getallen (de tikken van een klok), waarbij we niet meer nodig hebben dan de wiskundige operaties +, - en *. We moeten er dan wel op letten dat men twee duraties bij elkaar mag optellen, dat men een duratie bij een moment mag optellen, maar dat men nooit twee momenten bij elkaar mag optellen.
- Soms modelleren we de tijd beter met reële getallen zo als de natuurkundigen het doen. Voor duraties en momenten geldt hetzelfde als bij natuurlijke getallen.
- Soms, bij hoge snelheden, mag men tijden niet eens zo maar optellen maar heeft een flink stuk natuurkunde nodig.
Domeintheorie in talen
|
|
|
