O nierozstrzygalności wyprowadzania typów przy ograniczonej randze lub arności

Speaker(s)

Aleksy Schubert

Affiliation

MIM

Date

June 2, 2023, 12:15 p.m.

Room

room 5820

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

W modelowaniu języków funkcyjnych z polimorfizmem ważną rolę odgrywa System F Girarda i Reynoldsa. Wiadomo, że dla termów w stylu Curry'ego, jeśli system nie jest w żaden sposób ograniczony, to wyprowadzanie typów jest nierozstrzygalne już dla typów rangi 3. Jednak istniejący dowód ma tę cechę, że w wyporwadzeniu mogą pojawić się typy dowolnej rangi. W trakcie referatu pokażę, że problem ten pozostaje nierozstrzygalny, jeśli nałoży się dodatkowe ograniczenie na wyprowadzenia, że typy w nich się pojawiające nie mogą być dowolnej rangi i dopuści się pewne niewielkie adnotacje typowe w termach. Ta sama konstrukcja działa, jeśli wprowadzi się analogiczne ograniczenie na arność typów.

---