Beweren en bewijzen/de zuilen/Taal/6. Tijdslogica
| literatuur |
Inhoud
Types
Vaak wil je in zulke specificaties kwantificeren over de tijd. Stel je wilt eisen dat de slagbomen altijd dicht zijn.
∀t, bomen dicht t
is streng genomen niet juist, want t zou ook iets anders dan een tijdspunt kunnen zijn. Volgens Van Benthem heb je dan een predikaat nodig, laten we het T noemen, om aan te geven dat t een tijdspunt is:
∀t, T t → bomen dicht t
Onze taal gaat verder dan Van Benthem: het is een getypeerde logica. Hier geef je bij elke kwantor met een dubbele punt de verzameling aan, waaruit de waarden voor de gekwantificeerde variabele mogen komen:
∀t:T, bomen dicht t
Een klok is een apparaat dat op elk moment t een representatie van dat moment aangeeft, bijvoorbeeld door wijzers in een bepaalde hoek te draaien:
Definition klok := ∀t:T, wijs t (repr t)
Bij grotere specificaties is het gebruik van getypeerde logica zeker aan te bevelen. Daarom gebruiken we in Beweren en Bewijzen getypeerde logica.
Intervallen
In specificaties wil je vaak praten over tijdsintervallen. Dat kan gewoon met de rekenkundige vergelijkingsoperatoren:
t<t1 ∧ t1<t+d
geeft aan dat t1 in het open interval (t, t+d) ligt.
LET OP: veel mensen korten t<t1 ∧ t1<t+d af tot t<t1<t+d. Informeel is dat gebruikelijk. In de strenge taal van de logica kun je deze formule niet typeren en heeft ze geen betekenis: t<t1 is een predikaat en dus waar of onwaar. En een waarheidswaarde kun je niet vergelijken met een moment! Haal je de systaxboom voor ogen en je ziet het. Als je in deze cursus iets als t<t1<t+d opschrijft en er mogelijk ook nog Coq mee lastig valt, is het niet meer dan de beruchte taalfout: taalkitsch .
In specificaties van temporeel gedrag hebben we vaak intervallen nodig, bijv.:
∀t:T, t1<t∧t≤t2 → P t
Het is gebruikelijk om zo'n half-open interval zo te schrijven:
∀t:T, t∈(t1,t2] → P t
In een getypeerde logica kunnen we nog een stap verder gaan en het interval als type gebruiken:
∀t: (t1,t2], P t
De bewijsregels voor natuurlijke deductie kennen geen types. Op de pagina over onze taal staat een tabel met de notatie en de Coq notatie. Je ziet dat je in Coq geen intervallen als types mag gebruiken. Daarom moet je, om iets conform de deductieregels te kunnen bewijzen, je formules weer omzetten, hetzij naar ongetypeerde logica zonder intervallen, hetzij naar Coq-notatie met in.
Voorbeelden
In een paar eenvoudige voorbeelden komt vrijwel alles voor, wat je voor specificaties van tijdcritische systemen nodig hebt.
Een domeinmodel voor wekkers in tijdschakelaars
| type | betekenis (verzameling) | ||
|---|---|---|---|
| T | de tijd, d.w.z. de verzameling van momenten. In dit voorbeeld reële getallen, eenheid: sec. | ||
| D | de verzameling van duraties. In dit voorbeeld niet negatieve reële getallen, eenheid: sec. | ||
| K | de verzameling van representaties van momenten en duraties op klokken | ||
| B | {false, true} aanwezig in Coq als standaard type | ||
| functie | type | betekenis | |
| repr | T→K | repr t: de representatie van moment t op de wijzerplaat van de klok (bv. hoeken van wijzers) | |
| zrepr | T→K | zrepr t: de representatie van de gewenste kooktijd bij het instellen (bv positie van een instelschroef) | |
| predicaat | type | betekenis | |
| wijst | T→K→B | wijst t1 (repr t2): op moment t1 wijst de klok de representatie van tijd t2 aan | |
| gezet | T→K→B | gezet t1 (zrepr t2): op moment t1 wordt de klok gezet op t2 | |
| rinkelt | T→B | rinkelt t: op moment t is een rinkelsignaal hoorbaar | |
| flip | T→B | flip t: op moment t krijgt de flipflop een impuls | |
| is | T→B→B | is t false: op moment t is de toestand van de flipflop: 0 | |
| stroom | T→B | stroom t: op moment t staat de lamp onder stroom | |
De absolute klok
∀t:T, wijst t (repr t)
Een klok die gelijkgezet kan worden
∀t:T, ∀t0:T, ∀d:D, gezet t (repr t0) ∧ (∀t1:(t,t+d], ¬(∃x:K, gezet t1 x)) → wijst (t+d) (repr (t0+d))
Een kookwekker
∃r:(1,3],
(∀t:T, ∀d:D,
gezet t (zrepr d)
∧ (∀t1: (t,t+d], ¬(∃x:K, gezet t1 x))
→
(∀a:(t+d,t+d+r), rinkelt a)
)
/\
(∀ a:T,
rinkelt a
→
(∃t:[a-r,a], ∃d:D, gezet (t-d) (zrepr d))
)
Flip-flop
In de literatuur wordt de term flip-flop voor een aantal dingen gebruikt. Dit is de meest eenvoudige. Het ding staat op 0 dan wel 1 zolang er geen flip-signaal komt. Bij een flip wisselt het van 0 naar 1 of juist van 1 naar 0.
∀t:T, ∀ d:D, ∀x:B,
is t x ∧ flip t ∧ (∀t1:(t,t+d), ¬ flip t1)
→
is (t+d) (~x)
"Als het nu op 0 (dan wel 1) staat en nu een flip-signaal komt en dan tot op een willekeurig volgend moment geen zo'n signaal komt, dan staat het op dat moment op 1 (dan wel 0)." Hieruit volgt, dat het ook op alle momenten tussen t en t+d op deze stand staat.
Dit is de hoge kunst van het specificeren. Men heeft de neiging om veel meer te vertellen:
∀t:T, ∀ d:D, ∀x:B,
is t x ∧ flip t ∧ flip (t+d) ∧ (∀t1:(t,t+d), ¬ flip t1)
→
(∀t1:(t,t+d], is t1 (~x))
"Bij een flip wisselt het van toestand, waarop de toestand onveranderd blijft tot de volgende flip." Dat klopt, maar dit is dus een logisch gevolg van de vorige specificatie. Je kunt het bewijzen.
Waarom is de eerste specificatie dan beter?
- Ze is eenvoudiger. Wetenschappers houden van eenvoud. Als ze een eenvoudige formule nog niet helemaal vertrouwen, proberen ze er de dingen die men zou verwachten uit te bewijzen. In casu dus de tweede formule.
- Zo'n flipflop wordt gebruikt als onderdeel van een groter artefact. Bij het bewijzen van diens correctheidsstelling moet men bewijzen dat het flipflop op een bepaald moment een zekere waarde heeft.
lamp
∀t:T, stroom t ↔ licht t
drieminutenlicht
Hier vind je een uitgebreide casus met bewijs.
stoplicht
Hier vind je een uitgebreide casus met bewijs.
