Hulp
Deze pagina aan uw boek toevoegen
Boek weergeven (27 pagina's)
Pagina's suggererenTestbp
Inhoud
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.
