System F
![]() | Ten artykuł od 2011-07 wymaga zweryfikowania podanych informacji. Należy podać wiarygodne źródła w formie przypisów bibliograficznych. Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte. Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary) Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu. |
![]() | Ten artykuł dotyczy wariantu rachunku lambda. Zobacz też: Ferry Corsten. |
System F – jeden z wariantów rachunku lambda z typami. Jest to najprostszy rachunek zawierający typy proste oraz typy polimorficzne.
Zbiór typów można zdefiniować jako najmniejszy taki zbiór U, że przy danym, ustalonym i przeliczalnym zbiorze zmiennych V, zachodzą następujące własności:
- V zawiera się w U,
- jeśli oraz należą do U, to również należy do U,
- jeśli jest zmienną (należy do V) oraz należy do U, to również należy do U.
Typy postaci należy traktować (nieformalnie) jako każdą możliwą instancję typu taką, że za każde wystąpienie zmiennej wstawiamy dowolny inny typ (za każde wystąpienie zmiennej ten sam).