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

Prelegent(ci)

Aleksy Schubert

Afiliacja

MIM

Termin

2 czerwca 2023 12:15

Pokój

p. 5820

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

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.

---