Semantiek en berekeningsmodellen (2IF55)

1. Behandeld op 12 november 2009: de notie formele afleiding en Exercises 1.1 en 1.2 uit het boek.
   Eerste inleveropgave [ps,pdf]. (Inleveren op donderdag 19 november aan het begin van de instructie).
2. Behandeld op 19 november 2009: Exercises 1.5 en 1.9.
   Tweede inleveropgave is Exercise 1.10 (blz. 76) uit het boek. (Inleveren uitgesteld tot donderdag 3 december aan het begin van de instructie.)
   
3. Behandeld op 26 november 2009: eerste inleveropgave, bewijs van (M1) van de tweede inleveropgave, Exercise 1.4, argument dat Term uit Exercise 1.10 i.h.a. niet compleet is.
   Derde inleveropgave: bewijs de claim in Lemma 1.41 voor de gevallen p1=a, p1=a.p1'  en p1=a.p1', p1=a.p1'. (Inleveren op donderdag 3 december aan het begin van de instructie.)
4. Behandeld op 3 december 2009: Exercises 1.8, 1.12.
   Vierde inleveropgave: Exercise 1.15(b). (Inleveren op donderdag 10 december 2009 aan het begin van de instructie.)
   
Hints bij inleveropgave:

Zie Lemma 1.38 voor een voorbeeldtoepassing van de epsilon<=epsilon/2 techniek.
Gebruik inductie naar wgt(\pi).
In het geval \pi=(D|s1;s2), gebruik (of beter nog: bewijs) dat O(D|s1;s2)=O(D|s1);O(D|s2) en gebruik Lemma 1.41.
5. Behandeld op 10 december 2009: 1.12(b), 1.13, 1.14 (begin voorgedaan, zelf afmaken!).
   Vijfde inleveropgave:
   
   Neem aan dat D(x)=a;y;c en D(y)=b;x (met a,b,c in Act en x,y in PVar).
   Bepaal de eerste vier transities van de transitierij die begint met x (geef ook de vier bijbehorende afleidingen).
   Gok vervolgens O(D|x) en controleer of je gok klopt door te controleren of O(D|x)=D(D|x).
   (Zie ook Lem. 1.43 voor inspiratie!)
(Inleveren op donderdag 17 december 2009 aan het begin van de instructie.)
6. Behandeld op 17 december 2009: 1.15, voorbeelden operationele semantiek Lwh.
   Zesde inleveropgave: 1.18(b) en bewijs, gebruikmakend van de epsilon <= epsilon/2 methode, dat O(D|s1;s2)=O(D|s1);O(D|s2).
   (Inleveren op donderdag 7 januari 2010 aan het begin van de instructie.)
7. Behandeld op 7 januari 2010: 1.18, 1.21 (de uitbreiding van O met "repeat s until e end" is behandeld; doe zelf de rest van de opgave!).
   Zevende inleveropgave: Vul het bewijs van Lemma 1.63(a) aan met een behandeling van de gevallen [skip] en [if e then s1 else s2 fi]; vul het bewijs van Lemma 1.63(b) aan met een behandeling van de gevallen [v:=e] en [while e do s od]; en vul het bewijs van Lemma 1.65 aan met een behandeling van het geval [if e then s1 else s2 fi]. (Inleveren op donderdag 14 januari 2010 aan het begin van de instructie.)

• Uitwerking tweede inleveropgave [ps,pdf]
• Uitwerking van de vierde inleveropgave (incl. een bewijs dat O(D|s1;s2)=O(D|s1);O(D|s2) met de epsilon <= epsilon/2 methode) [ps,pdf]

Laatste wijziging: 08 januari 2010