Recursión inductiva

En la teoría de tipos intuicionista (TTI), una disciplina dentro de la lógica matemática , la inducción-recursión es una característica que permite declarar simultáneamente un tipo y una función sobre ese tipo. Permite la creación de tipos más grandes que los tipos inductivos , como los universos . Los tipos creados siguen siendo predicativos dentro de la TTI.

Una definición inductiva viene dada por reglas para generar elementos de un tipo. A partir de ese tipo, se pueden definir funciones por inducción sobre la forma en que se generan sus elementos. La recursión inductiva generaliza esta situación, ya que permite definir simultáneamente el tipo y la función, puesto que las reglas para generar elementos del tipo pueden referirse a la función. ^{[ 1 ]}

La inducción recursiva puede utilizarse para definir tipos grandes, incluyendo diversas construcciones de universos. Esto aumenta sustancialmente la solidez demostrativa de la teoría de tipos. Sin embargo, las definiciones inductivas recursivas aún se consideran predicativas .

La inducción recursiva surgió de las investigaciones sobre las reglas de la teoría de tipos intuicionista de Martin-Löf . Esta teoría cuenta con varios "formadores de tipos" y cuatro tipos de reglas para cada uno. Martin-Löf había sugerido que las reglas para cada formador de tipos seguían un patrón que preservaba las propiedades de la teoría (por ejemplo, la normalización fuerte y la predicatividad ). Los investigadores comenzaron a buscar la descripción más general de este patrón, ya que esto indicaría qué tipos de formadores de tipos podrían añadirse (¡o no!) para extender la teoría de tipos.

El tipo "universo" fue el más interesante, porque cuando se escribieron las reglas "a la Tarski", definieron simultáneamente el "tipo universo" y una función que operaba sobre él. Esto finalmente llevó a Dybjer a la inducción-recursión.

Los trabajos iniciales de Dybjer llamaban a la inducción-recursión un "esquema" para reglas. Indicaba qué formadores de tipos podían añadirse a la teoría de tipos. Más tarde, él y Setzer escribirían un nuevo formador de tipos con reglas que permitían crear nuevas definiciones inductivo-recursivas dentro de la teoría de tipos. ^{[ 2 ]} Esto se añadió al asistente de prueba Half (una variante de Alf ).

Antes de abordar los tipos inductivos recursivos, veamos el caso más sencillo: los tipos inductivos. Los constructores para tipos inductivos pueden ser autorreferenciales, pero de forma limitada. Los parámetros del constructor deben ser "positivos":

• no hacer referencia al tipo que se está definiendo
• ser exactamente el tipo que se está definiendo, o
• ser una función que devuelva el tipo que se está definiendo.

Con los tipos inductivos, el tipo de un parámetro puede depender de parámetros anteriores, pero no puede referirse a parámetros del tipo que se está definiendo. Los tipos inductivos recursivos van más allá: los tipos de un parámetro pueden referirse a parámetros anteriores que utilizan el tipo que se está definiendo. Estos deben ser "semipositivos":

• ser una función que depende de un parámetro anterior si ese parámetro está incluido en la función que se está definiendo.

Entonces, si${\displaystyle D}$es el tipo que se está definiendo y${\displaystyle f}$Si la función se está definiendo (simultáneamente), estas declaraciones de parámetros son positivas:

• ${\displaystyle a:A}$
• ${\displaystyle d:D}$
• ${\displaystyle g:A\to {\mathsf {Type}}}$
• ${\displaystyle h:A\to D}$
• ${\displaystyle i:A\to B\to D}$
• ${\displaystyle j:g\ a}$ (Depende de parámetros anteriores, ninguno de los cuales es de tipo${\displaystyle D}$.)

Esto es parcialmente positivo:

• ${\displaystyle k:(f\ d)\to D}$ (Depende del parámetro)${\displaystyle d}$de tipo${\displaystyle D}$pero solo a través de una llamada a${\displaystyle f}$.)

No son ni positivos ni semipositivos:

• ${\displaystyle k:D\to A}$ (${\displaystyle D}$es un parámetro de la función.)
• ${\displaystyle l:(A\to D)\to A}$ (El parámetro toma una función que devuelve${\displaystyle D}$pero regresa${\displaystyle A}$sí mismo.)
• ${\displaystyle m:z\ d}$ (Depende de${\displaystyle d}$de tipo${\displaystyle D}$pero no a través de la función${\displaystyle f}$.)

Un ejemplo común y sencillo es el formador de tipos para un universo a la Tarski. Consiste en un tipo${\displaystyle U}$y una función${\displaystyle T:U\to {\mathsf {Type}}}$de tal manera que existe un elemento de${\displaystyle U}$para cada tipo en la teoría de tipos (excepto${\displaystyle U}$¡en sí mismo!), y la función${\displaystyle T}$mapea los elementos de${\displaystyle U}$al tipo asociado.

El tipo${\displaystyle U}$En la teoría de tipos, existe un constructor (o regla de introducción) para cada formador de tipos. El correspondiente a las funciones dependientes sería:

${\displaystyle {\mathsf {constructor}}_{\Pi }(u:U)(u':T(u)\to U):U}$

Es decir, toma un elemento${\displaystyle u}$de tipo${\displaystyle U}$que se asignará al tipo del parámetro y una función${\displaystyle u'}$de tal manera que para todos los valores${\displaystyle x:T(u)}$,${\displaystyle u'(x)}$se asigna al tipo de retorno de la función (que depende del valor del parámetro,${\displaystyle x}$). (El final${\displaystyle :U}$dice que el resultado del constructor es un elemento de tipo${\displaystyle U}$.)

La regla de reducción (o de cálculo) dice que${\displaystyle T({\mathsf {constructor}}_{\Pi }(u,u'))}$se reduce a${\displaystyle \prod _{x:T(u)}T(u'(x))}$.

Después de la reducción, la función${\displaystyle T}$está operando sobre una parte más pequeña de la entrada. Si eso se cumple cuando${\displaystyle T}$se aplica a cualquier constructor, entonces${\displaystyle T}$siempre terminará.

La recursión inductiva está implementada en Agda e Idris . ^{[ 3 ]}

• Inducción-inducción : trabajo adicional que define un tipo y una familia de tipos al mismo tiempo.

• Lista de publicaciones de Peter Dybjer sobre inducción e inducción-recursión.
• Diapositivas que abarcan la inducción-recursión y sus derivados.