Leertaak 7

Getypeerde lambda-calculus

Achtergrond

Met typering in programmeertalen kunnen we voorkomen dat een programmeur bewerkingen toepast op argumenten waarvoor de betreffende operatie niet bedoeld is. Uit de typespecificatie van de optelling kan bijvoorbeeld afgeleid worden dat er geen string bij een integer kan worden opgeteld. Naast deze controle op 'locale consistentie' hebben typeringssystemen soms nog andere toepassingen, bijvoorbeeld het detecteren van optimalisatiemogelijkheden.

We kunnen op verschillende manieren typering toevoegen aan de lambda-calculus: door types toe te wijzen aan ongetypeerde termen, of door type-informatie op te nemen in de syntax van termen.

De uitspraak "term M heeft type A" kunnen we in computationele zin opvatten als "M is een programma en A is zijn type", maar ook in logische zin, namelijk als "M is een bewijs van propositie A".

Leerdoel

Na het voltooien van deze taak kunt u

Instructie

  1. Lees p. 33-36. Kernbegrippen:
  2. Construeer een type voor de term lambda xy.x(yx).
  3. Beantwoord opgave 5.1 (i)-(ii).
  4. Beantwoord opgave 5.2. (We hebben op het college een begin gemaakt.)
  5. Beantwoord opgave 5.4 (i).

Product

Reflectie