Sistema O

En llògica matemàtica, Sistema O i Sistema O⁻ són sistemes de tipos purs, és dir, formes especials d'un càlcul lambda tipado en un número arbitrari de gèneros, axioma i regles (o dependències entre els gèneros). Jean-Yves Girard va demostrar que abdós eren inconsistentes en 1972. Este resultat va dur a donar-se conte de que la teoria de tipos original de Martin-Löf de 1971 era inconsistente, ya que permetia el mateix comportament de «Tipo en tipo» que explota la paradoxa de Girard.

Definició formal

El Sistema O es definix com un sistema de tipo pur en

• tres tipos $\{\ast ,◻,\mathrm{△}\}$ ;
• dos axioma $\{\ast :◻,◻:\mathrm{△}\}$ ; i
• cinc regles $\{(\ast ,\ast ),(◻,\ast ),(◻,◻),(\mathrm{△},\ast ),(\mathrm{△},◻)\}$ .

El Sistema O⁻ es definix igual en l'excepció de el $(\mathrm{△},\ast )$ regla.

els tipos $\ast$ i $◻$ es denominen convencionalment «Tipo» i «Tipo», respectivament; el tipo $\mathrm{△}$ no té un nom específic. Els dos axioma descriuen la contenció de tipos en classes ( $\ast :◻$ ) i tipos en $\mathrm{△}$ ( $◻:\mathrm{△}$ ). Intuitivament, els gèneros descriuen una jerarquia en la naturalea dels térmens.

1. Tots els valors tenen un tipo, com un tipo base ( p. eix. $b:\mathrm{B}\mathrm{o}\mathrm{o}\mathrm{l}$ es llig com " b és un booleano") o un tipo de funció (depenent) ( p. eix. $f:\mathrm{N}\mathrm{a}\mathrm{t}\to \mathrm{B}\mathrm{o}\mathrm{o}\mathrm{l}$ es llig com “ f és una funció d'número natural a booleanos”).
2. $\ast$ és el gènero de tots eixos tipos ( $t:\ast$ es llig com “ t és un tipo”). De $\ast$ podem construir més térmens, com $\ast \to \ast$ que és el tipo d'operadors unarios de nivell de tipo ( p. eix. $\mathrm{L}\mathrm{i}\mathrm{s}\mathrm{t}:\ast \to \ast$ es llig com “ List és una funció de tipos a tipos”, és dir, un tipo polimòrfic). Les regles restringixen cóm podem formar nous tipos.
3. $◻$ és el tipo de tots eixos tipos ( $k:◻$ es llig com “ k és una espècie”). D'igual forma podem construir térmens relacionats, d'acort a lo que permeten les regles.
4. $\mathrm{△}$ és el gènero de tots eixos térmens.

Les regles rigen les dependències entre els gèneros: $(\ast ,\ast )$ diu que els valors poden dependre dels valors (funciones), $(◻,\ast )$ permet que els valors depenguen dels tipos (polimorfisme), $(◻,◻)$ permet que els tipos depenguen dels tipos (operadors de tipo), i aixina successivament.

Paradoxa de Girard

Les definicions de Sistema O i O⁻ permeten l'assignació de tipos polimòrfics a constructors genèrics de forma anàloga als tipos polimòrfics de térmens en càlculs lambda polimòrfics clàssics, com Sistema F. Un eixemple d'un constructor genèric d'este tipo podria ser (a on k denota una espècie de variable)

$\lambda k^{◻}\lambda {\alpha }^{k\to k}\lambda {\beta }^k.\alpha (\alpha \beta ):\Pi k:◻((k\to k)\to k\to k)$ .

Este mecanisme és suficient per a construir un terme en el tipo $(\mathrm{\forall }p:\ast ,p)$ (equival al tipo $\mathrm{\perp }$ ), lo que implica que tot tipo està habitat. Per la correspondència de Curry-Howard, açò és equivalent a que totes les proposicions llògiques siguen demostradores, lo que fa que el sistema siga inconsistente.

La paradoxa de Girard és l'anàlec teòric de tipos de la paradoxa de Russell en la teoria de conjunts.