En matemàtiques i informàtica teòrica, una teoria de tipus és la presentació formal d'un sistema de tipus específic. La teoria de tipus és l'estudi acadèmic dels sistemes de tipus.

Algunes teories de tipus serveixen com a alternatives a la teoria de conjunts com a fonament de les matemàtiques. Dues teories de tipus influents que s'han proposat com a fonaments són:

λ-càlcul tipificat d'Alonzo Church Teoria de tipus intuïcionista de Per Martin-Löf

La majoria dels sistemes informatitzats de redacció de proves utilitzen una teoria de tipus com a fonament. Una d'elles és el Càlcul de Construccions Inductives de Thierry Coquand.

Història La teoria de tipus es va crear per evitar paradoxes en la teoria de conjunts ingènua i la lògica formal, com ara la paradoxa de Russell que demostra que, sense axiomes propis, és possible definir el conjunt de tots els conjunts que no són membres d'ells mateixos; aquest conjunt es conté a si mateix i no es conté a si mateix. Entre 1902 i 1908, Bertrand Russell va proposar diverses solucions a aquest problema.

El 1908, Russell va arribar a una teoria ramificada dels tipus juntament amb un axioma de reducibilitat, ambdós apareguts a l' obra Principia Mathematica de Whitehead i Russell, publicada el 1910, 1912 i 1913. Aquest sistema evitava les contradiccions suggerides a la paradoxa de Russell creant una jerarquia de tipus i després assignant cada entitat matemàtica concreta a un tipus específic. Les entitats d'un tipus determinat es construïen exclusivament a partir de subtipus d'aquest tipus, impedint així que una entitat es definís utilitzant-se a si mateixa. Aquesta resolució de la paradoxa de Russell és similar als enfocaments adoptats en altres sistemes formals, com ara la teoria de conjunts de Zermelo-Fraenkel.

La teoria de tipus és particularment popular juntament amb el càlcul lambda d'Alonzo Church. Un exemple notable de teoria de tipus és el càlcul lambda simplement tipificat de Church. La teoria de tipus de Church va ajudar el sistema formal a evitar la paradoxa de Kleene-Rosser que afectava el càlcul lambda original no tipificat. Church va demostrar que podia servir com a fonament de les matemàtiques i es va anomenar lògica d'ordre superior.

En la literatura moderna, la "teoria de tipus" es refereix a un sistema tipificat basat en el càlcul lambda. Un sistema influent és la teoria de tipus intuïcionista de Per Martin-Löf, que es va proposar com a fonament de les matemàtiques constructives. Un altre és el càlcul de construccions de Thierry Coquand, que és utilitzat com a fonament per Rocq (anteriorment conegut com a Coq ), Lean i altres assistents de prova per ordinador. La teoria de tipus és una àrea activa de recerca, una de les quals és el desenvolupament de la teoria de tipus d'homotopia.

Aplicacions Fonaments matemàtics El primer assistent de prova per ordinador, anomenat Automath, utilitzava la teoria de tipus per codificar les matemàtiques en un ordinador. Martin-Löf va desenvolupar específicament la teoria de tipus intuïcionista per codificar totes les matemàtiques i servir com a nova base per a les matemàtiques. Hi ha una investigació en curs sobre els fonaments matemàtics que utilitzen la teoria de tipus d'homotopia.

Els matemàtics que treballaven en teoria de categories ja tenien dificultats per treballar amb els fonaments àmpliament acceptats de la teoria de conjunts de Zermelo-Fraenkel. Això va conduir a propostes com la Teoria Elemental de la Categoria de Conjunts (ETCS) de Lawvere. La teoria de tipus d'homotopia continua en aquesta línia utilitzant la teoria de tipus. Els investigadors estan explorant connexions entre els tipus dependents (especialment el tipus identitat) i la topologia algebraica (específicament l'homotopia).

Assistents de prova Gran part de la recerca actual en teoria de tipus està impulsada per verificadors de proves, assistents de prova interactius i demostradors de teoremes automatitzats. La majoria d'aquests sistemes utilitzen una teoria de tipus com a base matemàtica per codificar proves, cosa que no és sorprenent, donada l'estreta connexió entre la teoria de tipus i els llenguatges de programació:

LF és utilitzat per Twelf, sovint per definir altres teories de tipus; Moltes teories de tipus que pertanyen a la lògica d'ordre superior són utilitzades per la família de demostradors HOL i PVS; La teoria de tipus computacional és utilitzada per NuPRL; El càlcul de construccions i les seves derivades són utilitzats per Rocq (anteriorment conegut com a Coq ), Matita i Lean; La UTT (Teoria Unificada de Tipus Depenents de Luo) és utilitzada per Agda, que és alhora un llenguatge de programació i un assistent de prova.

Moltes teories de tipus són compatibles amb LEGO i Isabelle. Isabelle també admet fonaments a més de les teories de tipus, com ara ZFC. Mizar és un exemple d'un sistema de demostració que només admet la teoria de conjunts.

Llenguatges de programació Qualsevol anàlisi estàtica de programes, com ara els algoritmes de comprovació de tipus en la fase d'anàlisi semàntica del compilador, té una connexió amb la teoria de tipus. Un exemple principal és Agda, un llenguatge de programació que utilitza UTT (Teoria Unificada de Tipus Depenents de Luo) per al seu sistema de tipus.

El llenguatge de programació ML es va desenvolupar per manipular teories de tipus (vegeu LCF) i el seu propi sistema de tipus va estar molt influenciat per aquestes.

Lògica Una teoria de tipus és una lògica matemàtica, és a dir, un conjunt de regles d'inferència que donen lloc a judicis. La majoria de les lògiques tenen judicis que afirmen "La proposició és certa", o "La fórmula és una fórmula ben formada". Una teoria de tipus té judicis que defineixen els tipus i els assignen a una col·lecció d'objectes formals, coneguts com a termes. Un terme i el seu tipus sovint s'escriuen junts com a .

Termes En lògica, un terme es defineix recursivament com un símbol constant, una variable o una aplicació de funció, on un terme s'aplica a un altre terme. Els símbols constants poden incloure el nombre natural , el valor booleà , i funcions com ara la funció successora i operador condicional Així, alguns termes podrien ser , , , i .

Judicis La majoria de teories de tipus tenen 4 judicis:

" és un tipus " " és un terme del tipus " "Tipus és igual al tipus " "Termes i tots dos de tipus són iguals "

Els judicis poden derivar-se de suposicions. Per exemple, es podria dir "suposant és un terme del tipus i és un terme del tipus , d'això es dedueix que és un terme del tipus ". Aquests judicis s'escriuen formalment amb el símbol del torniquet .

Si no hi ha suposicions, no hi haurà res a l'esquerra del torniquet.

La llista de suposicions de l'esquerra és el context del judici. Majúscules gregues, com ara i , són opcions comunes per representar algunes o totes les suposicions.

Regles d'inferència Les regles d'inferència d'una teoria de tipus diuen quins judicis es poden fer, basant-se en l'existència d'altres judicis. Les regles s'expressen com una deducció d'estil Gentzen utilitzant una línia horitzontal, amb els judicis d'entrada requerits per sobre de la línia i el judici resultant per sota de la línia. Per exemple, la següent regla d'inferència estableix una regla de substitució per a la igualtat de judicis.

Les regles són sintàctiques i funcionen reescrivint. Les metavariables , , , , i en realitat pot consistir en termes i tipus complexos que contenen moltes aplicacions de funcions, no només símbols individuals.

Per generar un judici particular en teoria de tipus, hi ha d'haver una regla per generar-lo, així com regles per generar totes les entrades requerides per aquesta regla, i així successivament. Les regles aplicades formen un arbre de prova, on les regles superiors no necessiten suposicions. Un exemple d'una regla que no requereix cap entrada és una que estableix el tipus d'un terme constant. Per exemple, afirmar que hi ha un terme de tipus , s'escriuria el següent.

Connexions a fonaments El marc lògic d'una teoria de tipus s'assembla a la lògica intuïcionista o constructiva. Formalment, la teoria de tipus sovint es cita com una implementació de la interpretació de Brouwer-Heyting-Kolmogorov de la lògica intuïcionista. A més, es poden fer connexions amb la teoria de categories i els programes informàtics.

Diferències amb la teoria de conjunts El fonament més comunament acceptat per a les matemàtiques és la lògica de primer ordre amb el llenguatge i els axiomes de la teoria de conjunts de Zermelo-Fraenkel amb l'axioma d'elecció, abreujat ZFC. Les teories de tipus que tenen prou expressibilitat també poden actuar com a fonament de les matemàtiques. Hi ha diverses diferències entre aquests dos enfocaments.

La teoria de conjunts té regles i axiomes, mentre que les teories de tipus només tenen regles. Les teories de tipus, en general, no tenen axiomes i es defineixen per les seves regles d'inferència. La teoria de conjunts i la lògica clàssiques tenen la llei del terç exclòs. Quan una teoria de tipus codifica els conceptes de "i" i "o" com a tipus, condueix a la lògica intuïcionista i no necessàriament té la llei del terç exclòs. En teoria de conjunts, un element no està restringit a un conjunt. L'element pot aparèixer en subconjunts i unions amb altres conjunts. En teoria de tipus, els termes (generalment) pertanyen només a un tipus. Quan s'utilitzaria un subconjunt, la teoria de tipus pot utilitzar una funció de predicat o utilitzar un tipus de producte de tipus dependent, on cada element s'aparella amb una demostració que la propietat del subconjunt es compleix per a Quan s'utilitzaria una unió, la teoria de tipus utilitza el tipus suma, que conté nous termes canònics. La teoria de tipus té una noció de computació inherent. Per tant, "1+1" i "2" són termes diferents en la teoria de tipus, però calculen amb el mateix valor. A més, les funcions es defineixen computacionalment com a termes lambda. En la teoria de conjunts, "1+1=2" significa que "1+1" és només una altra manera de referir-se al valor "2". La computació de la teoria de tipus requereix un concepte complicat d'igualtat. La teoria de conjunts codifica els nombres com a conjunts. La teoria de tipus pot codificar els nombres com a funcions utilitzant la codificació de Church, o més naturalment com a tipus inductius, i la construcció s'assembla molt als axiomes de Peano. En teoria de tipus, les demostracions són tipus, mentre que en teoria de conjunts, les demostracions formen part de la lògica de primer ordre subjacent.

Els defensors de la teoria de tipus també assenyalaran la seva connexió amb les matemàtiques constructives a través de la interpretació BHK, la seva connexió amb la lògica mitjançant l'isomorfisme de Curry-Howard i les seves connexions amb la teoria de categories.

Referències

Categoria:Informàtica Categoria:Ordinadors