stringtranslate.com

tipo cociente

En el campo de la teoría de tipos en informática , un tipo cociente es un tipo de datos que respeta una relación de igualdad definida por el usuario . Un tipo cociente define una relación de equivalencia entre elementos del tipo; por ejemplo, podríamos decir que dos valores del tipo son equivalentes si tienen el mismo nombre; formalmente si . En las teorías de tipos que permiten tipos de cocientes, se establece un requisito adicional de que todas las operaciones deben respetar la equivalencia entre elementos. Por ejemplo, si es una función sobre valores de tipo , debe darse el caso de que para dos s y , si entonces .Personp1 == p2p1.name == p2.namefPersonPersonp1p2p1 == p2f(p1) == f(p2)

Los tipos de cociente son parte de una clase general de tipos conocidos como tipos de datos algebraicos . A principios de la década de 1980, se definieron e implementaron tipos de cocientes como parte del asistente de prueba Nuprl , en un trabajo dirigido por Robert L. Constable y otros. [1] [2] Los tipos de cociente se han estudiado en el contexto de la teoría de tipos de Martin-Löf , [3] la teoría de tipos dependientes , [4] la lógica de orden superior , [5] y la teoría de tipos de homotopía . [6]

Definición

Para definir un tipo de cociente, normalmente se proporciona un tipo de datos junto con una relación de equivalencia en ese tipo, por ejemplo, Person // ==donde ==hay una relación de igualdad definida por el usuario. Los elementos del tipo cociente son clases de equivalencia de elementos del tipo original. [3]

Los tipos de cocientes se pueden utilizar para definir la aritmética modular . Por ejemplo, si Integeres un tipo de datos de números enteros, se puede definir diciendo que si la diferencia es par. Luego formamos el tipo de números enteros módulo 2: [1]

Integer //

Se puede demostrar que las operaciones con números enteros +están -bien definidas en el nuevo tipo de cociente.

Variaciones

En las teorías de tipos que carecen de tipos de cocientes, a menudo se utilizan setoides (conjuntos explícitamente equipados con una relación de equivalencia) en lugar de tipos de cocientes. Sin embargo, a diferencia de los setoides, muchas teorías de tipos pueden requerir una prueba formal de que cualquier función definida en tipos de cocientes está bien definida . [7]

Propiedades

Los tipos de cociente son parte de una clase general de tipos conocidos como tipos de datos algebraicos . Así como los tipos de producto y los tipos de suma son análogos al producto cartesiano y la unión disjunta de estructuras algebraicas abstractas, los tipos de cociente reflejan el concepto de cocientes de teoría de conjuntos , conjuntos cuyos elementos se dividen en clases de equivalencia mediante una relación de equivalencia dada en el conjunto. Las estructuras algebraicas cuyo conjunto subyacente es un cociente también se denominan cocientes. Ejemplos de tales estructuras de cocientes incluyen conjuntos de cocientes , grupos , anillos , categorías y, en topología, espacios de cocientes . [3]

Referencias

  1. ^ ab Constable, Robert L. (1986). Implementación de Matemáticas con el Sistema de Desarrollo Nuprl Proof. Prentice Hall. ISBN 978-0-13-451832-9.
  2. ^ Agente, RL (1984). "Matemáticas como programación". En Clarke, Edmund; Kozen, Dexter (eds.). Lógicas de Programas . Apuntes de conferencias sobre informática. vol. 164. Berlín, Heidelberg: Springer. págs. 116-128. doi :10.1007/3-540-12896-4_359. hdl : 1813/6405 . ISBN 978-3-540-38775-6.
  3. ^ abc Li, Nuo (15 de julio de 2015). "Tipos de cocientes en teoría de tipos". eprints.nottingham.ac.uk . Consultado el 13 de septiembre de 2023 .
  4. ^ Hofmann, Martín (1995). "Un modelo simple para tipos de cocientes". Cálculos Lambda mecanografiados y aplicaciones . Apuntes de conferencias sobre informática. vol. 902. Berlín, Heidelberg: Springer. págs. 216-234. doi :10.1007/BFb0014055. ISBN 978-3-540-49178-1.
  5. ^ Más hogareño, Peter V. (2005). "Una estructura de diseño para cocientes de orden superior". En Hurd, Joe; Melham, Tom (eds.). Demostración de teoremas en lógica de orden superior . Apuntes de conferencias sobre informática. vol. 3603. Berlín, Heidelberg: Springer. págs. 130-146. doi :10.1007/11541868_9. ISBN 978-3-540-31820-0.
  6. ^ "El libro HoTT". Teoría del tipo de homotopía . 2013-03-12 . Consultado el 13 de septiembre de 2023 .
  7. ^ Hofmann, Martín (1997). "Constructos extensionales en la teoría de tipos intensionales". Enlace Springer . doi :10.1007/978-1-4471-0963-1. ISBN 978-1-4471-1243-3.

Ver también