Nie jesteś zalogowany | zaloguj się

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Aktualności — Wydarzenia

SLIWOWICA

 

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


Prelegent: Aleksy Schubert

2023-06-02 12:15

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.