I00091 (I00091)
Semantiek en logica 2*
< 2006/2007 > 04-09-2006 t/m 20-01-2007 () H
Informatica - Bachelor (2003) Software: Programmeren en algoritmiek (2 ec) (2 ec) Grondslagen (4 ec) (4 ec)
omvang
6 ec (168 uur) : 32 uur plenair college, 32 uur groepsgewijs college, 0 uur computerpracticum, 8 uur 'droog' practicum, 0 uur gesprekken met de docent, 36 uur onderling overleg met medestudenten (werkgroepen, projectwerk e.d.), 60 uur zelfstudie
investering
6 ec * 28 u/ec + #std * (1 + 6ec * 0.15 u/student/ec)
inzet tentatief

examinator
afdeling
tijdbesteding

prof. dr. Erik Barendsen
sws
105u.

docent
afdeling
tijdbesteding

prof. dr. Herman Geuvers
sws
105u.

speciale web-site
/E.Barendsen/onderwijs/sl2/

 

Ook in deze vervolgcursus leer je formele methoden ontwikkelen en gebruiken in de informatica.

We bekijken geavanceerde formalismen om de operationele semantiek van programmeertalen en taalconstructies vast te leggen. Je zult in deze cursus imperatieve, functionele en logische talen tegenkomen.

Je leert de formele technieken gebruiken voor taalontwerp, analyse van berekeningen en programmaverificatie (soms met een tool).

We onderzoeken de grenzen van formele logische systemen: naast de volledigheid van de predicatenlogica maak je kennis met onvolledigheidsresultaten.

Als informaticus zul je formele methoden niet alleen toepassen, maar ook zelf formalismen moeten beoordelen, uitbreiden of ontwikkelen. Daarom gaat deze cursus ook over de eigenschappen van de formele systemen zelf: de metatheorie.

Leerdoelen

Na afloop van deze cursus kunnen de deelnemers:

  • Betekenis van imperatieve taalconstructies vastleggen met inductieve formele technieken. Verschillende beschrijvingsvormen inzetten en voor een gegeven toepassing een verantwoorde keuze maken. Het effect van taalontwerpbeslissingen zoals parameteroverdracht en scoperegels verklaren.
  • Eigenschappen van programma's specificeren in een formalisme en de correctheid verifiëren met behulp van geautomatiseerde technieken.
  • Berekeningen in functionele talen modelleren in lambda-calculus. Berekeningen in dit herschrijfmodel analyseren. Typeringssystemen modelleren via typetoewijzingssystemen in de lambda-calculus.
  • Semantiek van logisch programmeren vastleggen via resolutielogica.
  • Mogelijkheden en beperkingen van predicaatlogische systemen aangeven met betekking tot uitdrukkingskracht en beslisbaarheid.

Onderwerpen

  • Semantiek van imperatieve talen: structurele operationele semantiek, parallellisme, nondeterminisme, scope, procedure-evaluatie, recursie
  • Specificatieformalismen: JML tools
  • Lambda-calculus: bèta-reductie, confluentie, normalisatie, representatie berekenbare functies, typering, unificatie
  • Semantiek van logische talen: resolutie
  • Axiomatische systemen: onvolledigheid, beslisbaarheid

Werkvormen

Taakgestuurd onderwijs, met een cyclus van oriëntatie (hoorcolleges), zelfstudie (leertaken) en nabespreking (responsiecolleges). Een werkstuk met bespreking. Case study.

Voor communicatie (mededelingen, e-mail, beoordelingen) gebruiken we Blackboard.

Vereiste voorkennis

Om deze cursus succesvol te kunnen volgen voldoe je aan de volgende voorwaarden.

  • Je hebt programmeerervaring met imperatieve, functionele en logische talen (zoals in de cursussen rond programmeren en kunstmatige intelligentie, eventueel parallel te volgen).

Je kunt:

  • (Programmeer)talen en taaluitbreidingen specificeren met behulp van reguliere expressies en contextvrije grammatica's (zoals in de cursus Talen en automaten).
  • Berekenbaarheid van numerieke operaties aantonen (zoals in de cursus Berekenbaarheid).
  • Helder formuleren, zowel bij het motiveren van oplossingen als het weergeven van wiskundige redeneringen (zoals in de voorafgaande cursussen in de wiskunde en de theoretische informatica).
  • Betekenis van imperatieve taalconstructies vastleggen met behulp van natuurlijke semantiek (ns) (zoals in de cursus Semantiek en Logica 1)
  • Afleidingen voor propositie- en predicaatlogica opstellen in natuurlijke-deductiestijl. Constructieve en (essentieel) niet-constructieve constructies onderscheiden (zoals in de cursus Semantiek en Logica 1).
  • De relatie tussen syntaxis (taal) en semantiek (model) aanduiden. Bewijs- en modeltheoretische eigenschappen onderzoeken en hun onderlinge verbanden verklaren (zoals in de cursus Semantiek en Logica 1).
  • Eigenschappen van programma's (waaronder correctheid) aantonen met behulp van correctheidscalculi.
  • Berekeningen in functionele talen modelleren met behulp van termherschrijfsystemen. Berekeningen in termherschrijfsystemen analyseren, bijvoorbeeld confluentie- en terminatiegedrag.

Tentaminering

De beoordeling is gebaseerd op vier resultaten:

  • het practicum (de case study over specificatieformalismen),
  • het werkstuk over semantiek van imperatieve talen,
  • een deeltentamen over het onderdeel lambda-calculus,
  • een deeltentamen over de onderdelen semantiek van logische talen en axiomatische systemen.

Om voor een beoordeling in aanmerking te komen, moet je het practicum met voldoende resultaat hebben afgerond. Het eindcijfer is dan het gemiddelde van de beoordelingen van het werkstuk en de twee deeltentamens.

Combinatiemogelijkheden

Volgt op de cursus Semantiek en Logica 1. Bereidt voor op onderwijs waarin formalismen en modellen van berekeningen worden gebruikt. Verdere ontwikkeling van semantiek en typering vindt plaats in de mastercursussen Semantiek en Type Theory.

Literatuur

  • Hanne Riis Nielson en Flemming Nielson: Semantics with applications, 1999 (via internet: PDF)
  • J.F.A.K. van Benthem, H.P. van Ditmarsch, J. Ketting, J.S. Lodder en W.P.M. Meyer-Viol: Logica voor informatica, derde editie, Pearson Education, 2003, ISBN 90-430-0722-6.
    (Dit boek wordt ook in de cursussen Beweren en Bewijzen en Semantiek en Logica 1 gebruikt.)
  • Henk Barendregt en Erik Barendsen: Introduction to lambda calculus (elektronisch document)
  • Opgavenbundel lambda-calculus
  • Aanvullend materiaal


Evaluatie: studentenquêtes ; geen docentevaluatie bekend Rendement: 25 begonnen, echt meegedaan, geslaagd met 1e kans, geslaagd totaal
Q: