En la teoría de tipos intuicionista (ITT), una disciplina dentro de la lógica matemática , la inducción-recursividad es una característica para declarar simultáneamente un tipo y función en ese tipo. Permite la creación de tipos más grandes, como universos, que tipos inductivos . Los tipos creados siguen siendo predicativos dentro de ITT.
Una definición inductiva viene dada por reglas para generar elementos de un tipo. Luego, se pueden definir funciones de ese tipo por inducción sobre la forma en que se generan los elementos del tipo. La inducción-recursión generaliza esta situación ya que se puede definir simultáneamente el tipo y la función, porque las reglas para generar elementos del tipo pueden referirse a la función. [1]
La inducción-recursión se puede utilizar para definir tipos grandes, incluidas varias construcciones de universos. Aumenta sustancialmente la fuerza de la teoría de la prueba de la teoría de tipos. Sin embargo, las definiciones recursivas inductivas-recursivas todavía se consideran predicativas .
Fondo
La inducción-recursión surgió de las investigaciones sobre las reglas de la teoría de tipos intuicionistas de Martin-Löf . La teoría de tipos tiene varios "formadores de tipos" y cuatro tipos de reglas para cada uno. Martin-Löf había insinuado que las reglas para cada formador de tipos seguían un patrón, que conservaba las propiedades de la teoría de tipos (por ejemplo, normalización fuerte , predicatividad ). Los investigadores comenzaron a buscar la descripción más general del patrón, ya que eso diría qué tipos de formadores de tipos se podrían agregar (¡o no!) Para extender la teoría de tipos.
El formador de tipo "universo" fue el más interesante, porque cuando las reglas se escribieron "a la Tarski", definieron simultáneamente el "tipo de universo" y una función que operaba sobre él. Esto eventualmente llevó a Dybjer a la inducción-recursividad.
Los artículos iniciales de Dybjer llamaron a la inducción-recursión un "esquema" para las reglas. Declaró qué formadores de tipo se podrían agregar a la teoría de tipos. Más tarde, él y Setzer escribirían un nuevo formador de tipos con reglas que permitieran crear nuevas definiciones de inducción-recursión dentro de la teoría de tipos. [2] Esto se agregó al asistente de prueba Half (una variante de Alf ).
La idea
Antes de cubrir los tipos inductivos-recursivos, el caso más simple son los tipos inductivos. Los constructores para tipos inductivos pueden ser autorreferenciales, pero de forma limitada. Los parámetros del constructor deben ser "positivos":
- no se refiere al tipo que se está definiendo
- ser exactamente del 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 los del tipo que se está definiendo. Los tipos inductivos-recursivos van más allá y los tipos de parámetros pueden referirse a parámetros anteriores que utilizan el tipo que se está definiendo. Estos deben ser "medio positivos":
- ser una función que dependa de un parámetro anterior si ese parámetro está envuelto en la función que se está definiendo.
Así que si es el tipo que se está definiendo y es la función que se define (simultáneamente), estas declaraciones de parámetros son positivas:
- (Depende de los parámetros anteriores, ninguno de los cuales es de tipo .)
Esto es medio positivo:
- (Depende del parámetro de tipo pero solo a través de una llamada a .)
Estos no son positivos ni semispositivos:
- ( es un parámetro de la función.)
- (El parámetro toma una función que devuelve , pero regresa sí mismo.)
- (Depende de de tipo , pero no a través de la función .)
Ejemplo de universo
Un ejemplo común simple es el formador de tipo Universe à la Tarski. Crea un tipo y una función . Hay un elemento de para cada tipo en la teoría de tipos (excepto ¡sí mismo!). La función mapea los elementos de al tipo asociado.
El tipo tiene un constructor (o regla de introducción) para cada formador de tipos en la teoría de tipos. El de las funciones dependientes sería:
Es decir, se necesita un elemento de tipo que se correlacionará con el tipo de parámetro y una función tal que para todos los valores , se asigna al tipo de retorno de la función (que depende del valor del parámetro, ). (El final dice que el resultado del constructor es un elemento de tipo .)
La reducción (o regla de cálculo) dice que
se convierte en .
Después de la reducción, la función está operando en una parte más pequeña de la entrada. Si eso se mantiene cuando se aplica a cualquier constructor, luego siempre terminará. Sin entrar en detalles, Inducción-Recursión establece qué tipos de definiciones (o reglas) se pueden agregar a la teoría de manera que las llamadas a funciones siempre terminen.
Uso
La inducción-recursividad se implementa en Agda e Idris . [3]
Ver también
- Inducción-inducción : trabajo adicional que define un tipo y una familia de tipos al mismo tiempo
Referencias
- ^ Dybjer, Peter (junio de 2000). "Una formulación general de definiciones inductivo-recursivas simultáneas en la teoría de tipos" (PDF) . Revista de lógica simbólica . 65 (2): 525–549. CiteSeerX 10.1.1.6.4575 . doi : 10.2307 / 2586554 . JSTOR 2586554 .
- ^ Dybjer, Peter (1999). Una axiomatización finita de definiciones inductivo-recursivas . Apuntes de conferencias en Ciencias de la Computación . 1581 . págs. 129-146. CiteSeerX 10.1.1.219.2442 . doi : 10.1007 / 3-540-48959-2_11 . ISBN 978-3-540-65763-7.
- ^ Bove, Ana; Dybjer, Peter; Norell, Ulf (2009). Berghofer, Stefan; Nipkow, Tobias; Urbano, cristiano; Wenzel, Makarius (eds.). "Una breve descripción de Agda: un lenguaje funcional con tipos dependientes" . Demostración de teoremas en lógicas de orden superior . Apuntes de conferencias en informática. Berlín, Heidelberg: Springer: 73–78. doi : 10.1007 / 978-3-642-03359-9_6 . ISBN 978-3-642-03359-9.