En matemáticas , un setoide ( X , ~) es un conjunto (o tipo ) X equipado con una relación de equivalencia ~. Un Setoid también puede llamarse E-set , Bishop set o set extensional . [1]
Los setoides se estudian especialmente en la teoría de la prueba y en los fundamentos de la teoría de tipos de las matemáticas . A menudo, en matemáticas, cuando se define una relación de equivalencia en un conjunto, se forma inmediatamente el conjunto cociente (convirtiendo la equivalencia en igualdad ). Por el contrario, los setoides pueden usarse cuando se debe mantener una diferencia entre identidad y equivalencia, a menudo con una interpretación de igualdad intensional (la igualdad en el conjunto original) e igualdad extensional (la relación de equivalencia o la igualdad en el conjunto cociente).
Teoría de la prueba
En la teoría de la prueba, particularmente la teoría de la prueba de la matemática constructiva basada en la correspondencia Curry-Howard , a menudo se identifica una proposición matemática con su conjunto de pruebas (si las hay). Una proposición dada puede tener muchas pruebas, por supuesto; de acuerdo con el principio de irrelevancia de la prueba , normalmente sólo importa la verdad de la proposición, no qué prueba se utilizó. Sin embargo, la correspondencia Curry-Howard puede convertir las pruebas en algoritmos , y las diferencias entre los algoritmos suelen ser importantes. Por lo tanto, los teóricos de la prueba pueden preferir identificar una proposición con un conjunto de pruebas, considerando las pruebas equivalentes si pueden convertirse entre sí mediante conversión beta o similar.
Teoría de tipos
En los fundamentos de la teoría de tipos de las matemáticas, los setoides pueden usarse en una teoría de tipos que carece de tipos de cociente para modelar conjuntos matemáticos generales. Por ejemplo, en Per Martin-Löf 's teoría de tipos intuicionista , no hay ningún tipo de números reales , solamente un tipo de secuencias regulares de Cauchy de números racionales . Para hacer un análisis real en el marco de Martin-Löf, por lo tanto, uno debe trabajar con un setoide de números reales, el tipo de secuencias regulares de Cauchy equipadas con la noción habitual de equivalencia. Es necesario definir predicados y funciones de números reales para secuencias de Cauchy regulares y demostrar que son compatibles con la relación de equivalencia. Normalmente (aunque depende de la teoría de tipos utilizada), el axioma de elección se mantendrá para funciones entre tipos (funciones intensionales), pero no para funciones entre setoides (funciones extensionales). [ aclaración necesaria ] El término "conjunto" se utiliza de diversas formas como sinónimo de "tipo" o como sinónimo de "setoide". [2]
Matemáticas constructivas
En matemáticas constructivas , a menudo se toma un setoide con una relación de separación en lugar de una relación de equivalencia, llamado setoide constructivo . A veces también se considera un setoide parcial usando una relación de equivalencia parcial o separación parcial. (ver, por ejemplo, Barthe et al. , sección 1)
Ver también
Notas
- ^ Alexandre Buisse, Peter Dybjer, "La interpretación de la teoría del tipo intuicionista en categorías cerradas localmente cartesianas - una perspectiva intuicionista" , Notas electrónicas en la informática teórica 218 (2008) 21-32.
- ^ "Teoría de conjuntos de Bishop" (PDF) : 9. Cite journal requiere
|journal=
( ayuda )
Referencias
- Hofmann, Martin (1995), "Un modelo simple para tipos de cociente", Cálculos y aplicaciones lambda tipificados (Edimburgo, 1995) , Lecture Notes in Comput. Sci., 902 , Berlín: Springer, págs. 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.
enlaces externos
- Implementación de setoides en Coq
- Setoid en nLab
- Obispo en nLab