Kodutöö 10
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,
- mida teha siis, kui kogu info pole antud (Curry stiilis termide tüüpide tuletamine), ja et
- tüüpimispuu ehitamine on tõestamine ning
- 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.
- {$ \vdash \lambda x:\alpha.\, \lambda y:\beta.\, y : ? $}
- {$ \{a : \alpha\} \vdash (\lambda x:\alpha. x)\, a :\, ? $}
- {$ \vdash (\lambda x:\alpha. x\,x)\,(\lambda x:\alpha. x\,x) :\, ? $}
- {$ \vdash (\lambda x:\alpha,\, y:\alpha\to\beta\to\gamma. (\lambda z:\alpha. y)\,x\,x) :\, ? $}
- {$\vdash (\lambda x:\alpha,\, y:\beta, z:(\beta\to\alpha)\to\beta. z\,(\lambda w:\beta. x)) :\, ? $}
- {$ \vdash (\lambda x:\beta.\,\lambda y:\alpha\to\beta.\, y\,(\lambda x:\alpha.\, x)) :\, ? $}