Leertaak 5
Berekeningen in de lambda-calculus
Achtergrond
De lambda-calculus is een tweede berekeningsmodel dat gebaseerd
is op herschrijven. Lambda-calculus is zeer eenvoudig: de taal bevat alleen
applicatie en abstractie (en bijvoorbeeld geen pattern-matching, functienamen
en directe recursie). Bovendien is er slechts één, universele,
herschrijfregel. Lambda-calculus is bij uitstek geschikt om berekeningen in
functionele talen in de meest pure vorm te analyseren.
Leerdoel
Na het voltooien van deze taak kunt u
- onderstaande kernbegrippen (zie 'Instructie') verklaren;
- bèta-reducties uitvoeren;
- het bèta-reductiegedrag van lambda-termen analyseren door de reductiegraaf
te tekenen;
- voor eenvoudige (niet-recursieve) specificaties een lambda-term vinden die
eraan voldoet.
Instructie
- Lees Barendregt & Barendsen, p. 5-10, p. 12 (alleen Example 2.10), p.
23. Kernbegrippen:
- applicatie, abstractie, lambda-term
- currying
- vrije variabelen, gesloten term, combinator
- standaardcombinatoren
- bèta-reductie
- Beantwoord opgave 1 van de opgavenbundel
(vat de gelijkheden op als meerstaps reducties).
- Bepaal de normaalvorm van de termen SKIKISS en
S(SK)I.
- Teken de reductiegraaf van de term in opgave 16.
- Bepaal lambda-termen bij de reductiegrafen in opgave 10 (i) en (ii).
Product
- Bèta-reductiepaden bij de gegeven conversies.
- Normaalvormen en bijbehorende reductiepaden.
- Reductiegrafen bij de gegeven termen.
- Lambda-termen die de gegeven reductiegrafen hebben.
Reflectie
- Houdt u zich aan de notationele afspraken zoals de haakjesconventie?
- Is het bij elke stap duidelijk welke redex erbij betrokken is?
- Is uw graaf een echte reductiegraaf? Bijvoorbeeld: Komt het aantal uitgaande
pijlen per knoop overeen met het aantal redexen in de betreffende term? Zijn
de termen bij de knopen onderling syntactisch verschillend?