Beweren en bewijzen/de zuilen/Formalisering/7. Vereenvoudigingen

Uit Werkplaats
< Beweren en bewijzen‎ | de zuilen‎ | Formalisering
Versie door Hanno Wupper (overleg | bijdragen) op 21 jan 2011 om 15:09 (Tekst vervangen - '{{BenB/Inhoud' door '<noinclude>{{BenB/Inhoud')
(wijz) ← Oudere versie | Huidige versie (wijz) | Nieuwere versie → (wijz)
Ga naar: navigatie, zoeken
de opzet 2017-18    KalenderIcon.gif multimedia kwaliteit commentaren
site map


Beweren en bewijzen
Wijsheid omgaan met onzekerheid: met open blik op wankele ondergrond levenspad bewandelen
Vernuft aanpak van glibberige problemen precies redeneren op het hoogste niveau
vier zuilen → Artefacten Formalisering Taal Zekerheid
1. Rationaliteit Rationaliteitsvierkant 4 werelden Beweren is moeilijk Overtuigen
2. Modellen Focus Precisie Logica Stelling en bewijs
3. Model en realiteit Specificaties Domeinmodel Syntax en semantiek Waarheid
4. Correctheid Structuur Correctheidsstelling Typering Nagaan
5. Methoden Decompositie Systemat. vertalen Definities Natuurl. deductie
6. Theorie Domeintheorie Tijd Tijdslogica Wiskunde
7. Complexiteit Hiërarch. decompositie Vereenvoudigingen Modules Bewijsassistenten
8. Generalisering Standaardisatie Parametrisatie Talen Hulpstellingen
Beweren en bewijzen/de zuilen/Formalisering/7. Vereenvoudigingen

Aan deze pagina wordt nog gewerkt. Bedankt voor uw begrip.

literatuur

Taxonomy/1. Quality/02. Models

We hebben eerder geleerd dat men beweringen, met name specificaties en blauwdrukken, beter kernachtig en goed opgemaakt kan opschrijven en dat men definities kan gebruiken om alles op precies één plek te schrijven.

Ook hebben we geleerd dat men een probleem vanuit verschillende gezichtspunten kan behandelen en onder elk gezichtspunt van veel dingen abstraheren.

Maar dan nog kunnen formules erg complex en onoverzichtelijk worden en hun controle en verwerking te moeilijk - zelfs voor computers.

Manieren om een specificatie overzichtelijk te houden
kernachtig en leesbaar
niet meer schrijven dan nodig is, en dit gesructureerd opmaken
definities
dingen maar op één plek zeggen
abstractie 
niet over (voor het gekozen gezichtspunt) irrelevante dingen praten
idealisatie 
verwaarloosbare hoeveelheden als 0 behandelen

Bij de besturing van de wissels en seinen van een spoorweg moet alles op het juiste moment gebeuren. Van de tijd kunnen we onmogelijk abstraheren. Bij het redeneren erover of alles correct gebeurt, moeten we voortdurend over momenten en duraties praten. Alles kost tijd: het rijden van de treinen, het bewegen van slagbomen, wissels, seinen, de berekeningen in het besturingskastje en de geleiding van stroom in de kabels. Moeten we al deze duraties ook in de formule meenemen?

Gelukkig niet. Hier kunnen we leren van de natuurkunde.

Terug naar de correctheidsstelling van onze deurbel. Streng genomen kan zo 'n deurbel als gespecificeerd niet bestaan, want de snelheid van de stroom in kabels is beperkt. Het rinkelt altijd ietsjes later dan de knop ingedrukt was. Een eerlijke specificatie zou die vertraging noemen, al dan niet gecontroleerd vaag. Natuurkundigen weten heel goed wanneer ze oneerlijk mogen doen alsof iets geen tijd kost, geen ruimte inneemt of geen wrijving heeft. Ze →verwaarlozen bepaalde kleine hoeveelheden. In deze traditie mogen we bij een huis- tuin- en keukendeurbel doen alsof de snelheid van stroom oneindig is. Maar we moeten wel goed weten wanneer zoiets mag, zie Beweren en bewijzen/de zuilen/Artefacten/6. Domeintheorie.

Zo ook bij de spoorwegovergang: de tijden die de computer nodig heeft voor zijn berekeningen (enkele microseconden) en de tijden die nodig zijn om seinen om te schakelen (minder dan één seconde) vallen in het niets t.o.v. de tijden die bij de verkeersleiding en beveiliging een rol spelen (tientallen seconden, soms vele minuten). Hier is verwaarlozing van de reken- en schakeltijden verantwoord. Zo hoeven in de formules niet voor te komen omdat we net doen alsof ze nul zijn.

Wisseltijden daarentegen worden niet verwaarloosd. Dat zijn relevante momenten omdat voor het vrijgeven en omschakelen de vorige trein de hele wissel verlaten moet hebben en hij pas weer gereserveerd kan worden voor een opvolgende trein als de wissel correct is vergrendeld. Het duurt ca. (n + 1) ∙ 6 sec om n wissels om te zetten. Men zet wissels niet precies tegelijk om om te vermijden dat er een grote piek in de stroombelasting komt. Deze tijden zijn relevant omdat die orde-grootte al relatief dicht bij die van de afstand tussen treinen ligt (typisch 2–3 minuten). Dan is 12 sec al 7–10%, en het omschakelen van wissels verkleint de capaciteit behoorlijk.

Ook niet verwaarloosd wordt de zichttijd, de tijd die een machinist nodig heeft om een sein te zien. Het sein moet dus al enkele seconden voordat de trein in de buurt komt op de juiste stand gezet worden.

Overlijdensakten en soortgelijke documenten verwaarlozen soms het precieze moment van het overlijden en noemen alleen de datum [1]. Dat is voldoende informatief voor een (weduwen- of wezen)pensioenfonds, maar bij bepaalde erfkwesties kan dat te weinig exact zijn.