Típuselmélet

Az oldal jelenlegi verzióját még nem ellenőrizték tapasztalt közreműködők, és jelentősen eltérhet a 2021. december 6-án felülvizsgált verziótól ; az ellenőrzések 2 szerkesztést igényelnek .

A típuselmélet bármely formális rendszer , amely a naiv halmazelmélet alternatívája, egy ilyen rendszer elemeinek osztályozásával egy bizonyos hierarchiát alkotó típusok segítségével. A típuselmélet alatt az ilyen formalizmusok tanulmányozását is értjük.

A típuselmélet matematikailag formalizált alapja az adattípus-rendszerek tervezésének, elemzésének és tanulmányozásának a programozási nyelvek elméletében ( a számítástechnika része ). Sok programozó használja ezt a kifejezést minden olyan elemző munkára, amely programozási nyelveken vizsgálja a típusrendszereket. Tudományos körökben a típuselméletet leggyakrabban a diszkrét matematika szűkebb ágaként értelmezik , különösen a λ-számítást típusokkal.

A modern típuselmélet részben a Russell-féle paradoxon feloldásának folyamatában alakult ki, és nagyrészt Bertrand Russell és Alfred Whitehead „ Principia mathematica ” [1] munkáján alapul .

Írja be a doktrínát

A típusok doktrínája B. Russell-ig nyúlik vissza, amely szerint bármely típust egy propozíciós (propozíciós) funkció jelentéstartományának tekintenek. Ezenkívül úgy gondolják, hogy minden függvénynek van típusa (tartománya, hatóköre). A típusok doktrínájában tiszteletben tartják annak az elvnek a megvalósíthatóságát, hogy egy típust (propozíciót) egy definíciósan ekvivalens típussal (propozícióval) helyettesítsünk .

Írja be az elméletet a logikába

Ez az elmélet a hierarchia elvén alapul. Ez azt jelenti, hogy a logikai fogalmak – kijelentések , egyedek, propozíciós függvények – típushierarchiában vannak elrendezve. Lényeges, hogy egy tetszőleges függvénynek csak azok a fogalmak legyenek argumentumai, amelyek a hierarchiában megelőzik.

Néhány típuselmélet

Egy bizonyos típusú elméleten általában magasabb rendű alkalmazott logikát értünk, amelyben a természetes számok N típusúak , és amelyben a Peano aritmetika axiómái teljesülnek. .

Elágazó típus elmélet

Történelmileg az első javasolt típuselmélet (1902-től 1913-ig tartó időszak) az elágazó típuselmélet ( RTT ) , amelyet Whitehead és Russell épített fel, és végül a Principia Mathematica című alapvető műben fogalmazták meg . Ez az elmélet azon az elven alapul, hogy korlátozza azon esetek számát, amikor az objektumok egyetlen típushoz tartoznak. Nyolc ilyen esetet kifejezetten deklarálunk, és két típushierarchiát különböztetünk meg: (egyszerűen) „típusok” és „rendek”. Ugyanakkor maga a „típus” jelölés nincs definiálva, és számos egyéb pontatlanság is van, mivel a fő szándék az volt, hogy különböző számú argumentumból vagy különböző típusú argumentumokból egyenlőtlen típusú függvényeket deklaráljanak [2] . Az elmélet szerves része a redukálhatóság axiómája .

Egyszerű típuselmélet

Az 1920-as években Chwistek és Ramsey egy egységes típuselméletet javasolt, amely ma "egyszerű típuselmélet" vagy egyszerű típuselmélet néven ismert, és amely összeomolja a típushierarchiát , kiküszöbölve a redukálhatóság axiómájának szükségességét.

Intuicionista típuselmélet

Az intuicionista típuselméletet ( ITT ) Per Martin-Löf építette fel .

Tiszta típusú rendszerek

A tiszta típusú rendszerek elmélete ( eng.  pure type systems , PTS ) általánosítja az összes lambda-kocka számítást , és olyan szabályokat fogalmaz meg, amelyek lehetővé teszik azok speciális esetként történő kiszámítását. Berardi és Terlouw önállóan építtette . A tiszta típusrendszerek csak a típus fogalmával működnek, a többi kalkulus összes fogalmát csak típusok formájában veszik figyelembe - ezért nevezzük őket " tisztának ". Nincs elválasztás a terminusok és a típusok, a különböző rétegek között (azaz a típusnemzetségeket típusoknak is nevezik, csak egy másik univerzummal kapcsolatosak), sőt magukat a rétegeket is nem fajtáknak , hanem típusoknak (pontosabban típusuniverzumoknak) nevezik. . Általában egy tiszta típusú rendszert egy specifikáció, öt kemény szabály és két rugalmas szabály határozza meg (amelyek rendszerenként változnak). A tiszta típusú rendszer specifikációja egy hármas (S, A, R), ahol a rendezésekS halmaza ( S orts) , az axiómák halmaza ( A xiómák) ezeken a rendezéseken, és a szabályok halmaza ( Rules ). [3] [4] [5]AR

Többdimenziós típuselméletek

A magasabb dimenziós típuselméletek vagy egyszerűen csak a magasabb típusú elméletek ( HTT ) általánosítják a hagyományos típuselméleteket , lehetővé téve a típusok közötti nem triviális ekvivalencia kapcsolatok megállapítását .  Például, ha veszünk egy természetes számpárt ( derékszögű szorzat ) és egy természetes számot visszaadó függvényhalmazt , akkor nem mondhatjuk, hogy ezeknek a halmazoknak az elemei páronként egyenlőek, de azt mondhatjuk, hogy ezek a halmazok egyenértékű. A típusok közötti izomorfizmusokat és tanulmányozzák kétdimenziós, háromdimenziós stb. típuselméletek. Az elméletek megfogalmazásához szükséges teljes alapot Girard-Reynolds fektette le , de magukat az elméleteket sokkal később fogalmazták meg. [6] [7]nat × natnat -> nat

Homotópia típuselmélet

A homotópiatípus-elmélet ( eng. Homotopy  type theory , HoTT ) általánosítja a többdimenziós elméleteket, létrehozva a típusok egyenlőségét a topológiák szintjén . A többdimenziós elméletekben a "típus-ekvivalencia" és a "típus-egyenlőség" fogalmát különbözőnek tekintik. A homotópiaelmélet radikális újítása az univalencia axiómája , amely azt feltételezi, hogy ha a típusok topológiailag egyenértékűek, akkor topológiailag egyenlők.

Gazdaságos típuselmélet

A 2020 - ban megfogalmazott Cost -Aware Type Theory ( CATT ) a  funkcionális típusokat a legegyszerűbb információkkal bővíti ki az algoritmus bonyolultságáról  - az eredmény eléréséhez szükséges számítási lépések számáról -, lehetővé téve a programok szemantikai helyességének ellenőrzését, hanem az előírt követelményeket is. időbeli összetettségi korlátok. [8] Ez a függő függvénytípusok konstruktorán keresztül történik . Az elmélet formalizálásához többek között figyelembe kell venni a leállítási problémát , amelyre a tipizálási szabályok megkövetelik, hogy a rekurzív hívás szigorúan kevésbé legyen összetett, mint az argumentum aktuális értékével rendelkező hívás. A CATT lehetővé teszi a matematikai lépéseket (például rekurzív hívást) magában foglaló "absztrakt költség" és a "gépi költség" közötti bizonyítást, figyelembe véve a fizikailag megvalósított utasítások hatékonyságát (például, hogy az összeg és a szorzat aritmetikai műveletei ugyanannyi időt vesznek igénybe a legtöbb processzoron). ), és vegye figyelembe a párhuzamosságot is . funtime

Lásd még

Jegyzetek

  1. ↑ "A matematika alapjai" - a matematikai logika alapvető háromkötetes könyve (Whitehead, Alfred N. A matematika alapjai: 3 kötetben / A. N. Whitehead, B. Russell; Szerk.: G. P. Yarovoy, Yu. N. Radaev. - Samara : Samara University Publishing House, 2005-2006 - ISBN 5-86465-359-4 )
  2. ↑ Modern Perspective on Type Theory, 2004 , 2b The Ramified Theory of Types RTT, p. 35.
  3. ↑ Barendregt, "Lambda Calculi with Types", 1992 , 5.2. Tiszta típusú rendszer, p. 96-114.
  4. ↑ Modern Perspective on Type Theory, 2004 , 4c Pure Type Systems, p. 116.
  5. ↑ Pierce, 2002 , p. 493.
  6. ↑ Harper, "Higher-Dimensional Type Theory", 2011 .
  7. ↑ Robert Harper Research Papers (hivatkozás nem érhető el) . Letöltve: 2016. október 20. Az eredetiből archiválva : 2016. október 30. 
  8. ↑ Yue Niu, Robert Harper. Költségtudatos típuselmélet. - Carnegie Mellon Egyetem, 2020. - arXiv : 2011.03660v1 .

Irodalom

Linkek

  Ugrás a Wikidata elemre  Szótárak és enciklopédiák