Beweren en bewijzen/de zuilen/Taal/4. Typering
| literatuur
... |
Inhoud
Syntax en correctheid
Syntax
Binnen een formele taal wordt in eerste instantie via de syntax vastgelegd wat je erin kunt of mag opschrijven. Vaak wordt dat door een grammatica bepaald. Zo is het bijvoorbeeld wel toegestaan om een expressie als 3+7*2 op te schrijven binnen een (normaal gedefinieerde) taal met aritmetische expressies, maar iets als 3+*2 niet.
Getypeerde talen hebben daarbovenop de eis dat wat wordt opgeschreven niet alleen qua syntax klopt, maar ook qua type. Zo is een expressie als 3*4<5 niet alleen goed qua syntax, maar ook qua type. De uit de grammatica afgeleide parseerboom zorgt er hier voor dat eerst de 3 en 4 met elkaar moeten worden vermenigvuldigd om vervolgens die 12 met de 5 te vergelijken. Het eindresultaat zal hier een Boolean zijn. Als we echter de expressie 3 <x< 7 bekijken, is dat binnen de wiskunde een normale manier om aan te geven dat x in het open interval (3,7) zit. Dus qua syntax is dat in die taal wel toegestaan. Echter, als we naar de typering kijken lopen we tegen een probleem aan: de grammatica impliceert misschien wel dat eerst de eerste < moet worden bekeken en daarna de tweede, maar dan levert 3< x een Boolean op die vervolgens moet worden vergeleken met een Integer en het resultaat daarvan is niet bepaald.
Nu is dit voorbeeld van slechte typering misschien ver gezocht, nette talen sluiten zo'n expressie helemaal uit, of spreken expliciet af dat 3 <x< 7 een afkorting is voor 3<x ∧ x<7 en dan gaat het weer helemaal goed met de typering: Integers worden met Integers vergeleken en Booleans worden met Booleans gecombineerd. Later zullen we zien dat het in de predikaatlogica heel gemakkelijk is om iets op te schrijven dat voldoet aan de grammatica, maar qua typering toch fout is.
Types
In het bijzonder hebben we hierboven dus gezien dat het belangrijk is om vast te leggen van wat voor type de verschillende operaties zijn. Hiervoor zijn twee varianten in omloop.
In veel talen leg je de types van operatoren als volgt vast:
<: Integer × Integer → Boolean +: Integer × Integer → Integer *: Integer × Integer → Integer
Hierbij worden deze operaties gezien als iets dat telkens twee argumenten krijgt en er één oplevert.
Wij gebruiken een andere variant, uit de vorige afgeleid door de zog. Currying-techniek. In onze voorbeelden wordt dat:
<: Integer → Integer → Boolean +: Integer → Integer → Integer *: Integer → Integer → Integer
Het idee van Currying is dat de + eigenlijk een operatie is die maar één argument gebruikt en als resultaat geen Integer oplevert maar een operatie van het type Integer → Integer.
Merk op dat → rechtsassociatief is en Integer → Integer → Integer dus gelezen moet worden als Integer → (Integer → Integer).
Deze Currying techniek is heel erg handig bij functionele talen. Zie bijvoorbeeld [1] voor meer informatie.
Predikaten en functies
De voorbeelden hierboven zien er overigens natuurlijk wel heel simpel uit. Het voorbeeld van de CD-speler geeft al aan dat er best ingewikkeldere types voor kunnen komen.
Wat verder opvalt in dat voorbeeld, is het verschil tussen zogenaamde predikaten en functies. Predikaten geven eigenschappen aan en hebben als eindresultaat dus altijd iets van het type Boolean. (De combinatie van de parameters voldoet wel of niet aan de beschreven eigenschap.) In het bijzonder dienen predikaten eigenlijk altijd samen te gaan met zogenaamde metingen: beschrijvingen die uitleggen hoe bepaald kan worden of een predikaat nu wel of niet geldt. Functies daarentegen kunnen elk type als eindresultaat hebben. Ze worden gebruikt om nieuwe objecten te construeren uit reeds bekende objecten. De hierboven genoemde optelling en vermenigvuldiging zijn eenvoudige voorbeelden van functies. In het CD-spelervoorbeeld is s een functie die aan tijdsobjecten een klankobject koppelt.
Predikaatlogica en typering
Getypeerd of niet
Klassieke predikaatlogica kent geen typering. Als we willen aangeven dat slagbomen altijd dicht zijn, ligt het dan ook voor de hand om dat te doen via de formule ∀t, bomendicht t. Maar strikt genomen is dat 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 Tijd noemen, om aan te geven dat t een tijdspunt is: ∀t, Tijd t → bomendicht t Onze taal is een getypeerde logica. Dat houdt in dat bij kwantoren, functieparameters en in definities, kortom overal waar een variabele geïntroduceerd wordt, achter een dubbele punt het type van de nieuwe variabele aangegeven moet worden:
| ongetypeerde logica | getypeerde logica |
|---|---|
| ∀t, Tijd t → P t | ∀t: T, P t |
| ∃t, Tijd t ∧ P t | ∃t: T, P t |
Met ongetypeerde logica moet je dus de beperking met een predikaat formuleren. Bij de universele quantor moet dat met een implicatie, bij de existentiële met een conjunctie. Niet omdat de syntax het voorschrijft maar omdat het anders niet betekent wat je wilt. Dit is "logisch" en berust niet op een afspraak over de notatie.
In een aantal voorbeelden gebruiken we hier ook tijdsintervallen als types, zo als in hoofdstuk Beweren en bewijzen/de zuilen/Formalisering/3. Domeinmodel:
(∀t: (0,8], Spanning t 230 ∧ Aan t) → Warm 8 180
Dit verhoogt de leesbaarheid, maar helaas kan onze bewijsassistent Coq dit niet aan. Alvorens zulke formules met Coq te bewerken, moet men ze dus herschrijven:
| intervallen als types | herschreven naar Coq-syntax | herschreven zonder gebruik van in |
helemaal herschreven naar ongetypeerde logica |
|---|---|---|---|
| ∀ t : (a,b], P t | ∀t: T, t in (a, b] → P t | ∀t: T, (a<t ∧ t<=b) → P t | ∀t, Tijd t → (a<t ∧ t<=b) → P t |
| ∃t, t : (a,b], P t | ∃t: T, t in (a, b] ∧ P t | ∃t: T, (a<t ∧ t<=b) ∧ P t | ∃t, Tijd t ∧ (a<t ∧ t<=b) ∧ P t |
Types in onze grammatica
Onze grammatica (zie Bestand:Grammatica.pdf) definieert niet alleen de syntaxcategorieën die gebruikt moeten worden om een bepaalde tekst te parseren, maar legt tevens allerlei relaties tussen de types vast. Dit gaat via de Griekse letters in de superscripten. Er staat bijvoorbeeld
formuleParsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle ^{B|\tau}}
Volgens de legenda moet dit als volgt gelezen worden. Een element van de syntaxcategorie 'formule' is ofwel van type Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle B} (Boolean) of via een alternatief van type Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \tau} . Maar wat betekent dit nu? Kijken we naar de definitie van 'formule' dan zien we dat er drie alternatieven zijn: een formule met een kwantor waarbij de variabele gekoppeld wordt aan een type, een formule met een kwantor waarbij de variabele gekoppeld wordt aan een interval en een equivalentie. De eerste twee alternatieven zijn beide van type Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle B} omdat dit om 'echte' formules gaat. Het derde alternatief heeft type Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \tau} omdat we hier niet weten of het om een echte equivalentie gaat die een Boolean oplevert of om een oneigenlijke equivalentie die bijvoorbeeld eigenlijk een term is met mogelijkerwijs een heel ander type. In beginsel geven de gebruikte letters Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma} en Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \tau} een willekeurig type aan, tenzij er een beperking op wordt gelegd zoals bijvoorbeeld bij 'product' wordt gedaan: daar moet Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma} ofwel een geheel getal ofwel een reëel getal zijn.
Hoe moeten we nu deze types toepassen? Bekijk het voorbeeld van de term zoals die op de grammatica als voorbeeld is gegeven:
max 3 m
Dit is vermoedelijk bedoeld als een functie die de grootste van de twee getallen 3 en m oplevert. (Het had natuurlijk ook van type R->R->R kunnen zijn, maar dat is hier niet van belang.) Het type van deze functie is dan ook: max: Z -> Z -> Z Een functie met twee argumenten van type Z met als resultaat weer iets van type Z. We geven hier nu de parseerboom van deze term en laten zien dat de types kloppen. Voor het gemak gebruiken we subscripten om aan te geven dat de verschillende Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma} 's in theorie verschillende types zijn.
max 3 m | ||||
In de onderste regel zien we dat de term van type Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \tau_1} is. Een regel daarboven hebben we de hele term opgesplitst in een kleinere term en een waarde. Volgens de grammatica moet die kleinere term van type Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma\rightarrow\tau} zijn, waarbij Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \tau} al vastligt en gelijk moet zijn aan de Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \tau_1} van de onderste regel, maar Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma} nog vrij gekozen kan worden. We kiezen Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma=\sigma_1} om het onderscheid tussen de verschillende Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma} 's te kunnen zien. Door de kolommen in de tabel te volgen zien we hier overigens ook dat 'max 3' een functie is van Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_1\rightarrow\tau_1} , dus een functie met een argument van type Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_1} met als resultaat Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \tau_1} . Uit de grammatica volgt overigens meteen dat het type van de waarde ook diezelfde Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_1} moet zijn.
Gaan we weer een regel omhoog in de grammatica doen we weer hetzelfde. We splitsen de term van type Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_1\rightarrow\tau_1} in een kleinere term en een waarde. Op dit moment heeft de Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \tau} in de grammatica al de waarde Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_1 \rightarrow \tau_1} en mogen we weer een nieuwe Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma} kiezen die het type van de waarde en van de kleinere term vastlegt. We kiezen Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma=\sigma_2} . Vandaar dat het type van de term Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_2\rightarrow(\sigma_1\rightarrow\tau_1)} wordt en dat van de waarde Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_2} .
De term kan niet verder worden opgesplitst en is dus eigenlijk een waarde van het zelfde type Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_2\rightarrow(\sigma_1\rightarrow\tau_1)} . En die waarde is dan weer een naam van hetzelfde type. Het type van deze naam is dan ook precies het type van de functie max: Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_2\rightarrow(\sigma_1\rightarrow\tau_1)} en wegens de rechtsassociativiteit van → is dat gelijk aan Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_2\rightarrow\sigma_1\rightarrow\tau_1} . Omdat we al wisten dat max van type Z → Z → Z is, betekent dat automatisch dat Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_2=Z} , Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma_1=Z} en Parsen mislukt (MathML met SVG- of PNG-terugval (aanbevolen voor moderne browsers en toegankelijkheidshulpmiddelen): Ongeldig antwoord ("Math extension cannot connect to Restbase.") van server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \tau_1=Z} . En dit komt dan weer precies overeen met het feit dat de hele term max 3 m uiteindelijk van type Z is, hetgeen we in de onderste rij van de tabel kunnen zien. Merk verder op dat 3 inderdaad van type Z is en m blijkbaar ook, maar omdat dat een naam is zien we dat niet bovenaan in de tabel, maar op de plaats waar de naam gesplitst gaat worden in tekens. Alles klopt dus inderdaad precies.
Typeringen binnen Coq
Coq houdt zich aan de typeringsregels zoals opgelegd in onze grammatica. Hier zullen we daar een voorbeeld van zien.
Bekijk nu eens de volgende tekst.
Variable P: Set. Variable Q: Set. Variable R: P->Q->B. Theorem g: forall p:P, forall q:Q, R p q. Theorem f: forall p:P, forall q:Q, R q p.
Volgens onze grammatica is deze tekst te parseren als vijf secties, waarvan we hier alleen de boom voor de laatste sectie geven.
Theorem f: forall p:P, forall q:Q, R q p. | |||||||||||||||||||||||
| |
|||||||||||||||||||||||
| |
|
|
|||||||||||||||||||||
Maar er zit toch echt een fout in de typering van de argumenten van R in de laatste regel. Als we deze tekst aan Coq geven via deze commando's
Require Import BenB. Variable P: Set. Variable Q: Set. Variable R: P->Q->B. Theorem g: forall p: P, forall q: Q, R p q. Theorem f: forall p: P, forall q: Q, R q p.
dan krijgen we dit resultaat:
Toplevel input, characters 40-41 > Theorem f: forall p: P, forall q: Q, R q p. > ^ Error: In environment p : P q : Q The term "q" has type "Q" while it is expected to have type "P"
Gelukkig ziet Coq dus dat er fouten in de typering zijn gemaakt! Als we ergens hebben gezegd dat een bepaalde variabele van een bepaald type is, dan zal Coq dat consequent onthouden.
