Teorie typů

Technology
12 hours ago
8
4
2
Avatar
Author
Albert Flores

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

5 min read
Share this post:
Like it 8

Leave a Comment

Please, enter your name.
Please, provide a valid email address.
Please, enter your comment.
Enjoy this post? Join Cesko.wiki
Don’t forget to share it
Top