Tipo inductivo - Inductive type

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 .

 Inductive nat : Type :=
   | 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)).

Ésta 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). 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 de 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. Cada tipo W es isomorfo al álgebra inicial de un llamado functor 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

{\ Displaystyle \ mathbb {N}: = {\ mathsf {W}} _ {x: \ mathbf {2}} f (x)}

con f : 2 → U se define 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).

Se pueden definir listas sobre un tipo A : U como donde ${\ Displaystyle \ operatorname {Lista} (A): = {\ mathsf {W}} _ {(x: \ mathbf {1} + A)} f (x)}$

{\ Displaystyle {\ begin {alineado} f (\ operatorname {inl} (1 _ {\ mathbf {1}})) & = \ mathbf {0} \\ f (\ operatorname {inr} (a)) & = \ mathbf {1} \ end {alineado}}}

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 un al principio de otra lista.

{\ Displaystyle f (\ operatorname {inl} (1 _ {\ mathbf {1}}))}

{\ Displaystyle f (\ operatorname {inr} (a))}

El constructor de elementos de un tipo W genérico tiene el tipo ${\ 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).}

También podemos escribir esta regla en el estilo de una prueba de 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 (según la interpretación de proposiciones como tipos ) es válida para todos los subárboles de un árbol dado, también es válida para ese árbol, entonces es válida 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 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. En las teorías de tipo intensional con el axioma de univalencia , esta correspondencia se mantiene hasta la homotopía (igualdad proposicional).

Los tipos M son duales a los tipos W, representan datos coinductivos (potencialmente infinitos) como flujos . Los tipos M se pueden derivar de los tipos W.

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 :

Inductive even : nat -> Prop :=
  | zero_is_even : even O
  | S_of_odd_is_even : (forall n:nat, odd n -> even (S n))
with odd : nat -> Prop :=
  | S_of_even_is_odd : (forall n:nat, even n -> odd (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 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

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 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 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

Programa de Fundaciones Univalentes (2013). Teoría de tipos de homotopía: fundamentos univalentes de las matemáticas . Instituto de Estudios Avanzados.

Languages

In other projects