Leertaak 7

Representatie en normalisatie in de lambda-calculus

Achtergrond

Om de rekenkracht van de lambda-calculus te onderzoeken, construeren we representaties van verschillende datatypes: booleans, paren (tuples) en natuurlijke getallen. Naast recursie (met de dekpuntcombinator) blijkt ook pattern matching te vertalen naar lambda-calculus. Hiermee zijn alle berekenbare functies representeerbaar in de lambda-calculus, hetgeen dit berekeningsmodel even krachtig maakt als zijn imperatieve tegenhanger, de Turingmachine.

De reductiegraaf van een term kan zeer complex zijn, en evaluatie van een functioneel programma via het systematisch doorzoeken van alle reductiemogelijkheden daarmee ondoenlijk. Zogenaamde reductiestrategieën geven specifieke paden in de reductiegraaf aan. Zo'n strategie is bruikbaar voor berekeningen indien de normaalvorm (zo die er is) van elke term zich op het betreffende pad bevindt.

Leerdoel

Na het voltooien van deze taak kunt u

• onderstaande kernbegrippen (zie 'Werkwijze') verklaren;
• voor berekenbare numerieke functies een lambda-definiërende term construeren;
• de rol van reductiestrategieën voor normalisatie (bijvoorbeeld t.b.v. implementaties van functionele talen) uitleggen; de inherente tegenstelling tussen 'veilig' (normaliserend) en 'efficiënt' verklaren;
• voor gegeven termen de normaalvorm bepalen, dan wel aantonen dat die niet bestaat;
• eenvoudige specificaties in termen van normalisatiegedrag realiseren.

Instructie

1. Lees p. 17-20, p. 30. Kernbegrippen:
   • representatie van booleans, paren/tuples
   • numeral
   • lambda-definieerbaarheid
   • reductiestrategie, leftmost-reductie
   • normalisatiestelling
2. Construeer een lambda-definiërende term voor de functies in opgave 5 van de opgavenbundel.
3. Laat zien dat de term in opgave 22 van de opgavenbundel geen normaalvorm heeft.
4. Beantwoord opgave 13.
5. Beantwoord opgave 17.

Product

• Lambda-definiërende termen voor de betreffende functies.
• Redeneringen die de niet-normaliseerbaarheid van de gegeven termen aantonen.
• Lambda-termen met het betreffende normalisatiegedrag; een redenering waarom uw oplossing correct is.

Evaluatie

• Is het duidelijk hoe u aan de definiërende lambda-termen gekomen bent? Indien u de dekpuntcombinator gebruikt: heeft u de functiespecificatie naar een equivalente recursieve specificatie vertaald?
• Is de redenering over het normalisatiegedrag helder en compact? Ingeval u een beroep doet op de normalisatiestelling: is het voor de lezer evident dat het aangegeven leftmost-reductiepad oneindig is?