Funktsionaalprogrammeerimine 2024/25 sügis

Kodutöö 9

Selles praktikumis joonistame tüüpimispuid lihtsalt tüübitud $\lambda$-arvutuses. Abiks on tüüpimisreeglid lihtsalt tüübitud $\lambda$-arvutuse konspektis.

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,

1. mida teha siis, kui kogu info pole antud (Curry stiilis termide tüüpide tuletamine), ja et
2. tüüpimispuu ehitamine on tõestamine ning
3. 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)) :\, ?$