Typeteori

Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 6. december 2021; checks kræver 2 redigeringer .

Typeteori er ethvert formelt system , som er et alternativ til naiv mængdeteori , ledsaget af en klassificering af elementerne i et sådant system ved hjælp af typer, der danner et bestemt hierarki. Typeteori forstås også som studiet af sådanne formalismer.

Typeteori er et matematisk formaliseret grundlag for at designe, analysere og studere datatypesystemer i teorien om programmeringssprog (sektion af datalogi ). Mange programmører bruger dette udtryk til at henvise til ethvert analytisk arbejde, der studerer typesystemer i programmeringssprog. I videnskabelige kredse forstås typeteori oftest som en snævrere gren af ​​diskret matematik , især λ-regning med typer.

Moderne typeteori blev delvist udviklet i processen med at løse Russells paradoks og er i vid udstrækning baseret på Bertrand Russells og Alfred Whiteheads arbejde " Principia mathematica " [1] .

Skriv Doktrin

Læren om typer går tilbage til B. Russell, ifølge hvilken enhver type betragtes som en række af betydning for en propositionel (propositionel) funktion. Derudover menes det, at hver funktion har en type (dets domæne, omfang). I doktrinen om typer respekteres gennemførligheden af ​​princippet om at erstatte en type (proposition) med en definitionsmæssigt ækvivalent type (proposition) .

Indtast teori i logik

Denne teori er baseret på princippet om hierarki. Det betyder, at logiske begreber - udsagn , individer, propositionelle funktioner - er arrangeret i et hierarki af typer. Det er væsentligt, at en vilkårlig funktion kun har de begreber, der går forud for den i hierarkiet som sine argumenter.

Noget typeteori

En bestemt typeteori forstås sædvanligvis som anvendt logik af højere orden, hvor der er en type N af naturlige tal, og hvor aksiomerne for Peano- aritmetikken er opfyldt .

Forgrenet typeteori

Historisk set er den første foreslåede teori om typer (perioden fra 1902 til 1913) Ramified Theory of Types ( RTT ) , bygget af Whitehead og Russell, og endelig formuleret i det grundlæggende værk Principia Mathematica . Denne teori er baseret på princippet om at begrænse antallet af tilfælde, hvor objekter tilhører en enkelt type. Otte sådanne tilfælde er eksplicit erklæret, og der skelnes mellem to typehierarkier: (simpelthen) "typer" og "ordrer". Samtidig er selve "type"-notationen ikke defineret, og der er en række andre unøjagtigheder, da hovedhensigten var at erklære ulige typer af funktioner fra et forskelligt antal argumenter eller fra argumenter af forskellige typer [2] . En integreret del af teorien er aksiomet for reduktion .

Simple type theory

I 1920'erne foreslog Chwistek og Ramsey en uforgrenet typeteori, nu kendt som "Simple Type Theory" eller Simple Type Theory , som kollapser typehierarkiet og eliminerer behovet for aksiomet om reduktion.

Intuitionistisk typeteori

Intuitionistisk Typeteori ( ITT ) blev bygget af Per Martin-Löf .

Rene type systemer

Teorien om rene typesystemer ( eng.  pure type systems , PTS ) generaliserer alle lambda- terningberegninger og formulerer regler, der tillader, at de kan beregnes som særlige tilfælde. Det blev bygget uafhængigt af Berardi og Terlouw . Rene type systemer fungerer kun med begrebet en type, idet man kun betragter alle andre kalkstens begreber i form af typer - det er derfor, de kaldes " rene ". Der er ingen adskillelse mellem termer og typer, mellem forskellige lag (dvs. slægter af typer kaldes også typer, kun relateret til et andet univers), og selv lagene kaldes ikke varieteter , men typer (mere præcist, universer af typer) . Generelt er et system af ren type defineret af begrebet en specifikation, fem hårde regler og to fleksible (som varierer fra system til system). Specifikationen af ​​et ren type system er en tredobbelt (S, A, R), hvor er mængden af ​​sorter ( Sorts), er Ssættet af aksiomer ( A xiomer ) over disse sorter, og er sættet af regler ( Regler ). [3] [4] [5]AR

Multidimensionelle typeteorier

Højere -dimensionelle typeteorier eller simpelthen højere typeteorier ( HTT ) generaliserer traditionelle typeteorier , hvilket gør det muligt at etablere ikke-trivielle ækvivalensforhold mellem typer .  For eksempel, hvis man tager et sæt par ( kartesiske produkter ) af naturlige tal og et sæt funktioner, der returnerer et naturligt tal , så kan man ikke sige, at elementerne i disse mængder er parvis ens, men man kan sige, at disse mængder er tilsvarende. Isomorfismer mellem typer og studeres i todimensionelle, tredimensionelle osv. type teorier. Hele det nødvendige grundlag for formuleringen af ​​disse teorier blev lagt af Girard-Reynolds , men selve teorierne blev formuleret meget senere. [6] [7]nat × natnat -> nat

Homotopi type teori

Homotopi type teori ( eng. Homotopy  type theory , HoTT ) generaliserer multidimensionelle teorier og etablerer lighed mellem typer på topologiniveau . I multidimensionelle teorier betragtes begreberne "typeækvivalens" og "typelighed" som forskellige. En radikal nyskabelse af homotopi-teorien er univalensaksiomet , der postulerer, at hvis typer er topologisk ækvivalente, så er de topologisk ens.

Økonomisk typeteori

Cost -Aware Type Theory ( CATT )  , formuleret i 2020 , udvider funktionelle typer med den enkleste information om algoritmisk kompleksitet  - antallet af beregningstrin, der kræves for at opnå et resultat - hvilket giver dig mulighed for at verificere programmer ikke kun for semantisk korrekthed, men også for pålagt tidskompleksitetsbegrænsninger. [8] Dette gøres gennem konstruktøren af ​​afhængige funktionstyper . Formaliseringen af ​​teorien kræver blandt andet, at der tages højde for standsningsproblemet , for hvilket indtastningsreglerne kræver, at det rekursive kald er strengt taget mindre komplekst end kaldet med den aktuelle værdi af argumentet. CATT gør det muligt at skelne et bevis mellem "abstrakte omkostninger", der involverer matematiske trin (såsom et rekursivt opkald) og "maskinomkostninger" under hensyntagen til effektiviteten af ​​fysisk implementerede instruktioner (f.eks. at sum- og produktaritmetiske operationer tager samme tid på de fleste processorer). ), og tager også højde for parallelitet . funtime

Se også

Noter

  1. ↑ "Foundations of Mathematics" - en grundlæggende tre-binds bog om matematisk logik (Whitehead, Alfred N. Foundations of Mathematics: In 3 volumes / A. N. Whitehead, B. Russell; Redigeret af 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, s. 35.
  3. ↑ Barendregt, "Lambda Calculi with Types", 1992 , 5.2. Ren type system, s. 96-114.
  4. ↑ Modern Perspective on Type Theory, 2004 , 4c Pure Type Systems, s. 116.
  5. ↑ Pierce, 2002 , s. 493.
  6. ↑ Harper, "Higher-Dimensional Type Theory", 2011 .
  7. ↑ Robert Harper Research Papers (link ikke tilgængeligt) . Hentet 20. oktober 2016. Arkiveret fra originalen 30. oktober 2016. 
  8. ↑ Yue Niu, Robert Harper. Omkostningsbevidst typeteori. - Carnegie Mellon University, 2020. - arXiv : 2011.03660v1 .

Litteratur

Links

  Gå til Wikidata-elementet  Ordbøger og encyklopædier