Teorie typů

Teorie typů je teorie na pomezí matematiky, filosofie a algoritmiky, kterou jako první předložil Bertrand Russell za účelem vyřešení paradoxů teorie množin, ačkoliv zárodky lze najít již u Bernarda Bolzana. Nejjednodušším příkladem použití je typovaný lambda kalkul.

V teorie typů existuje univerzum typů a jejich hodnot, přičemž každá proměnná má určený typ, například ve formuli \lambda x:\mathbb{N}.x+1.

Teorie typů hraje důležitou roli v Henkinově důkazu faktu, že každá bezesporná teorie vyššího řádu má obecný model. Hintikka o několik let později dokázal, že každá teorie libovolně velkého konečného řádu je sémanticky ekvivalentní odpovídající reifikované teorii druhého řádu, tedy přechodem na vyšší řád nezískáme silnější logický systém.

Existují různá rozšíření původní Russellovy teorie typů, například obsahující závislostní typy.

Algebraické datové typy tvoří algebru, která je polookruhem.

Externí odkazy