Teorie typů

Aktuální verze stránky ještě nebyla zkontrolována zkušenými přispěvateli a může se výrazně lišit od verze recenzované 6. prosince 2021; kontroly vyžadují 2 úpravy .

Teorie typů je jakýkoli formální systém , který je alternativou k naivní teorii množin , doprovázený klasifikací prvků takového systému pomocí typů, které tvoří určitou hierarchii. Teorie typů je také chápána jako studium takových formalismů.

Teorie typů je matematicky formalizovaný základ pro navrhování, analýzu a studium systémů datových typů v teorii programovacích jazyků (sekce informatiky ). Mnoho programátorů používá tento termín k označení jakékoli analytické práce, která studuje typové systémy v programovacích jazycích. Ve vědeckých kruzích je teorie typů nejčastěji chápána jako užší odvětví diskrétní matematiky , zejména λ-počet s typy.

Moderní teorie typu byla zčásti vyvinuta v procesu řešení Russellova paradoxu a je z velké části založena na práci Bertranda Russella a Alfreda Whiteheada „ Principia mathematica “ [1] .

Type Doctrine

Nauka o typech sahá až k B. Russellovi, podle kterého je jakýkoli typ považován za rozsah významnosti výrokové (výrokové) funkce. Kromě toho se má za to, že každá funkce má svůj typ (svou doménu, rozsah). V doktríně typů je respektována proveditelnost principu nahrazení typu (propozice) definičně ekvivalentním typem (propozice) .

Teorie typů v logice

Tato teorie je založena na principu hierarchie. To znamená, že logické pojmy – výroky , individua, výrokové funkce – jsou uspořádány v hierarchii typů. Podstatné je, že libovolná funkce má jako své argumenty pouze ty pojmy, které jí v hierarchii předcházejí.

Nějaká teorie typů

Určitá teorie typů je obvykle chápána jako aplikovaná logika vyšších řádů, ve které existuje typ N přirozených čísel a ve které jsou splněny axiomy Peanovy aritmetiky . .

Teorie rozvětvených typů

Historicky první navrhovanou teorií typů (období od roku 1902 do roku 1913) je rozvětvená teorie typů ( RTT ) , postavená Whiteheadem a Russellem a nakonec formulovaná v základní práci Principia Mathematica . Tato teorie je založena na principu omezení počtu případů, kdy objekty patří k jednomu typu. Osm takových případů je explicitně deklarováno a rozlišují se dvě hierarchie typů: (prostě) "typy" a "objednávky". Přitom samotný zápis „typu“ není definován a existuje řada dalších nepřesností, neboť hlavním záměrem bylo deklarovat nestejné typy funkcí z různého počtu argumentů nebo z argumentů různých typů [2] . Nedílnou součástí teorie je axiom redukovatelnosti .

Jednoduchá teorie typů

Ve dvacátých letech minulého století Chwistek a Ramsey navrhli nerozvětvenou teorii typu, nyní známou jako „Simple Type Theory“ nebo Simple Type Theory , která hroutí hierarchii typů, čímž eliminuje potřebu axiomu redukovatelnosti.

Intuicionistická teorie typů

Intuicionistic Type Theory ( ITT ) vytvořil Per Martin-Löf .

Systémy čistého typu

Teorie systémů čistého typu ( eng.  pure type systems , PTS ) zobecňuje všechny výpočty lambda-krychle a formuluje pravidla, která umožňují jejich výpočet jako speciální případy. To bylo nezávisle postaveno Berardi a Terlouw . Systémy čistého typu pracují pouze s konceptem typu, přičemž všechny koncepty ostatních kalkulů uvažují pouze ve formě typů - proto se nazývají " čisté ". Neexistuje žádné oddělení mezi pojmy a typy, mezi různými vrstvami (tj . rody typů se také nazývají typy, pouze související s jiným vesmírem), a dokonce i vrstvy samotné se nazývají nikoli variety , ale typy (přesněji vesmíry typů) . Obecně je systém čistého typu definován pojmem specifikace, pěti pevných pravidel a dvou flexibilních pravidel (která se liší systém od systému). Specifikace čistého typového systému je trojitá (S, A, R), kde jeS množina druhů ( S orts), Aje množina axiomů ( A xiomy) nad těmito druhy a Rje množina pravidel ( Pravidla ). [3] [4] [5]

Vícerozměrné teorie typů

Vyšší - dimenzionální typové teorie nebo jednoduše vyšší typové teorie ( HTT ) zobecňují tradiční typové teorie , dovolovat netriviální vztahy rovnocennosti mezi typy být založen .  Vezmeme-li například množinu dvojic ( karteziánských součinů ) přirozených čísel a množinu funkcí, které vracejí přirozené číslo , pak nelze říci, že prvky těchto množin jsou párově stejné, ale lze říci, že tyto množiny jsou ekvivalent. Izomorfismy mezi typy a jsou studovány ve dvourozměrném, trojrozměrném atd. teorie typu. Celý nezbytný základ pro formulaci těchto teorií položil Girard-Reynolds , ale samotné teorie byly formulovány mnohem později. [6] [7]nat × natnat -> nat

Teorie homotopických typů

Teorie homotopických typů ( angl. Homotopy  type theory , HoTT ) zobecňuje multidimenzionální teorie a zakládá rovnost typů na úrovni topologií . V multidimenzionálních teoriích jsou koncepty „typové ekvivalence“ a „typové rovnosti“ považovány za odlišné. Radikální inovace teorie homotopie je axiom univalence , postulovat to jestliže typy jsou topologically ekvivalentní, pak oni jsou topologically se rovnat.

Teorie ekonomických typů

Cost -Aware Type Theory ( CATT )  , formulovaná v roce 2020 , rozšiřuje funkční typy o nejjednodušší informace o algoritmické složitosti  – počtu výpočetních kroků potřebných k získání výsledku – což vám umožňuje ověřit programy nejen z hlediska sémantické správnosti, ale také z hlediska vynucených omezení časové složitosti. [8] To se provádí pomocí konstruktoru typů závislých funkcí . Formalizace teorie vyžaduje mimo jiné zohlednění problému zastavení , pro který pravidla psaní vyžadují, aby rekurzivní volání bylo přísně méně složité než volání s aktuální hodnotou argumentu. CATT umožňuje rozlišovat mezi „abstraktními náklady“ zahrnujícími matematické kroky (jako je rekurzivní volání) a „náklady na stroj“ s přihlédnutím k účinnosti fyzicky implementovaných instrukcí (například, že aritmetické operace součtu a součinu trvají stejnou dobu na většině procesorů). ), a také vzít v úvahu paralelismus . funtime

Viz také

Poznámky

  1. ↑ „Základy matematiky“ – základní třídílná kniha matematické logiky (Whitehead, Alfred N. Základy matematiky: Ve 3 dílech / A. N. Whitehead, B. Russell; Edited by G. P. Yarovoy, Yu. N. Radaev. – Samara : Samara University Publishing House, 2005-2006 - ISBN 5-86465-359-4 )
  2. ↑ Moderní pohled na teorii typů, 2004 , 2b The Ramified Theory of Types RTT, str. 35.
  3. ↑ Barendregt, "Lambda Calculi s typy", 1992 , 5.2. Systém čistého typu, str. 96-114.
  4. ↑ Moderní pohled na teorii typů, 2004 , 4c Systémy čistého typu, str. 116.
  5. ↑ Pierce, 2002 , str. 493.
  6. ↑ Harper, "Higher-Dimensional Type Theory", 2011 .
  7. ↑ Robert Harper Research Papers (odkaz není k dispozici) . Získáno 20. října 2016. Archivováno z originálu 30. října 2016. 
  8. ↑ Yue Niu, Robert Harper. Cost-Aware Type Theory. - Carnegie Mellon University, 2020. - arXiv : 2011.03660v1 .

Literatura

Odkazy

  Přejděte na položku Wikidata  Slovníky a encyklopedie