Leertaak 4

Berekeningen in de lambda-calculus

Achtergrond

De lambda-calculus is een berekeningsmodel dat gebaseerd is op herschrijven, net als de termherschrijfsystemen die we hebben gezien in de cursus Semantiek en Logica 1. Lambda-calculus is zeer eenvoudig: de taal bevat alleen applicatie en abstractie (en bijvoorbeeld geen pattern-matching, functienamen en directe recursie). Bovendien er is 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

1. Lees Barendregt & Barendsen, p. 5-11 tot Remark 2.8, p. 12 (alleen Example 2.10), p. 23-24 tot en met Example 4.3. Kernbegrippen:
   • applicatie, abstractie, lambda-term
   • currying
   • vrije variabelen, gesloten term, combinator
   • standaardcombinatoren
   • gelijkheid
   • bèta-reductie
2. Beantwoord opgave 1 van de opgavenbundel.
3. Bepaal de normaalvorm van de termen SKIKISS en S(SK)I.
4. Teken de reductiegraaf van de term in opgave 16.
5. Bepaal lambda-termen bij de reductiegrafen in opgave 10 (i) en (ii). (NB Antwoord bij (ii): (\yx.y (\z.zz))(\v.vv) I

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?