En la teoría de tipos , un sistema tiene tipos inductivos si tiene facilidades para crear un nuevo tipo a partir de constantes y funciones que crean términos de ese tipo. La función cumple una función similar a las estructuras de datos en un lenguaje de programación y permite que una teoría de tipos agregue conceptos como números , relaciones y árboles . Como sugiere el nombre, los tipos inductivos pueden ser autorreferenciales, pero generalmente solo de una manera que permita la recursividad estructural .
El ejemplo estándar es codificar los números naturales usando la codificación de Peano .
Nat inductivo : Tipo : = | 0 : nat | S : nat -> nat .
Aquí, un número natural se crea a partir de la constante "0" o aplicando la función "S" a otro número natural. "S" es la función sucesora que representa sumar 1 a un número. Por tanto, "0" es cero, "S 0" es uno, "S (S 0)" es dos, "S (S (S 0))" es tres, y así sucesivamente.
Desde su introducción, los tipos inductivos se han extendido para codificar más y más estructuras, sin dejar de ser predicativos y de apoyo a la recursividad estructural.
Eliminación
Los tipos inductivos generalmente vienen con una función para probar propiedades sobre ellos. Por lo tanto, "nat" puede venir con:
nat_elim : ( forall P : nat -> Prop , ( P 0 ) -> ( forall n , P n -> P ( S n )) -> ( forall n , P n )).
Esta es la función esperada para la recursividad estructural para el tipo "nat".
Implementaciones
Tipos W y M
Los tipos W son tipos bien fundamentados en la teoría de tipos intuicionista (ITT). [1] Generalizan números naturales, listas, árboles binarios y otros tipos de datos "en forma de árbol". Sea U un universo de tipos . Dado un tipo A : U y una familia dependiente B : A → U , se puede formar un tipo W. El tipo A puede considerarse como "etiquetas" para los (potencialmente infinitos) constructores del tipo inductivo que se está definiendo, mientras que B indica la aridad (potencialmente infinita) de cada constructor. Los tipos W (resp. Tipos M) también pueden entenderse como árboles bien fundamentados (resp. No bien fundamentados) con nodos etiquetados por elementos a : A y donde el nodo etiquetado por a tiene B ( a ) -muchos subárboles. [2] Cada tipo W es isomorfo al álgebra inicial de un llamado funtor polinomial .
Sean 0 , 1 , 2 , etc. tipos finitos con habitantes 1 1 : 1 , 1 2 , 2 2 : 2 , etc. Se pueden definir los números naturales como el tipo W
con f : 2 → U se define por f (1 2 ) = 0 (que representa el constructor de cero, que no toma argumentos), y f (2 2 ) = 1 (que representa la función sucesora, que toma un argumento).
Se pueden definir listas sobre un tipo A : U como dónde
y 1 1 es el único habitante de 1 . El valor de corresponde al constructor de la lista vacía, mientras que el valor de corresponde al constructor que agrega un al principio de otra lista.
El constructor de elementos de un tipo W genérico tiene tipo
También podemos escribir esta regla en el estilo de una prueba de deducción natural ,
La regla de eliminación para los tipos W funciona de manera similar a la inducción estructural en árboles. Si, siempre que una propiedad (bajo la interpretación de proposiciones como tipos ) se aplica a todos los subárboles de un árbol dado, también se aplica a ese árbol, luego se aplica a todos los árboles.
En las teorías de tipo extensional, los tipos W (resp. Tipos M) se pueden definir hasta el isomorfismo como álgebras iniciales (resp. Coalgebras finales) para functores polinomiales . En este caso, la propiedad de inicialidad (res. Finalidad) corresponde directamente al principio de inducción apropiado. [3] En las teorías de tipo intensional con el axioma de univalencia , esta correspondencia se mantiene hasta la homotopía (igualdad proposicional). [4] [5] [6]
Los tipos M son duales a los tipos W, representan datos coinductivos (potencialmente infinitos) como flujos . [7] Los tipos M pueden derivarse de los tipos W. [8]
Definiciones mutuamente inductivas
Esta técnica permite algunas definiciones de múltiples tipos que dependen unas de otras. Por ejemplo, definir dos predicados de paridad en números naturales usando dos tipos mutuamente inductivos en Coq :
Inductivo incluso : nat -> Prop : = | zero_is_even : even O | S_of_odd_is_even : ( forall n : nat , impar n -> incluso ( S n )) con extraña : nat -> Prop : = | S_of_even_is_odd : ( forall n : nat , incluso n -> extraño ( S n )).
Inducción-recursión
La inducción-recursión comenzó como un estudio de los límites de la ITT. Una vez encontrados, los límites se convirtieron en reglas que permitieron definir nuevos tipos inductivos. Estos tipos pueden depender de una función y la función del tipo, siempre que ambos se definan simultáneamente.
Los tipos de universo se pueden definir mediante inducción-recursión.
Inducción-inducción
Inducción inducción permite la definición de un tipo y una familia de tipos al mismo tiempo. Entonces, un tipo A y una familia de tipos.
Tipos inductivos superiores
Esta es un área de investigación actual en la teoría de tipos de homotopía (HoTT). HoTT se diferencia de ITT por su tipo de identidad (igualdad). Los tipos inductivos superiores no solo definen un nuevo tipo con constantes y funciones que crean elementos del tipo, sino también nuevas instancias del tipo de identidad que los relacionan.
Un ejemplo simple es el círculo tipo, que se define con dos constructores, un punto de base;
- base : círculo
y un bucle;
- bucle : base = base .
La existencia de un nuevo constructor para el tipo de identidad hace que el círculo sea un tipo inductivo superior.
Ver también
- La coinducción permite (efectivamente) estructuras infinitas en la teoría de tipos.
Referencias
- ^ Martin-Löf, Per (1984). Teoría de tipos intuicionistas (PDF) . Sambin, Giovanni. Nápoles: Bibliopolis. ISBN 8870881059. OCLC 12731401 .
- ^ Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis (12 de abril de 2015). "Árboles no bien fundamentados en la teoría de tipos de homotopía". arXiv : 1504.02949 . doi : 10.4230 / LIPIcs.TLCA.2015.17 . Cite journal requiere
|journal=
( ayuda ) - ^ Dybjer, Peter (1997). "Representación de conjuntos definidos inductivamente por ordenamientos de pozo en la teoría de tipos de Martin-Löf" . Informática Teórica . 176 (1–2): 329–335. doi : 10.1016 / s0304-3975 (96) 00145-4 .
- ^ Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (18 de enero de 2012). "Tipos inductivos en la teoría de tipos de homotopía". arXiv : 1201.3898 [ matemáticas.LO ].
- ^ Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis (12 de abril de 2015). "Árboles no bien fundamentados en la teoría de tipos de homotopía". arXiv : 1504.02949 . doi : 10.4230 / LIPIcs.TLCA.2015.17 . Cite journal requiere
|journal=
( ayuda ) - ^ Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (21 de abril de 2015). "Álgebras iniciales de homotopía en teoría de tipos". arXiv : 1504.05531 [ matemáticas.LO ].
- ^ van den Berg, Benno; Marchi, Federico De (2007). "Árboles no fundados en categorías". Anales de lógica pura y aplicada . 146 (1): 40–59. arXiv : matemáticas / 0409158 . doi : 10.1016 / j.apal.2006.12.001 .
- ^ Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil (2005). "Contenedores: Construyendo tipos estrictamente positivos". Informática Teórica . 342 (1): 3-27. doi : 10.1016 / j.tcs.2005.06.002 .
- Programa de Fundaciones Univalentes (2013). Teoría de tipos de homotopía: fundamentos univalentes de las matemáticas . Instituto de Estudios Avanzados.
enlaces externos
- Diapositivas de inducción-recursividad
- Guías de inducción-inducción
- Tipos inductivos superiores: un recorrido por la colección de animales