Leertaak 8

Getypeerde lambda-calculus (vervolg)

Achtergrond

Typering in de simpel-getypeerde (eerste-orde) lambda-calculus voldoet aan een aantal natuurlijke eigenschappen, zoals typeerbaarheid van alle subtermen van elke typeerbare term. Verder blijven types behouden tijdens reductie (maar niet noodzakelijkerwijs bij expansie) van termen.

Alle typeerbare termen zijn sterk normaliserend. Deze eigenschap impliceert dat niet alle berekenbare functies definieerbaar zijn door een typeerbare term.

Leerdoel

Na het voltooien van deze taak kunt u

• onderstaande kernbegrippen (zie 'Werkwijze') verklaren;
• de subtermeigenschap, substitutie-eigenschap, subject-reductie-eigenschap en sterke-normalisatie-eigenschap van het typeringssysteem uitleggen;
• deze eigenschappen gebruiken in redeneringen, bijvoorbeeld over typeerbaarheid van termen;
• typeerbaarheid van lambdatermen onderzoeken en zo mogelijk een type bepalen;
• bewoners van gegeven eerste-orde types construeren.

Instructie

1. Lees p. 36-38 in Barendregt & Barendsen. Lees p. 9-11 in het dictaat over typetheorie (bij het SN-bewijs gaat het om het bewijsidee, niet de details). Kernbegrippen:
   • generatielemma, typeerbaarheid van subtermen,
   • substitutie-eigenschap, subject reductie,
   • sterke normalisatie
2. Construeer (indien mogelijk) types voor de termen in opgave 5.3 (van B&B).
3. Beantwoord opgave 35 (van de opgavenbundel).
4. Construeer bewoners bij de types in opgave 32 (ii) en 5.4. (ii).
5. Laat zien dat geen enkele dekpuntcombinator (een gesloten term D met de eigenschap Df = f(Df), bijvoorbeeld Y) typeerbaar is in de eerste-orde lambda-calculus.

Product

• Beoordeling van de typeerbaarheid van de gegeven termen.
• Bewoners van de gegeven types.
• Een redenering die aantoont dat dekpuntcombinatoren niet typeerbaar zijn.

Reflectie

• Verantwoordt u de typeerbaarheidsuitspraken met een typetoewijzing resp. redenering over non-typeerbaarheid?
• Verwijst u bij redeneringen over (non-)typeerbaarheid naar de afleidingsregels en/of de theoretische eigenschappen van het typeringssysteem?