Setoid

En matemáticas , un setoide ( X , ~) es un conjunto (o tipo ) X dotado de una relación de equivalencia ~. Un setoide también puede denominarse conjunto E , conjunto de Bishop o conjunto extensional . ^{[ 1 ]}

Los setoides se estudian especialmente en la teoría de la demostración y en los fundamentos de la teoría de tipos en matemáticas . A menudo, en matemáticas, al definir una relación de equivalencia en un conjunto, se forma inmediatamente el conjunto cociente (convirtiendo la equivalencia en igualdad ). En cambio, los setoides se utilizan cuando es necesario mantener una diferencia entre identidad y equivalencia, generalmente con una interpretación de la igualdad intensional (la igualdad en el conjunto original) y la igualdad extensional (la relación de equivalencia o la igualdad en el conjunto cociente).

En la teoría de la demostración, particularmente en la teoría de la demostración de las matemáticas constructivas basada en la correspondencia de Curry-Howard , a menudo se identifica una proposición matemática con su conjunto de demostraciones (si las hay). Una proposición dada puede tener muchas demostraciones, por supuesto; según el principio de irrelevancia de la demostración, normalmente solo importa la veracidad de la proposición, no qué demostración se utilizó. Sin embargo, la correspondencia de Curry-Howard puede convertir las demostraciones en algoritmos , y las diferencias entre algoritmos suelen ser importantes. Por lo tanto, los teóricos de la demostración pueden preferir identificar una proposición con un conjunto de demostraciones, considerando que las demostraciones son equivalentes si pueden convertirse entre sí mediante la conversión beta o similar.

En los fundamentos de las matemáticas basados ​​en la teoría de tipos, los setoides pueden utilizarse en una teoría de tipos que carece de tipos cociente para modelar conjuntos matemáticos generales. Por ejemplo, en la teoría de tipos intuicionista de Per Martin-Löf , no existe un tipo de números reales , sino solo un tipo de sucesiones regulares de Cauchy de números racionales . Por lo tanto, para realizar análisis real en el marco de Martin-Löf, es necesario trabajar con un setoide de números reales, el tipo de sucesiones regulares de Cauchy dotado de la noción habitual de equivalencia. Es necesario definir predicados y funciones de números reales para sucesiones regulares de Cauchy y demostrar su compatibilidad con la relación de equivalencia. Típicamente (aunque depende de la teoría de tipos utilizada), el axioma de elección se cumple para funciones entre tipos (funciones intensionales), pero no para funciones entre setoides (funciones extensionales). El término «conjunto» se utiliza indistintamente como sinónimo de «tipo» o como sinónimo de «setoide». ^{[ 2 ]}

En matemáticas constructivas , a menudo se utiliza un setoide con una relación de separación en lugar de una relación de equivalencia, denominado setoide constructivo . En ocasiones, también se considera un setoide parcial mediante una relación de equivalencia parcial o una separación parcial (véase, por ejemplo, Barthe et al. , sección 1).

• Grupoide

• Hofmann, Martin (1995), "Un modelo simple para tipos cociente", Cálculos lambda tipados y aplicaciones (Edimburgo, 1995) , Lecture Notes in Comput. Sci., vol.  902, Berlín: Springer, pp. 216–234 , CiteSeerX 10.1.1.55.4629 , doi : 10.1007/BFb0014055 , ISBN   978-3-540-59048-4, MR 1477985 .
• Barthe, Gilles; Capretta, Venanzio; Pons, Olivier (2003), "Setoides en la teoría de tipos" (PDF) , Journal of Functional Programming , 13 (2): 261–293 , doi : 10.1017/S0956796802004501 , MR 1985376 , S2CID 10069160  .

• Implementación de setoides en Rocq
• Setoid en el laboratorio n
• Bishop se instaló en el Laboratorio n