Leertaak 6
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
- Lees p. 24, p. 12 (lees 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
- Construeer oplossingen van de specificatie in opgave 3 (iii)
van de opgavenbundel.
- Beantwoord opgave 37 (i)-(ii).
- Beantwoord opgave 27 (de termen true en false
zijn K respectievelijk K*).
- 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?