Tekst źródłowy strony System F

{{Dopracować|źródła=2011-07}}
{{inne znaczenia|wariantu [[Rachunek lambda|rachunku lambda]]|[[Ferry Corsten]]}}
'''System F''' – jeden z wariantów [[Rachunek lambda|rachunku lambda]] z [[Rachunek lambda z typami|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 [[Zbiór przeliczalny|przeliczalnym]] zbiorze [[Zmienna (matematyka)|zmiennych]] ''V'', zachodzą następujące własności:
* ''V'' zawiera się w ''U'',
* jeśli <math>\sigma</math> oraz <math>\tau</math> należą do ''U'', to <math>\sigma\to\tau</math> również należy do ''U'',
* jeśli <math>\alpha</math> jest zmienną (należy do ''V'') oraz <math>\sigma</math> należy do ''U'', to <math>\forall\alpha.\ \sigma</math> również należy do ''U''.

Typy postaci <math>\forall\alpha.\ \sigma</math> należy traktować (nieformalnie) jako każdą możliwą [[Instancja|instancję]] typu <math>\sigma</math> taką, że za każde wystąpienie zmiennej <math>\alpha</math> wstawiamy dowolny inny typ (za każde wystąpienie zmiennej ten sam).

[[Kategoria:Rachunek lambda]]