Beweren en bewijzen/de zuilen/Taal/5. Definities

literatuur ...

Declaraties en definities

Een declaratie geeft aan dat er iets met een bepaalde naam en een bepaald type bestaat. Een declaratie zegt echter niets over de waarde. Ieder ding van het type zou het kunnen zijn.

• De declaratie Variable lichtintensiteit: R. declareert een variabele lichtintensiteit, maar zonder te zeggen welke waarde deze heeft.
• Een propositie is niets meer dan een variabele van type B.
• Een nieuw type (mensen) declareert men als volgt: Variable M : Set..
• Op dezelfde wijze kan men functies (en dus ook predikaten) declareren, bv. Variable sofinummerverdeling: M → Z. of het predikaat Variable is_man: M → B.. Wederom zegt men niets over de waarde: sofinummerverdeling kan nog iedere mogelijke functie zijn die aan elk mens een nummer uit Z toekent. Uit het domeinmodel zal blijken dat is_man voor ieder mens vertelt of dit een man is, maar of is_man in het geval David Hasselhoff waar zal zijn wordt in het midden gelaten.

Je gebruikt declaraties voor de proposities, predikaten en abstracte functies in het domeinmodel.

In plaats van declareren kan men ook definiëren. Dit houdt in dat men een naam met type declareert, maar ook zegt welke waarde erbij hoort.

• Zo kan men bijvoorbeeld een constante definiëren: Definition transmissieFactor := 3..
• Of bijvoorbeeld een alias voor een type (windkracht): Definition W := R..
• Maar ook concrete functies, bv. Definition wieken_transmissie (w:W) := 3 * w..
• Of natuurlijk de specificatie van een onderdeel: Definition luidsprekerkabel := (versterker_uit_links -> luidspreker_in_links) /\ (versterker_uit_rechts -> luidspreker_in_rechts).
• Definities gebruik je ook als afkorting voor een ingewikkelde formule die op verschillende plaatsen gebruikt wordt. Je hebt bijvoorbeeld een formule XXXXXXXXXX. Je bedenkt een naam NN voor deze formule. Je definieert: Definition NN := XXXXXXXXXX. en vervolgens kun je overal NN schrijven waar je XXXXXXXXXX bedoelt, de betekenis is precies dezelfde. In sommige talen staat in plaats van de := een =, ::=, ::, DEF= of =DEF - ook hier zijn de meest uiteenlopende notaties gebruikelijk.
• Definities gebruik je ook om hulppredikaten te maken: ingewikkelde combinaties van reeds bekende (hulp)predikaten: Definition is_zoon_van (x:M) (y:M) := is_man x /\ is_kind_van x y..

Je gebruikt definities dus voor aliassen, afkortingen, constanten, hulppredikaten, concrete functies en specificaties.