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

• onderstaande kernbegrippen (zie 'Werkwijze') verklaren;
• bij gegeven lambda-termen een type construeren in de simpel-getypeerde lambda-calculus;
• deze typetoewijzing staven met een afleiding;
• in voorkomende gevallen aantonen dat een term niet typeerbaar is;
• bij een gegeven type een bewoner construeren.

Instructie

1. Lees p. 33-36 en de twee extra bladzijden over "vlaggenafleidingen". Kernbegrippen:
   • impliciete en expliciete typering, Curry- versus Church-typering;
   • typevariabelen, types
   • typeringsuitspraak, typeafleiding
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

• Drie typetoewijzingen aan lambda-termen.
• Een redenering die aantoont dat de gegeven termen niet typeerbaar zijn.
• Een bewoner van het gegeven type.

Reflectie

• Staaft u elke typeringsuitspraak met een afleiding?
• Verwijst u bij redeneringen over (non-)typeerbaarheid naar de afleidingsregels?