Teoria de tipos

En matemàtiques, llògica i ciències de la computació, la teoria de tipos és qualsevol de varis sistemes formals que poden servir com a alternatives a la teoria de conjunts com fonament de les matemàtiques constructives, o a l'estudi de tals formalisme en general. En la teoria de llenguages de programació, una branca de les ciències de la computació, la teoria de tipos pot referir-se al disseny, anàlisis i estudi dels sistemes de tipos, encara que alguns teòrics de la computació llimiten el significat del terme a l'estudi de formalisme abstractes com el càlcul lambda tipado.

Història

Bertrand Russell va inventar la primera teoria de tipos en resposta al seu descobriment de que la versió de Gottlob Frege de la teoria ingènua de conjunts és afectada per la paradoxa de Russell. Este tipo de la teoria de tipos apareix primàriament en el Principia Mathematica de Whitehead i Russell. Esta teoria evita la paradoxa de Russell creant una jerarquia de tipos, després assignant cada entitat matemàtica a un tipo. Objectes d'un tipo donat són creats exclusivament per objectes d'un tipo anterior (aquells més avall en la jerarquia), per lo tant evitant cicles.

Alonzo Church, inventor del càlcul lambda, va desenrollar una llògica d'orde superior comunament cridada Teoria de Tipos de Church, per a evitar la paradoxa de Kleen-Rosser que afectava al càlcul lambda pur original. La teoria de tipos de Church és una variant del càlcul lambda en el qual les expressions (també cridades fòrmules o térmens lambda) són classificades en tipos, i els tipos d'expressions restringixen les maneres en que poden ser combinades. En atres paraules, és un càlcul lambda tipado. Hui en dia molts atres càlculs estan en us, incloent la teoria de tipos intuicionista de Per Martin-Löf, el Sistema F de Jean-Yves Girard i el Càlcul de Construccions. En el càlcul lambda tipado, els tipos juguen un paper similar al dels conjunts en la teoria de conjunts.