Funktsionaalprogrammeerimine 2025/26 sügis

Kodutöö 8

Selles praktikumis joonistame tüüpimispuid lihtsalt tüübitud {$\lambda$}-arvutuses. Abiks on tüüpimisreeglid lihtsalt tüübitud {$\lambda$}-arvutuse peatükis.

Tüüpimispuud

Etteruttavalt, harjutame väga üldise meetodi väga lihtsat vormi. Tõestame formaalselt, et Churchi stiilis {$\lambda$}-term {$ t $} on mingit konkreetset tüüpi {$ \sigma $}.

Kirjutis {$\Gamma \vdash t : \sigma $} on väide, et term {$t$} on tüüpi {$\sigma$}, kus vabade muutujate tüübid on väärtustega {$\Gamma$}. Püüame selliseid väiteid tõestada, kasutades lihtsalt tüübitud {$\lambda$}-arvutuse reegleid ehk lihtsalt tüübitud {$\lambda$}-arvutuse loogikas.

Järgnevates loengutes näeme, et formaalne tõestamine ongi täpselt tüübipuu ehitamine.

Ülesanded

Joonistage järgnevad tüüpimispuud -- kui võimalik. Mis väärtused tuleb panna lünkadesse? Kui tüüpimispuu on võimatu, kirjeldage põhjust.

1. {$ \vdash \lambda x:\alpha.\, \lambda y:\beta.\, y : ? $}
2. {$ \{a : \alpha\} \vdash (\lambda x:\alpha. x)\, a :\, ? $}
3. {$ \vdash (\lambda x:\alpha. x\,x)\,(\lambda x:\alpha. x\,x) :\, ? $}
4. {$ \vdash (\lambda x:\alpha,\, y:\alpha\to\beta\to\gamma. (\lambda z:\alpha. y)\,x\,x) :\, ? $}
5. {$\vdash (\lambda x:\alpha,\, y:\beta, z:(\beta\to\alpha)\to\beta. z\,(\lambda w:\beta. x)) :\, ? $}
6. {$ \vdash (\lambda x:\beta.\,\lambda y:\alpha\to\beta.\, y\,(\lambda x:\alpha.\, x)) :\, ? $}