Leertaak 5

Reductie en recursie in de lambda-calculus

Achtergrond

Voor het nabootsen van recursie in de lambda-calculus gebruiken we een speciale dekpunteigenschap. Via een truc waarin zelfapplicatie essentieel is, kunnen we een combinator construeren waarmee we directe recursies kunnen oplossen.

De lambda-calculus is confluent. Net zoals in de TRS-wereld komt deze Church-Rosser-eigenschap van pas bij redeneringen over reductie-, conversie- en normalisatievragen.

Leerdoel

Na het voltooien van deze taak kunt u

• onderstaande kernbegrippen (zie 'Instructie') verklaren;
• voor direct-recursieve equationele specificaties een lambda-term construeren die eraan voldoet;
• de stelling van Church-Rosser (en directe gevolgen) gebruiken om (on)gelijkheid van lambda-termen aan te tonen.

Instructie

1. Lees p. 24, p. 12 (lees eventueel de gelijkheid als bèta-gelijkheid), p. 25-26 en bekijk het 'diagrammenbewijs' van de Church-Rosser stelling op p. 27-29. Kernbegrippen:
   • bèta-conversie (bèta-gelijkheid)
   • dekpunt, dekpuntcombinator
   • Church-Rosser
2. Construeer oplossingen van de specificatie in opgave 3 (iii) van de opgavenbundel.
3. Beantwoord opgave 37 (i)-(ii).
4. Beantwoord opgave 27 (de termen true en false zijn K respectievelijk K*).
5. Beantwoord opgave 31.

Product

• Oplossingen van de recursieve specificatie.
• Een normalisatie van de term.
• Een redenering die aantoont dat de term geen normaalvorm heeft.
• Een redenering die aantoont dat de betreffende specificatie onoplosbaar is.
• Een redenering die aantoont dat de term een dekpuntcombinator is.

Reflectie

• Voldoet de lambda-term aan de specificatie? Is dat eenvoudig in te zien?
• Zijn uw redeneringen helder? Verwijst u adequaat naar de gebruikte theoretische resultaten? Is het voor een lezer duidelijk dat deze resultaten van toepassing zijn?
• Is uw betoog over de non-realiseerbaarheid to the point, dat wil zeggen: bevat het een concreet tegenvoorbeeld?