Beweren en bewijzen/de zuilen/Taal/3. Syntax en semantiek

Uit Werkplaats
Ga naar: navigatie, zoeken
de opzet 2017-18    KalenderIcon.gif multimedia kwaliteit commentaren
site map

Beweren en bewijzen
Wijsheid omgaan met onzekerheid: met open blik op wankele ondergrond levenspad bewandelen
Vernuft aanpak van glibberige problemen precies redeneren op het hoogste niveau
vier zuilen → Artefacten Formalisering Taal Zekerheid
1. Rationaliteit Rationaliteitsvierkant 4 werelden Beweren is moeilijk Overtuigen
2. Modellen Focus Precisie Logica Stelling en bewijs
3. Model en realiteit Specificaties Domeinmodel Syntax en semantiek Waarheid
4. Correctheid Structuur Correctheidsstelling Typering Nagaan
5. Methoden Decompositie Systemat. vertalen Definities Natuurl. deductie
6. Theorie Domeintheorie Tijd Tijdslogica Wiskunde
7. Complexiteit Hiërarch. decompositie Vereenvoudigingen Modules Bewijsassistenten
8. Generalisering Standaardisatie Parametrisatie Talen Hulpstellingen
Beweren en bewijzen/de zuilen/Taal/3. Syntax en semantiek
Ook talen kunnen gemodelleerd worden.
literatuur

Boek Logica voor alfa's en informatici

Syntax

We hebben al eerder deze informele beschrijving van de taal van de predikaatlogica gezien:

De termen van de predikaatlogica worden als volgt geconstrueerd:

  1. individuele variabelen
  2. individuele constanten
  3. als F een k-plaatsige functieletter is en t1,...,tk zijn termen, dan is (F t1...tk) ook een term
  4. niets is een term dan op grond van 1, 2, of 3.

Voorbeelden van termen zijn: windsnelheid, 3, (max 2 3).

De formules van de predikaatlogica worden als volgt geconstrueerd:

  1. Als A een propositieletter is dan is A een formule
  2. als A een k-plaatsige predikaatletter is en t1,...,tk zijn termen, dan is A t1...tk een formule
  3. als s en t termen zijn, dan is s=t een formule
  4. als P en Q formules zijn, dan ook ¬ P, (P ∧ Q), (P ∨ Q), (P → Q) en (P ↔ Q)
  5. als P een formule is, x een individuele variabele, en D een type, dan zijn (∀ x: D, P) en (∃ x: D, P) ook formules
  6. niets is een formule dan op grond van 1, 2, 3, 4 of 5

Voorbeelden van formules zijn: ZonIsOp; isGroterDan 2 3; 2 = 3 ∧ ZonIsOp; ∀y: IJsberen, isWit y.


Iets dergelijks staat ook in veel logicaboeken. Mensen lijken er wijs uit te worden, maar eigenlijk is het raar: er wordt een taal gedefinieerd waarin zo ongeveer alles tussen haakjes moet staan, en vervolgens wordt uitgelegd welke haakjes men weg mag laten.

Grammatica's

Grammatica's worden gebruikt om precies te beschrijven hoe (formele) talen zijn opgebouwd. Op deze pagina beschrijven we de grammatica van de predikaatlogica die we bij dit vak gebruiken. Er zijn verschillende grammatica's bekend voor de predikaatlogica, maar wij houden in dit college vast aan de grammatica die Coq hanteert.

De grammatica van onze taal vind je hier: Bestand:Grammatica.pdf

Constructieboom

Neem de grammatica van onze taal bij de hand. We bekijken de constructieboom (ook syntaxboom genoemd) van de bewering:"Zij x het natuurlijke getal dertien. Driemaal x plus de tweede macht van twee is groter dan x". In onze taal is dat: Definition x := 13. Theorem th1 : 3*x+2^2>x.. Dit is de luifel van de syntaxboom. De afzonderlijke tekens in deze tekst zijn de bladeren. De stam is de syntactische categorie sectie. Deze stam vertakt zich in zich vertakkende takken met namen als abstractie, naamgeving, som, product. Die takken vertakken zich in twijgen zo als naam en constante, en die dragen de bladeren van de categorieën letter, cijfer, maaldoor enz.

Er zijn verschillende manieren om constructiebomen te tekenen. In dit medium kun je niet goed schuine takken en twijgen tekenen, maar 'tables' zijn geen enkel probleem. Met wat visuele fantasie zie je de takken en vertakkingen.

(Nb: deze boom is gebaseerd op de grammatica van versie 02/03/2011. Schrik dus niet als je hem niet helemaal kunt volgen als je hem met een oudere (of nieuwere) versie bekijkt!)

Definition x := 13. Theorem th1 : 3*x+2^2>x.
Definition x := 1 3 . Theorem t h 1 : 3 * x + 2 ^ 2 > x .











constante
eersteteken









constante






waarde
naam


constante
eersteteken



constante





term
waarde
constante
waarde
naam



waarde





macht
term
waarde
term
waarde



term





negatief
macht
term
macht
term



macht





product maaldoor negatief
macht
macht



negatief





product
negatief
negatief



product





som plusminus product
product



som





som kleinergelijkgroter som



vergelijking





vergelijking



negatie





negatie



conjunctie





conjunctie



disjunctie



overigteken
disjunctie



implicatie


overigteken etcetera
implicatie



equivalentie

eersteteken etcetera
equivalentie

eersteteken
formule

naam
formule

naam abstractie
naamgeving
naamgeving sectie
sectie




Let op: Iedereen is het erover eens dat men zo'n structuur 'boom' noemt, vanwege de vertakkingen. Echter, de helft van de informatici, logici, filosofen en taalkundigen tekenen de boom op z'n kop: met de stam bovenaan en de bladeren onderaan. Ook Van Benthem doet dat.

Er zijn twee manieren, voor een gegeven tekst de syntaxboom te construeren: van de bladeren naar de stam (dat noemt men in de informatica bottom-up) en van de stam naar de bladeren (dat noemt men top-down). Pak de Bestand:Grammatica.pdf en volg deze uitleg:

  • Bottom up (van de bladeren naar de stam, als de boom op z'n kop staat is dat dus omhoog)
    • We bekijken het eerste blad: 'Definition'.
    • Dat komt alleen maar voor in een 'naamgeving', dus dit moet onderdeel zijn van zo'n 'naamgeving'.
    • Een naamgeving die met 'Definition' begint, moet verder een 'naam' en een 'abstractie' bevatten en met een '.' worden afgesloten. Die '.' zien we meteen.
    • Nu kijken of we de tussenliggende bladeren kunnen inpassen in een 'naamgeving'.
    • We zien een 'x'. Omdat dit vooraan staat kan het geen 'overigteken' zijn en moet het wel een 'eersteteken' zijn. Zo'n 'eersteteken' is op zich weer een 'naam'. En dat was wat we zochten in de 'naamgeving'
    • Vervolgens zien we ':='. Die komt alleen maar voor in een 'abstractie', wat ook precies past bij een 'naamgeving'. Binnen zo'n 'abstractie' moet de ':=' gevolgd worden door een 'formule'.
    • We zien echter staan '13'. Is dat een 'formule'? Ja, want als we goed kijken zien we dat we de 13 moeten splitsen in een 'constante' (1) gevolgd door een 3. En samen is dat ook weer een 'constante'.
    • Maar een 'constante' is een 'waarde'. Een 'waarde' is een 'term'. En zo verder gaand zien we dat de '13' inderdaad een 'formule' is. Dus het past allemaal precies!
  • Top down (van de stam naar de bladeren, als de boom op z'n kop staat dus omlaag)
    • Het hele ding moet een sectie voorstellen.
    • Er zijn twee soorten secties:
      • Een simpele sectie die eigenlijk een 'naamgeving' is.
      • Een samengestelde sectie die begint met een 'naamgeving' en weer gevolgd wordt door een 'sectie'.
      • Omdat er twee keer een '.' in ons voorbeeld staat, kan het niet slechts één naamgeving zijn en moet het dus wel een 'naamgeving' gevolgd door een 'sectie' zijn.
    • We kijken alleen naar de 'naamgeving', waarvan we drie soorten hebben:
      • Een die begint met 'Variable'.
      • Een die begint met 'Definition'.
      • Een die begint met 'Theorem'.
      • In ons voorbeeld moet het dus het tweede geval zijn en moeten we binnen de 'naamgeving' nog een 'naam' gevolgd door een 'abstractie' krijgen.
    • Laten we alleen even kijken naar die abstractie. Ook hier weer twee soorten:
      • Een die begint met ':='.
      • Een die begint met een 'parameter'.
      • Het is duidelijk dat we hier de eerste variant moeten hebben en dus moeten laten zien dat de '13' die we tussen de ':=' en de '.' hebben staan, precies een 'formule' is. Probeer dat zelf te laten zien!


In de praktijk is men meestal tegelijk bottom up en top down bezig.

De grammatica zit zo in elkaar dat men, klimmende in de boom, langs veel oneigenlijke categorieën komt: een product met maar één factor wordt ook product genoemd. Een disjunctie zonder of-tekens, eigenlijk dus een conjunctie, wordt toch disjunctie genoemd.

Dat leidt in de syntaxboom tot lange rijen opeengestapelde oneigenlijke categorieën.

Als de syntaxboom eenmaal geconstrueerd is, kunnen we de typering controleren.

Opmaak

Wie ingewikkelde formules opschrijft moet alles doen dat de lezer de structuur kan doorgronden. Naast het gebruik van definities speelt de opmaak (layout) een grote rol (zie Beweren en bewijzen/de zuilen/Formalisering/2. Precisie#Leesbaar).

Wie de betekenis van een tekst wil kennen moet allereerst de structuur doorgronden. Bij formele talen betekent dit: de semantiek van de taal is gedefinieerd langs de syntaxis. Om taalconstructen te begrijpen moeten we hun syntaxboom voor ogen kunnen zien.

Pas als we ondubbelzinnige beweringen hebben opgeschreven, heeft het zin te proberen ons gelijk te bewijzen.

nothumb

Semantiek

(modeltheorie)

Overgenomen van "https://lab.cs.ru.nl/algemeen/index.php?title=Beweren_en_bewijzen/de_zuilen/Taal/3._Syntax_en_semantiek&oldid=193600"