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

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.