Formele systemen en hun toepassingen

Ga naar: navigatie, zoeken
Dave Clarke
Frank Piessens

Samenvattingen

Klik hier om de samenvattingen te bekijken

Examenvragen

2015-2016

2016-01-13 09u00

docent: Dominique Devriese (als vervanger voor Frank Piessens)

  1. Gegeven het formularium van untyped lambda calculus (met alles er in wat relevant is: syntax, e-rules, t-rules, ...). Dit formularium implementeert call-by-value. Geef een nieuwe set van evaluatieregels voor full beta evaluation (non-deterministic) Geef een vb. van een term die wel evalueert met de nieuwe regels, maar niet bij call-by-value.
  2. Gegeven het formularium van untyped lambda calculus. Eindigt de evaluatie van twee gegeven termen? Zo ja, geef de volledige evaluatie. Zo nee, geef de eerste 3 stappen en leg uit waarom niet. Iets in de trent van en ongeveer dezelfde term met een iets andere fix.
  3. Gegeven het formularium van System F. Formuleer het theorem van progress voor System F + bewijs. De nodige lemma's zijn gegeven en moeten niet bewezen worden.
  4. Gegeven het formularium van STLC + Base types + booleans. Ook gegeven de bewijzen van de normalization stelling voor STLC, samen met de lemma's en hun bewijzen (en de definitie van R_T). Breid het gegeven bewijs voor normalisation uit.
  5. Verdediging van het project. (Dit jaar geschreven in de taal Agda.)

2016-01-08 09u00

docent: Dominique Devriese (als vervanger voor Frank Piessens)

  1. Gegeven het formularium van untyped lambda calculus (met alles er in wat relevant is: syntax, e-rules, t-rules, ...). Dit formularium implementeert call-by-value. Geef een nieuwe set van evaluatieregels voor call-by-name/ Geef een vb. van een term die wel evalueert met de regels van call-by-name, maar niet bij call-by-value.
  2. Gegeven het formularium van STLC + references + let. Eindigt de evaluatie van de volgende term? Zo ja, geef de volledige evaluatie. Zo nee, geef de eerste 7 stappen en leg uit waarom niet.
  3. Gegeven het formularium van System F. Formuleer het theorem van preservation voor System F + bewijs. De nodige lemma's zijn gegeven en moeten niet bewezen worden.
  4. Gegeven het formularium van STLC + uitbreiding fix. Ook gegeven de bewijzen van de normalization stelling voor STLC, samen met de lemma's en hun bewijzen (en de definitie van R_T). Normalization geldt niet meer in STLC + fix. Leg uit waarom niet (specifieker: geldt de definitie nog? Welke lemma's gelden nog steeds/niet meer? Moeten er bewijzen uitgebreid worden wegens de nieuwe syntax (van fix)? Welke bewijzen ondervinden problemen, en waar? Enz.).
  5. Verdediging van het project. (Dit jaar geschreven in de taal Agda.)

2012-2013

docent: Frank Piessens

  1. Simply typed lambda-calculus met references, let, Unit, ... (regels gegeven in formularium)
    1. Eindigt de evaluatie van de volgende term? Zo ja, geef de volledige evaluatie. Zo nee, geef de eerste 5 stappen en leg uit waarom niet.
    2. Geef de preservation-stelling voor deze calculus (geen bewijs).
  2. Simply typed lambda-calculus met subtyping (geen records): bewijs minimal typing.
  3. Featherweight Java. Waarom is de volgende stelling fout? Als en dan is . Geef een tegenvoorbeeld en een gecorrigeerde versie van deze stelling.
  4. Verdediging van het project (System F).


2010-2011

docent: Dave Clarke

Je kreeg een formularium met alle relevante regels.

  1. Untyped Lambda-expressies evalueren met alle tussenstappen: niet van hoog niveau
  2. Arithmetic expressions and booleans
    1. Evalueren van een term met small-step (met transitieve sluiting = ) en (gegeven) big-step semantics
    2. Bewijsjes (induction):
      1. eindigt altijd met e' normal form
      2. evaluatie met de gegeven big-step semantics is deterministisch
      3. en big step semantics zijn equivalent
  3. FJ uitbreiden met errors en Exceptions. Rekening houden met:
    1. evaluatie
    2. typing, subtyping
    3. try/catch
  4. Realistische Store: semantics en typing uitwerken voor een store waar je locations kan vrijmaken met een 'free' operator. Rekening houden met het hergebruiken van locations en dangling references (opvragen van vrijgemaakte locatie in de store). Wat als je geen 'errors' wilt krijgen at runtime? = hoe kan je at compile-time nagaan of je geen typeringsfouten/dangling references hebt?

2009-2010

docent: Dave Clarke

Je kreeg een formularium met alle relevante regels.

  1. Inductive definitions.
    1. Gegeven was een inductieve definitie van een relatie "weird". De relatie gedefinieerd door de inductieve regels is de kleinste relatie gesloten onder de regels. Je moest dan voor een zestal termen aantonen of deze af te leiden m.b.v. de regels of niet.
    2. Welke regels kunnen weggelaten worden? (M.a.w. zodat de set van regels nog steeds exact dezelfde relatie definieert).
  2. STLC met references, let, ...
    1. Gegeven waren een drietal termen. Hiervan moest je de eind-value (na reductie) geven, evenals de uiteindelijke store. Je moest vertrekken van een lege store.
    2. Preservation theorem: gegeven was het theorem. Dan waren er een paar "alternatieven" gegeven die fout waren. Je moest een term geven waar deze "alternatieven" faalden.
      1. Bij de eerste was de assumptie weggelaten dat de initiele store well-typed moet zijn w.r.t. context en store typing
      2. Bij de tweede stond er in plaats van SOME Sigma' ALL Sigma'.
  3. STLC met subtyping
    1. Gegeven enkele expressies in STLC. Geef van elk de MINIMALE typing of schrijf NONE indien de term niet getypeerd kan worden.
    2. Stel dat we volgende regel toevoegen: Top <: {}. Blijft progress gelden? Geef kort aan waarom wel/niet.
    3. Stel dat we volgende regel toevoegen: Top->Top <: Top. Blijft progress gelden? Geef kort aan waarom wel/niet.
    4. De subtyping regel voor references is nogal strikt. (Nl. types moeten INvariant zijn). We kunnen beter doen: Ref S T waarmee bedoeld wordt dat S het type is voor schrijven en T het type voor lezen. Bij constructie zijn S en T gelijk.

Volgende regels worden gegeven:

T-REF: t : T


ref t : Ref T T

T-DEREF: r : Ref S T


!r : S

T-ASSIGN: r : Ref S T t : T


r := t : Unit

Gevraagd: geef de SUBtyping rule voor Ref S T.

  1. Project verdedigen (als het goed was wordt hier niet naar gekeken)


Sinds 2008-2009 wordt dit vak gegeven door Dave Clarke, waardoor de vragen hieronder niet irrelevant maar wel outdated zijn geworden.

2007-2008

2008-01-21 9h

Noot: Vanaf 2008 gaat het vak niet meer over de -calculus maar over de -calculus en type-systemen.

  1. Gegeven een term in de untyped lamda calculus: Geef een typering zodt de term welgetypeerd is en geef de type-afleiding
  2. Formuleer en bewijs progress voor de simply-typed--calculus met subtyping, records en variants
  3. De standaard preservation stelling is gegeven. Deze is niet correct voor Featherweight Java. Leg uit en geef een tegenvoorbeeld en geef de juiste stelling.
  4. Projectverdediging

2006-2007

2007-02-02 9h

  1. Definiëer bissimulatie + voorbeelden & tegenvoorbeelden (5pt)
  2. Formuleer & bewijs unique solutions (7pt)
  3. Hoe worden datastructuren in pi-calculus voorgesteld + leg verschil tussen volatile & persistent data uit. (8pt)

2007-01-16 9h

  1. Er is een relatie gedefinieerd tussen transities en reacties. Geef en bewijs.
  2. Definieer de notie van "sterke simulatie tot op ~" (strong simulation up to ~) en formuleer en bewijs het verband met sterke equivalentie voor concurrente proces expressies.
  3. Geef een mogelijke representatie van binaire bomen in de -calculus.

2005-2006

2006-02-03 9h

Volgend weinig origineel vragen trio:

  1. Definieer de notie van "sterke simulatie tot op ~" (strong simulation up to ~) en formuleer en bewijs het verband met sterke equivalentie voor concurrente proces expressies.
  2. Formuleer en bewijs "Unique solution of equations".
  3. Geef een mogelijke representatie van binaire bomen in de -calculus.

26-01-06 14u

1. Er is een relatie gedefinieerd tussen transities en reacties. Geef en bewijs.

2. Hoe kan je recursieve proces definities simuleren met behulp van de ! operator in de -calculus?

3. Kan je een M en N vinden waarvoor en niet zwak equivalent() zijn? Zo ja, geef een A en B. Zo nee, bewijs.

(Spoilers: 1. Stelling 5.6 | 2. p. 95 | 3. Nee)

2004-2005

17-01-05 9u

1. Definieer de notie van "zwakke simulatie tot op ~" (weak simulation up to ~) en formuleer en bewijs het verband met zwakke equivalentie voor concurrente proces expressies (7 punten)

2. Geef een mogelijke representatie van binaire bomen in de -calculus (7 punten)

3. Bespreek waarom klassieke equivalentie van automaten (de zogenaamde taal-equivalentie) niet geschikt is als equivalentie-maat voor reactieve systemen (6 punten)


Bijvragen:

1. betekent dat er verschillende acties voor en achter kunnen voorkomen. als P~Q en PP' en dus QQ' met P'~Q' zijn die sequenties van 's en hetzelfde voor beiden experimenten?

2. geen

3. stel dat we systemen beschouwen zonder interne reacties en we daar ~ op definieren. Is dit dan een voldoende maat om systemen equivalent te noemen of kan je een voorbeeld geven van twee systemen die ~ zijn maar niet observationeel hetzelfde doen?

17-01-05 14u

1. Bewijs dat sterke equivalentie een procescongruentie is.

2. Hoe kan je recursieve proces definities simuleren met behulp van de ! operator in de -calculus?

3. Kan je een M en N vinden waarvoor en niet zwak equivalent zijn? Zo ja, geef een A en B. Zo nee, bewijs.

05-02-05 9u

1. Formuleer en bewijs "Unique solution of equations".

2. Schrijf een sequential process expression voor een binaire stack + teken een deel van de (oneindige) transitiegraaf.

3. Bespreek hoe je datastructuren kunt voorstellen in de -calculus (= booleans + lijsten geven en uitleggen). Vluchtige (ephemeral) en persistente data uitleggen en verschil geven.

2003-2004

30-01-04

1) Geef de definitie van bisimulatie, geef ook vb'en en tegenvb'en.

2) Definieer een sequentiele proces dat een stapel van booleaanse waarden voorstelt (=specificatie), geef een implementatie van zo'n stapel mbv concurrente proces expressies (opgebouwd uit een aantal kleine bouwstenen). Leg uit (in grote lijnen) hoe je de correctheid van je implementatie kan bewijzen.

3) Er is een relatie gedefinieerd tussen transities en reacties. Geef en bewijs.

19-01-04

1) Leg uit waarom klassieke equivalentie van automaten ( taal-equivalentie ) ontoereikend is voor reactieve systemen

-> Gewoon schema'tje tekenen van die koffie/thee automaat

2) formuleer de stelling ivm de unieke oplossing van een stelsel vergelijkingen en bewijs ze

-> Maak vooral ivm theorië dat ge de intuïtie erachter snapt

3) Kan je een M en N vinden waarvoor en niet zwak equivalent() zijn? Zo ja, geef een A en B. Zo nee, bewijs.

-> A & B altijd zwak equivalent -> Intuïtie achter bewijs opnieuw belangrijk


Al bij al niet zo moeilijk, als ge't snapt moet het zeker lukken... Hij stelt wat bijvragen ( heeft mij erin laten lopen bij vraag 1:

. zijn states, abcd externe actions
    .            .
   / \           |
  a   a          a
 /     \         |
.       .        .
|       |       / \
b       b      b   b
|       |     /     \
.       .    .       .
|       |    |       |
c       d    c       d
|       |    |       |
.       .    .       .

zijn deze sterk equivalent? kan men ze observationeel onderscheiden?

2002-2003

18-08-03

1) Geef een sequentiele proces expressie voor een binaire stack (die oneindig kan groeien) teken hiervan het transitie-diagramma

2) Hoe kan je recursieve proces definities simuleren met behulp van de ! operator in de -calculus?

3) Definieer bisimulatie en geef enkele voorbeelden/tegenvoorbeelden.

28-01-03

1) formuleer en bewijs de stelling van unique handling (hfdst 10 dus)

2) oefening maak een specificatie (sequential process) en een implementatie (concurrent process) van een boolean-stack, en leg in grote lijnen uit hoe je zou bewijzen dat de implementatie aan de specificatie voldoet.

3) wat is sterke simulatie tot op congruentie, wat is de relatie hievan met sterke equivalentie, bewijs deze relatie

24-01-03 VM

1) bespreek waarom taal-equivalentie niet meer werkt voor reactieve systemen..

2) definieer bisimulatie en geef enkele voorbeelden/tegenvoorbeelden

blijkbaar verwacht ie bij uw voorbeelden eentje waarbij A B simuleert, B A simuleert maar er toch geen bisimulatie is. (dat had ik niet)

bijvraag: op welke wiskundige structuur kan je zo'n bisimulatie toepassen ? (niet gewoon LTS ofzo)

3) Geef een mogelijke representatie van binaire bomen in de -calculus. (en een voorbeeldje, en een bijvraag over persistentie, en over rekenen met die bomen met Treecases vb)

18-01-03

(gegeven: een blad met de reactie-regels, de transitie-regels en de structurele congruentie-regels)

1. Formuleer en bewijs de "Unique Solutions of Equations" stelling.

2. Hoe kan je recursieve proces definities simuleren met behulp van de ! operator in de -calculus?

3. Ontwerp een sequentiële procesuitdrukking voor een drankautomaat. Deze aanvaardt stukken van .5EUR, 1EUR, en 2EUR. Water kost 1EUR, limonade 1,5EUR. De automaat moet geld kunnen teruggeven. (Bijvraagje: wat indien je rekening wilt kunnen houden met het beschikbare geld in de automaat?)