tipo inductivo

En 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 característica 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 normalmente sólo de una manera que permita la recursividad estructural .

El ejemplo estándar es codificar los números naturales utilizando la codificación de Peano . Se puede definir en Coq de la siguiente manera:

  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. Así, "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 ampliado para codificar cada vez más estructuras, sin dejar de ser predicativos y respaldar la recursividad estructural.

Eliminación

Los tipos inductivos suelen venir con una función para demostrar propiedades sobre ellos. Por lo tanto, "nat" puede venir con (en la sintaxis de Coq):

 nat_elim  :  ( forall  P  :  nat  ->  Prop ,  ( P  0 )  ->  ( forall  n ,  P  n  ->  P  ( S  n ))  ->  ( forall  n ,  P  n )).

En palabras: para cualquier predicado "P" sobre números naturales, dada una prueba de "P 0" y una prueba de "P n -> P (n+1)", obtenemos una prueba de "forall n, P n ". Este es el conocido principio de inducción de los números naturales.

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 (o no bien fundados) con nodos etiquetados por los 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 . ${\displaystyle {\mathsf {W}}_{a:A}B(a)}$

Sean 0 , 1 , 2 , etc. tipos finitos con habitantes 1 ₁  : 1 , 1 ₂ , 2 ₂ : 2 , etc. Se pueden definir los números naturales como el tipo W con f  : 2 → U definido por f (1 ₂ ) = 0 (que representa el constructor de cero, que no toma argumentos), y f (2 ₂ ) = 1 (que representa la función sucesora, que toma un argumento). $${\displaystyle \mathbb {N} :={\mathsf {W}}_{x:\mathbf {2} }f(x)}$$

Se pueden definir listas sobre un tipo A  : U como donde y 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 a al comienzo de otra lista. ${\displaystyle \operatorname {List} (A):={\mathsf {W}}_{(x:\mathbf {1} +A)}f(x)}$ $${\displaystyle {\begin{aligned}f(\operatorname {inl} (1_{\mathbf {1} }))&=\mathbf {0} \\f(\operatorname {inr} (a))&=\mathbf {1} \end{aligned}}}$$ ${\displaystyle f(\operatorname {inl} (1_{\mathbf {1} }))}$ ${\displaystyle f(\operatorname {inr} (a))}$

El constructor para 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 , ${\displaystyle {\mathsf {W}}_{x:A}B(x)}$ $${\displaystyle {\mathsf {sup}}:\prod _{a:A}{\Big (}B(a)\to {\mathsf {W}}_{x:A}B(x){\Big )}\to {\mathsf {W}}_{x:A}B(x).}$$ $${\displaystyle {\frac {a:A\qquad f:B(a)\to {\mathsf {W}}_{x:A}B(x)}{{\mathsf {sup}}(a,f):{\mathsf {W}}_{x:A}B(x)}}.}$$

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 (según la interpretación de proposiciones como tipos ) se cumple para todos los subárboles de un árbol dado, también se cumple para ese árbol, entonces se cumple para todos los árboles. ${\displaystyle C:{\mathsf {W}}_{x:A}B(x)\to U}$

$${\displaystyle {\frac {w:{\mathsf {W}}_{a:A}B(a)\qquad a:A,\;f:B(a)\to {\mathsf {W}}_{x:A}B(x),\;c:\prod _{b:B(a)}C(f(b))\;\vdash \;h(a,f,c):C({\mathsf {sup}}(a,f))}{{\mathsf {elim}}(w,h):C(w)}}}$$

En las teorías de tipos extensionales, los tipos W (resp. tipos M) se pueden definir hasta el isomorfismo como álgebras iniciales (resp. coalgebras finales) para funtores 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 y 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 unos de otros. Por ejemplo, definir dos predicados de paridad en números naturales utilizando dos tipos mutuamente inductivos en Coq :

 Par  inductivo :  nat  ->  Prop  :=  |  zero_is_even  :  par  O  |  S_of_odd_is_even  :  ( forall  n : nat ,  impar  n  ->  par  ( S  n )) con  impar  :  nat  ->  Prop  :=  |  S_of_even_is_odd  :  ( forall  n : nat ,  par  n  ->  impar  ( S  n )).

Inducción-recursión

La inducción-recursión comenzó como un estudio sobre los límites de la ITT. Una vez encontrados, los límites se convirtieron en reglas que permitieron definir nuevos tipos inductivos. Estos tipos podrían depender de una función y la función del tipo, siempre que ambos estuvieran definidos simultáneamente.

Los tipos de universo se pueden definir mediante inducción-recursión.

Inducción-inducción

La inducción-inducción permite definir un tipo y una familia de tipos al mismo tiempo. Entonces, un tipo A y una familia de tipos . ${\displaystyle B:A\to Type}$

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 sólo 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 sencillo es el tipo círculo , que se define con dos constructores, un punto 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

1. Martin-Löf, Per (1984). Teoría de tipos intuicionista (PDF) . Sambin, Giovanni. Nápoles: Bibliópolis. ISBN 8870881059. OCLC  12731401.
2. 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 . Procedimientos internacionales de informática de Leibniz (LIPIcs). vol. 38. págs. 17-30. arXiv : 1504.02949 . doi : 10.4230/LIPIcs.TLCA.2015.17 . ISBN 9783939897873. S2CID  15020752.
3. Dybjer, Peter (1997). "Representación de conjuntos definidos inductivamente mediante buenos ordenamientos 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.
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].
5. 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 . Procedimientos internacionales de informática de Leibniz (LIPIcs). vol. 38. págs. 17-30. arXiv : 1504.02949 . doi : 10.4230/LIPIcs.TLCA.2015.17 . ISBN 9783939897873. S2CID  15020752.
6. 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].
7. van den Berg, Benno; Marchi, Federico De (2007). "Árboles no bien fundamentados 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. S2CID  360990.
8. Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil (2005). "Contenedores: Construcción de tipos estrictamente positivos". Informática Teórica . 342 (1): 3–27. CiteSeerX 10.1.1.166.34 . doi : 10.1016/j.tcs.2005.06.002 . 

• Programa de Cimentaciones 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-recursión
• Diapositivas de inducción-inducción
• Tipos inductivos superiores: un recorrido por la casa de fieras