¿Intuición detrás de la estricta positividad?

10

Me pregunto si alguien puede darme la intuición detrás de por qué la estricta positividad de los tipos de datos inductivos garantiza una fuerte normalización.

Para ser claros, veo cómo tener ocurrencias negativas conduce a la divergencia, es decir, al definir:

data X where Intro : (X->X) -> X

Podemos escribir una función divergente.

Pero me pregunto, ¿cómo podemos demostrar que los tipos inductivos estrictamente positivos no permiten la divergencia? es decir, ¿hay alguna medida de inducción que nos permita construir una prueba de fuerte normalización (usando relaciones lógicas o similares)? ¿Y dónde se desglosa tal prueba de sucesos negativos? ¿Hay alguna buena referencia que muestre una fuerte normalización para un lenguaje con tipos inductivos?

jmite
fuente
Creo que la idea es que los tipos estrictamente positivos pueden convertirse a tipos W, conceptualmente. También el tipo positivo no estricto es inconsistente con Coq vilhelms.github.io/posts/… . Se comenta que tipo positivo es consistente con Agda, pero me gustaría ver una explicación conceptual también ...
molikto
@molikto Gracias, eso es útil. ¿Pero pensé que los tipos W no daban los principios de inducción deseados en una teoría intensional? ¿Cómo podemos demostrar una fuerte normalización para inductivos estrictamente positivos en una teoría intensional?
jmite

Respuestas:

8

Parece que desea una descripción general de los argumentos de normalización para sistemas de tipos con tipos de datos positivos. Recomiendo la tesis doctoral de Nax Mendler: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html .

Como sugiere la fecha, este es un trabajo bastante clásico. La intuición básica es que un ordinal puede asociarse a cualquier elemento de un tipo inductivo positivo, por ejemplo, para el tipo de datosλ

Inductive Ord = Zero : Ord | Suc : Ord -> Ord | Lim : (Nat -> Ord) -> Ord

Obtendríamos:

λ(t)=0
si es una forma normal que no es un constructor y t
λ(Zero)=0
λ(Suc(o))=λ(o)+1
λ(Lim(f))=supnλ(f n)

donde varía sobre términos con formas normales. La advertencia es que esta interpretación solo se define en el tercer caso cuando tiene una forma normal, lo que requiere un poco de cuidado en las definiciones.nf n

Entonces se pueden definir funciones recursivas por inducción sobre este ordinal.

Tenga en cuenta que estos tipos de datos ya se pueden definir en la teoría de conjuntos clásica, como se indica en el excelente artículo de Inductive Families de Dybjer ( http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf ). Sin embargo, debido a que los espacios de funciones son tan grandes, los tipos como Ordrequieren ordinales realmente grandes para interpretar.

cody
fuente
Gracias, esto es muy útil! ¿Sabes si tales ordinales se pueden definir en la teoría de tipos en sí misma? es decir, si estaba tratando de usar Agda con inducción-recursión para modelar una teoría de tipos con inductivos (pero sin inducción-recursión), ¿podría usar algo como Ordmodelar los ordinales necesarios para mostrar la fundamentación?
jmite
@jmite, puedes, pero los ordinales en teorías constructivas son un poco extraños, y también podrías trabajar con órdenes o árboles bien fundados ( al estilo W, como sugiere molikto). Sin embargo, podría ser difícil tener un tipo de uniforme único que capture la fundamentación de cada inductivo en el lenguaje objeto ...
cody
1
@cody ¿No es el ejemplo Ord que le das un tipo estrictamente positivo?
Henning Basold
1
@HenningBasold sí lo es (¡por eso lo usé como ilustración!). Pero no se comporta exactamente como los ordinales en una teoría de conjuntos (clásica), y ciertamente no como el conjunto de todos los ordinales. En particular, es un poco difícil definir un orden en estos.
cody
1
@HenningBasold también debo tener en cuenta que la pregunta de jmite era específicamente sobre tipos estrictamente positivos, ¡aunque la información sobre la configuración más general también es interesante!
cody
6

Otra buena fuente para ir más allá de los tipos estrictamente positivos es la tesis doctoral de Ralph Matthes: http://d-nb.info/956895891

Discute las extensiones del Sistema F con tipos (estrictamente) positivos en el capítulo 3 y demuestra muchos resultados de normalización fuertes en el capítulo 9. Hay algunas ideas interesantes discutidas en el capítulo 3.

  1. Podemos agregar puntos menos fijos para cualquier tipo con variable libre , siempre y cuando podamos proporcionar un testigo de monotonicidad . Esta idea ya está presente en el trabajo de Mendler que Cody mencionó. Dichos testigos existen canónicamente para cualquier tipo positivo porque estos son sintácticamente monótonos.ρααβ.(αβ)ρρ[β/α]

  2. Cuando nos movemos de tipos estrictamente positivos a positivos, los tipos inductivos ya no pueden verse como árboles (la codificación de tipo W). En cambio, estos introducen alguna forma de impredicatividad porque la construcción de un tipo inductivo positivo ya cuantifica sobre el tipo en sí. Tenga en cuenta que esta es una forma leve de impredicatividad, ya que la semántica de estos tipos todavía se puede explicar en términos de iteración ordinal de funciones monótonas.

  3. Matthes también proporciona algunos ejemplos de tipos inductivos positivos. Particularmente interesantes son

    • el tipo de continuaciones , donde no ocurre en .μ.1+((αρ)ρ)αρ
    • el tipo que funciona para cualquier tipo convirtiéndolo en un tipo positivo. Tenga en cuenta que esto utiliza la impredicatividad del sistema F muy fuertemente.μαβ.(αβ)ρ[β/α]ρρ

Matthes también utiliza tipos inductivos positivos para analizar la doble negación, por ejemplo, en este documento: https://www.irit.fr/~Ralph.Matthes/papers/MatthesStabilization.pdf . Introduce una extensión de Parigot y demuestra una fuerte normalización.λμ

Espero que esto ayude con su pregunta.

Henning Basold
fuente