Beweren en bewijzen/de zuilen/Formalisering/3. Domeinmodel

literatuur Boek Logica voor alfa's en informatici

Redeneren betekent scheiden, passen en sluiten van gedachtenfragmentjes, en om te beginnen moeten we fragmentjes hebben die zo klein en goed gedefinieerd zijn dat we betrouwbaar na kunnen gaan of ze eigenlijk wel waar zijn t.a.v. de realiteit, of niet. Om zeker te zijn dat onze redenering klopt willen we daartoe een formalisme gebruiken en misschien de redenering ook nog door een computer laten controleren. Daartoe moeten we een formele taal maken.

Omdat dit nogal veel werk is, doen we er goed aan van begin af alles rigoreus weg te laten, wat er niet toe doet. Daarom is het ook belangrijk dat we een focus kiezen en daarmee een gezichtspunt. We hoeven dan niet te praten over fenomenen die onder dat gezichtspunt irrelevant zijn.

Als we bijvoorbeeld na willen gaan of de stroomdraden in een gebouw juist aangesloten zijn, moeten we ook over de kleur van de isolering praten. Er zijn namelijk voorschriften voor het gebruik van zwarte, blauwe, bruine en geel-groene kabels. Als we alleen willen beredeneren dat geen brand of kortsluiting kan ontstaan, doet de kleur van de kabels er niet toe, maar wel hun dikte en daarmee hun weerstand.

Hoe meer je vanaf het begin weloverwogen buiten beschouwing laat hoe makkelijker het later wordt; minder is meer. Maar in welke formele termen praten we het beste over wat we niet buiten beschouwing kunnen laten?

Ons speelveld

Exemplarische onderwerpen

Hoe men door formalisering precisie bereikt en tegen welke prijs leggen we hier exemplarisch uit aan de hand van correctheidsvraagstukken uit de ontwikkeling en verificatie van artefacten. Wat we hier zeggen geldt echter ook voor andere gebieden, al is de koppeling van het formalisme aan de realiteit niet overal zo makkelijk. We zullen namelijk hier alleen redeneren in termen van waarneembare fenomenen.

In Beweren en bewijzen/de zuilen/Artefacten/3. Specificaties gaven we de specificatie van een artefact en haar onderdelen in natuurlijke taal. Formaliseren wil zeggen op een precieze wiskundige manier de specificatie van in dit geval een artefact of onderdeel vastleggen. Door een formele taal te gebruiken wordt een aantal criteria wel gemakkelijker te toetsen. Bijvoorbeeld bij criterium S3: "Een specificatie praat alleen over fenomenen die het te specificeren ding deelt met zijn omgeving". Dit is eenvoudig te toetsen door te kijken of de namen die in de specificatie van een ding voorkomen, overeenkomen met van te voren gedeclareerde namen van fenomenen.

We sluiten dus aan bij de criteria voor specificaties uit Beweren en bewijzen/de zuilen/Artefacten/3. Specificaties en de criteria voor precisie uit Beweren_en_bewijzen/de_zuilen/Formalisering/2._Precisie.

Elke formele specificatie, in welke taal dan ook, praat over wiskundige objecten in de hoop dat deze overeenkomen met de realiteit. Bij ons zijn dat waarneembare fenomenen: verschijnselen waarvan we met een meting kunnen vaststellen of ze in de realiteit waar zijn en in de formele taal namen hebben die met wiskundige objecten corresponderen.

De correspondentie tussen reële fenomenen en namen voor wiskundige objecten geven we hier altijd aan in een tabel: het zogenaamde domeinmodel, ook wel "woordenboek" genoemd.

Gereedschappen zoals Coq kunnen worden gebruikt om een aantal zaken te controleren. Deze controle speelt zich uiteraard alleen af binnen het wiskundige domein.

Exemplarische talen

In deze cursus gebruiken we formele logica zoals uitgelegd in Beweren en bewijzen/de zuilen/Taal/2. Logica. Er zijn talloze andere specificatietalen op de markt, waarvan sommige voor de beroepspraktijk beter geschikt zijn. Maar in geen andere taal dan de logica leer je het beste wat de essentie van formeel specificeren en bewijzen is. Als je deze cursus voltooid hebt kun je andere talen zelf leren en aan elkaar relateren.

In de propositielogica zijn beweringen samengesteld uit eindig veel proposities. Om het verband tussen formele beweringen en de fysieke realiteit te leggen moet je bij elke propositie aangeven wat in de realiteit moet gelden wil de propositie waar zijn.

In de predikaatlogica kun je veel meer uitdrukken dan in de propositielogica. In plaats van eindig veel proposities heb je eindig veel predikaten, waarvan elk een aantal parameters kan hebben, waardoor men over oneindig veel situaties kan praten. Vaak zal één van deze parameters de tijd zijn, waarop het predikaat waar is. De precieze taal en notatie komt in het hoofdstuk Beweren en bewijzen/de zuilen/Taal uitgebreid aan te orde.

Voorbeelden

We zullen nu formele specificaties en domeinmodellen illustreren aan de hand van een aantal voorbeelden. De formules en domeinmodellen in predicaatlogica staan hier voor een eerste indruk waar we naar toe gaan, maar we zullen in het begin vooral oefenen met de - eenvoudigere maar zwakkere - propositielogica.

Oven

Onze focus is het functioneren van een oven. Veiligheid e.d. vallen buiten de focus en over de precieze spanningen, stromen, temperaturen en vermogens willen we het ook niet hebben. Het gaat alleen om het samenspel van stekker, knop en bakplaat:

Als er spanning op de steker staat en de Aan-knop is ingedrukt, dan is de bakplaat warm.

In propositielogica wordt dit:

Spanning ∧ Aan → Warm

In het domeinmodel geven we aan wat de gebruikte proposities met de realiteit te maken hebben:

domeinmodel

propositie	type	betekenis	meting	formele notatie t.b.v. Coq
Spanning	B	er staat spanning op de stekker	voltmeter	Variable Spanning: B.
Aan	B	de Aan-knop is ingedrukt	bekijken	Variable Aan: B.
Warm	B	de bakplaat is warm	thermometer	Variable Warm: B.

Als we nu een uitgebreidere specificatie maken waarin de oven een opwarmtijd van 8 minuten heeft, dan kunnen we niet langer abstraheren van de tijd en hebben we predikaatlogica nodig. We kunnen dan ook in één moeite door de nodige spanning en de gewenste temperatuur specificeren: "Als de oven 8 minuten lang ingeschakeld is en op 230V is aangesloten, is hij aan het eind van die periode opgewarmd op 180 C." Hier een eerste poging:

(∀t: (0,8], Spanning t 230 ∧ Aan t) → Warm 8 180

(Gemakshalve gebruiken we hier een half-open tijdsinterval als type. Hoe je daarmee in de taal van de logica en bij gebruik van een bewijsassistent precies moet omgaan, staat uitgelegd in de hoofdstukken Typering, Tijd en Tijdslogica.)

We kunnen bij een echte oven op ieder moment beginnen, niet alleen op het moment 0. De specificatie wordt dus:

∀m: T, (∀t: (0,8], Spanning(m+t) 230 ∧ Aan(m+t)) → Warm (m+8) 180

In het domeinmodel moeten we nu predicaten met tijds-, temperatuur- en spanningsparameters gebruiken:

domeinmodel

type		betekenis (verzameling)		formele notatie t.b.v. Coq
T		de tijd in minuten in reële getallen		Definition T := R.
U		de spanning in Volt in reële getallen		Definition U := R.
Tmp		de temperatuur in graden C in reële getallen		Definition Tmp := R.
(t1, t2]		{t: T | t1< t ∧ t ≤ t2}		Zie nadere toelichting.
predikaat	type	betekenis	meting	formele notatie
Spanning	T→U→B	Spanning t v: op moment t staat er v Volt op de steker	voltmeter	Variable Spanning: T->U->B.
Aan	T→B	Aan t: op moment t is de Aan-knop ingedrukt	bekijken	Variable Aan: T->B.
Warm	T→Tmp→B	Warm t x: op moment t is de bakplaat op temperatuur x C	thermometer	Variable Warm: T->Tmp->B.

Dit domeinmodel is ingewikkelder, maar we kunnen er ook veel meer me uitdrukken, bijvoorbeeld de afhankelijkheid van de temperatuur van de verwarmingsduur.

CD-speler

We willen een bepaald muziekstuk s horen:

∀t: (0, duratie s], hoor t (klank (s t))

Hierbij is s een functie van type T→C; dus voor een tijdstip is een klank digitaal beschreven.

Het stuk kiezen we door een cd aan te bieden waarop het staat. Die cd moet de hele tijd beschikbaar zijn, want we denken aan een speler zonder geheugen. Let op de nuance: de hele tijd bieden we een cd aan waarop het hele stuk s staat, maar op elk moment horen we precies dat moment van het stuk.

 (∀t: (0, duratie s], cd t s) → (∀t: (0, duratie s], hoor t (klank (s t)))

Het verhaal moet gelden voor elk willekeurig muziekstuk:

 ∀s: T→C, 
   (∀t: (0, duratie s], cd t s) → (∀t: (0, duratie s], hoor t (klank (s t)))

Bovendien moeten we de mogelijkheid hebben om op elk gewenst moment een stuk te horen:

 ∀m: T, 
   ∀s: T→C,
     (∀t: (0, duratie s], cd (m+t) s) → (∀t: (0, duratie s], hoor (m+t) (klank (s t)))

domeinmodel

type		betekenis (verzameling)		formele notatie t.b.v. Coq
T		de tijd in seconden in reële getallen		Definition T := R.
K		de hoorbare klanken		Variable K: Set.
C		digitale beschrijving van klanken		Variable C: Set.
(t1, t2]		{t: T | t1< t ∧ t ≤ t2}		Zie nadere toelichting.
functie	type	betekenis		formele notatie t.b.v. Coq
duratie	(T→C)→T	duratie s: de duratie van een digitaal beschreven stuk s		Variable duratie: (T->C)->T.
klank	C→K	klank c: de hoorbare klank bij de beschrijving c van een klank		Variable klank: C->K.
predikaat	type	betekenis	meting	formele notatie t.b.v. Coq
cd	T→(T→C)→B	cd t s: op moment t draait in de cd-speler een schijfje waarop stuk s staat	schijfje bekijken	Variable cd: T->(T->C)->B.
hoor	T→K→B	hoor t k: op moment t hoort men klank k	luisteren	Variable hoor: T->K->B.

Politielasergun

Voor een bepaalde auto a, willen we gedurende een tijd van 3000 ms de snelheid die a vlak daarvoor had op een display tonen:

∀s: S, snelheid 0 a s → (∀t: (0, 3000], toon t s)

We moeten in staat zijn dit op ieder gewenst moment te doen:

∀m: T, ∀s: S, snelheid m a s → (∀t: (0, 3000], toon (m+t) s)

We verzwakken de specificatie door te eisen dat voorafgaand aan m, 500 ms op de auto wordt gericht met de loop van de lasergun. Let op de nuance: de hele tijd in (-500, 0] wordt op de auto gericht.

 ∀m: T, (∀t: (-500, 0], richtOp a (m+t))
        →
        (∀s: S, snelheid m a s → (∀t: (0, 3000], toon (m+t) s))

De lasergun moet voor alle auto's werken:

 ∀a:A, 
   ∀m: T, (∀t: (-500, 0], richtOp a (m+t)) 
          →
          (∀s: S, snelheid m a s → (∀t: (0, 3000], toon (m+t) s))

domeinmodel

type		betekenis (verzameling)		formele notatie zonder tabel
T		de tijd in milliseconden in reële getallen		Definition T := R.
A		auto's		Variable A: Set.
S		snelheid in km/u		Variable S: Set.
(t1, t2]		{t: T | t1< t ∧ t ≤ t2}		Zie nadere toelichting.
predikaat	type	betekenis	meting	formele notatie zonder tabel
snelheid	T→A→S→B	snelheid t a s: op moment t heeft auto a snelheid s	met andere apparatuur nameten	Variable snelheid T->A->S->B.
toon	T→S→B	toon t s: op moment t wordt snelheid s op het display getoond	display bekijken	Variable toon: T->S->B.
richtOp	A→T→B	richtOp a t: op moment t wordt de loop op auto a gericht	hoeken opmeten	Variable richtOp: A->T->B.

Kwaliteitscriteria domeinmodel D1. Belangrijk is dat voor elk predikaat in het domeinmodel een meting aangegeven is, waarmee je in de realiteit kunt nagaan of een predikaat waar is. In Beweren en Bewijzen houden we ons alleen bezig met beweringen, opgebouwd uit predikaten die met zo'n meting corresponderen. D2. Een goed domeinmodel is minimaal, d.w.z. het bevat geen elementen die zich door definities laten samenstellen uit andere elementen van dit domeinmodel. (Als een domeinmodel bv. de predikaten 'is kind van' en 'is vrouwelijk' bevat, zijn de predikaten 'is zoon van' en 'is mannelijk' niet nodig, omdat ze zich laten definiëren.) D3. Zorgvuldig en systematisch gekozen namen in het domeinmodel en bij eigen definities kunnen helpen verwarring te voorkomen.