TYPENTHEORIE




Algemeen

Tijdens het college zal iedere maandag het huiswerk worden opgegeven voor die woensdag daar op volgend. ( Verandering sinds 13-9: in plaats van maandag, zal al de vrijdag daarvoor het huiswerk bekend zijn. zodoende heeft men ook nog het week einde om er naar te kijken. De opgaven zullen via deze pagina bekend worden gemaakt.) Het huiswerk dient dan ingeleverd te worden uiterlijk aan het begin van het werkcollege. Inleveren kan ook of persoonlijk in kamer 438, of via mijn postvakje in de docentenkamer, of electronisch naar
Joost Joosten
In het laatste geval heb ik het liefst een .ps formaat.

Voor algemene informatie over het hoorcollege en tentamenregeling zie Vincent van Oostrom.

Week 1

Woensdag 6 september er op het werkcollege de volgende sommen behandeld: 1.7.2. 1,2 en 3 ---- 1.7.3. ---- 1.7.4. 1,2 en 5 ---- 1.7.5. 1,2 en 5 ---- en 1.7.6. 1. Het Huiswerk voor de eerste week bestaat uit het volgende: 1.7.2. 4 [2] en 5, 1.7.4. 3 en 4 [2], 1.7.5. 3 en 4 [2] , 1.7.6. 2 en 3 [2], en een opgave die op het bord is geschreven [2]. (De aanduiding tussen de vierkante haken geeft aan hoeveel punten er bij die opgeve te vergeven waren.) De opgave die op het bord was geschreven is de volgende.

Je werkt met abstracte pijltjes (dus dit hoeft niet per se beta conversie te zijn) tussen abstracte objecten(dus niet per se lambda termen). De corresponderende multi-pijl is zoals altijd de transitieve, reflexieve afsluiting van de pijl. Er wordt nu gevraagd om een tegenmodel te geven voor { Als [(w pijl x en w pijl y) impliceeert het bestaan van een z met (x multipijl z en y multipijl z)] dan ook [(w multipijl x en w multipijl y) impliceeert het bestaan van een z met (x multipijl z en y multipijl z)]} . Merk op dat Church-Rosser uitsluit dat de lambda termen samen met de beta-pijlen een gezocht tegenmodel is!

Het is de bedoeling (in tegenstelling to de komende weken) dat de opgaven aan het eind van deze week worden ingeleverd, dat wil dus zeggen, voor vrijdag 8 september, zeg zes uur. Inleveren kan of persoonlijk in kamer 438, of via mijn postvakje in de docentenkamer, of electronisch naar
Joost Joosten
In het laatste geval heb ik het liefst een .ps formaat.
  • Uitwerkingen huiswerk week 1, beknopt doch correct
    [ DVI | Postscript| Pdf formaat]

    • Week 2

    Maandag 11-9-`00 is een aantal sommen opgegeven die dus woensdag de 13-de aan het begin van het werkcollege ingeleverd dienen te worden. (Of daarvoor natuurlijk.) Het huiswerk is: 1.7.10 [5], 1.7.13 [2] en 1.7.14. [3-4]
    In de werkgroep is er aan de volgende sommen gewerkt: 1.7.16, 1.7.17, 1.7.18, 1.7.22 en 3.6.1. Eigenlijk zijn we er alleen maar aan toe gekomen om 1.7.17 volledig te behandelen. Ook is er gesproken over inductieve definities en inductieve bewijzen.

    Week 3

    Hier het huiswerk dat woensdag 20 september op z'n laatst ingeleverd kan worden.
    1.7.18 [1],
    1.7.21 [3],
    1.7.22 [3],
    en
    3.6.1 [3].

    Week 4

    Op het hoorcollege zijn de volgende sommen behandeld: 3.6.2., 3.6.3., en een aantal sommetjes die niet in de syllabus staan zoals, geef een formele afleiding van het type van S (= \xyz.xz(yz) example 3.1.2. in de reader), bewijs de abstractie-stap in het inductieve bewijs van de subject reductie eigenschap, bewijs mbv volledige inductie de subject reductie eigenschap voor de beta-multipijl. Het huiswerk voor deze week is:

    a.) Het is mogelijk om de numerals te typeren (a la Church) zodanig dat alle numerals hetzelfde type hebben? Geef zo'n typering.
    b.) Is een lambda term (in normaalvorm) een numeral dan en slechts dan als hij van het bij a.) gegeven type is? Licht toe.
    en uit de reader:
    3.6.5, en
    3.6.11

    En verder:
    Verifieer a.) voor de numeral c_5 en 3.6.11 mbv Coq. Dwz zie de gevonden typen als formules van minimal logic en vind bewijzen van deze formules die corresponderen met de lambda-termen. Een kopie van de sessie volstaat.
    Joost Joosten
    Last modified: Wed Sep 27 10:28:16 MET DST 2000