Tipo inductivo

Los tipos W son tipos bien fundados en la teoría de tipos intuicionista (ITT). ^{[ 1 ]} Generalizan los números naturales, las listas, los árboles binarios y otros tipos de datos con 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.${\displaystyle {\mathsf {W}}_{a:A}B(a)}$. El tipo A puede pensarse como "etiquetas" para los (potencialmente infinitos) constructores del tipo inductivo que se está definiendo, mientras que B indica la (potencialmente infinita) aridad de cada constructor. Los tipos W (resp. tipos M) también pueden entenderse como árboles bien fundados (resp. no bien fundados) 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 functor polinomial .

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. $${\displaystyle \mathbb {N}$$ :={\mathsf {W}}_{x:\mathbf {2} }f(x)} con f  : 2 → U se define por f (1 ₂ ) = 0 (que representa el constructor para cero, que no toma argumentos), y f (2 ₂ ) = 1 (que representa la función sucesora, que toma un argumento).

Se pueden definir listas sobre un tipo A  : U como${\displaystyle \operatorname {Lista} (A):={\mathsf {W}}_{(x:\mathbf {1} +A)}f(x)}$dónde $${\displaystyle {\begin{aligned}f(\operatorname {inl} (1_{\mathbf {1} }))&=\mathbf {0} \\f(\operatorname {inr} (a))&=\mathbf {1} \end{aligned}}}$$ y 1 ₁ es el único habitante de 1 . El valor de${\displaystyle f(\operatorname {inl} (1_{\mathbf {1} }))}$corresponde al constructor para la lista vacía, mientras que el valor de${\displaystyle f(\operatorname {inr} (a))}$corresponde al constructor que agrega un al principio de otra lista.

El constructor para elementos de un tipo W genérico${\displaystyle {\mathsf {W}}_{x:A}B(x)}$tiene tipo $${\displaystyle {\mathsf {sup}}:\prod _{a:A}{\Big (}B(a)\to {\mathsf {W}}_{x:A}B(x){\Big )}\to {\mathsf {W}}_{x:A}B(x).}$$ También podemos escribir esta regla al estilo de una demostración por deducción natural , $${\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 (bajo la interpretación de proposiciones como tipos )${\displaystyle C:{\mathsf {W}}_{x:A}B(x)\to U}$Si se cumple para todos los subárboles de un árbol dado, también se cumple para ese árbol, y luego se cumple para todos los árboles.

$${\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 (o M) pueden definirse, salvo isomorfismo , como álgebras iniciales (o coálgebras finales) para functores polinomiales . En este caso, la propiedad de inicialidad (o finalidad) corresponde directamente al principio de inducción apropiado. ^{[ 3 ]} En las teorías de tipos intensionales con el axioma de univalencia , esta correspondencia se mantiene salvo 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 se pueden derivar de los tipos W. ^{[ 8 ]}

Esta técnica permite definir varios tipos que dependen unos de otros. Por ejemplo, definir dos predicados de paridad sobre números naturales utilizando dos tipos mutuamente inductivos en Rocq:

Inductivo par : nat -> Prop := | zero_is_even : even O | S_of_odd_is_even : ( para todo n : nat , odd n -> even ( S n )) con odd : nat -> Prop := | S_of_even_is_odd : ( para todo n : nat , even n -> odd ( S n )).

La inducción-recursión surgió como un estudio de los límites de la Teoría de Tipos Inductivos (TTI). Una vez descubiertos, estos límites se transformaron en reglas que permitieron definir nuevos tipos inductivos. Dichos tipos podían depender de una función, y la función del tipo, siempre que ambos se definieran simultáneamente.

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

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

Esta es un área de investigación actual en la teoría de tipos homotópicos (HoTT). Se diferencia de la teoría de tipos inductivos (ITT) por su tipo identidad (igualdad). Los tipos inductivos superiores definen un nuevo tipo con constantes y funciones que crean elementos del tipo, y nuevas instancias del tipo 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 identidad convierte al círculo en un tipo inductivo superior.