Parametricidad de la lógica lineal

Somos capaces de demostrar teoremas un parametricity gratis sobre funciones como ? Se supone que indica que f toma una lista y siempre devuelve una permutación de la misma.$f : \forall A . [A] ⊸ [A]$$f$

Otro ejemplo: probar que la función siempre devolverá una lista permutada con exactamente un elemento copiado.$f : \forall A . (A ⊸ (A, A)) ⊸ [A] ⊸ [A]$

Varias personas están interesadas en probar este tipo de cosas. Neel Krishnaswami mencionó este teorema particular aquí . También he visto a Frank Pfenning dar algunos ejemplos geniales para lógicas ordenadas. Por ejemplo, si tiene , entonces, en un sistema de tipo ordenado, e debe agregar las listas x e y .$A, x : [A], y : [A] \vdash e : [A]$$e$$x$$y$

La respuesta corta es que sí, podemos probar su primer ejemplo. En el contexto de los cálculos lambda, en este artículo se describe un enfoque lógico basado en las relaciones . Probarían tu teorema en dos pasos:

1. Defina una interpretación relacional de los tipos y úsela para probar un teorema libre convencional que ignore completamente la linealidad, es decir, esencialmente usando el mismo razonamiento que ve en, por ejemplo, "¡Teoremas gratis!". Dada , el teorema libre habitual nos dice que f devuelve una lista que contiene solo elementos que estaban presentes en la lista que se le dio. Dada una lista de variables lineales libres distintos x 1 ... x n , se deduce que f [ x 1 , . . . $\vdash f : \forall A . [A] \multimap [A]$$f$$x_1 \ldots x_n$ evalúa a alguna lista [ y 1 , . . . , Y m ] donde { y 1 , ... , y m } ⊆ { x 1 , . . . , x n } .$f [x_1, ..., x_n]$$[y_1, ..., y_m]$$\{y_1, \ldots, y_m\} \subseteq \{x_1, ..., x_n\}$
2. Tenga en cuenta que las variables lineales libres deben conservarse bajo evaluación. Esto nos permite aprovechar la linealidad. Si no fuera una permutación de [ x 1 , . . . , x n ] , entonces implicaría que algunos x i se perdieron o duplicaron durante la evaluación, lo que no puede suceder.$[y_1, \ldots, y_m]$$[x_1, ..., x_n]$$x_i$

Pero, este tipo de teoremas se vuelven más interesantes cuando miramos un lenguaje con efectos y nuestra capacidad de probarlos para dichos lenguajes es tristemente limitada. Por ejemplo, considere el isomorfismo del Sistema F. En una configuración de llamada por valor, este isomorfismo se rompe cuando agregamos no terminación. Debemos ser capaces de recuperar un isomorfismo similares, sin embargo, con tipos lineales: tau ≅ ∀ A . ( Tau → A ) ⊸ A . Desafortunadamente, no tenemos relaciones lógicas operativas que puedan probar esto.$\tau \cong \forall A . (\tau \to A) \to A$$\tau \cong \forall A . (\tau \to A) \multimap A$

Dicho esto, también hay métodos sintácticos que pueden probar tanto este isomorfismo como su teorema. Este parece ser un enfoque particularmente útil en un entorno lineal, y es mucho menos una carga que establecer una relación lógica para probar teoremas simples.

Editar: Dado que usted pidió, he aquí un ejemplo de una prueba sintáctica de un teorema libre para el tipo en un entorno con un término ⊥ que se repite para siempre y está bien escrito en cualquier contexto en cualquier tipo. La idea es encontrar un conjunto de términos canónicos de un tipo y usarlo para determinar cuáles son los posibles valores de retorno para una función. Comenzamos con un teorema de solidez para términos bien escritos.$\forall A . (A \otimes A) \multimap A$$\bot$

$\Delta; \Gamma \vdash e : \tau$

• $e \approx v$$\Delta; \Gamma \vdash v : \tau$
• $e \approx n$$\Gamma$$\Delta; \Gamma \vdash n : \tau$
• $e \approx \bot$

$\approx$$\Delta$$x$

$\vdash f : \forall A . (A \otimes A) \multimap A$$f \approx \lambda x . e$$A; x : (A \otimes A) \vdash e : A$

• $e$$A; x : (A \otimes A) \vdash (v_1, v_2) : A$$v_1$$v_2$$A$$A$
• $e$$x$
• $e$$f$$\lambda x . \bot$

$e \approx\ \mathrm{let} (x_1, x_2) = x\ \mathrm{in}\ e’$$A; x_1 : A, x_2 : A \vdash e’ : A$$f \approx \lambda x . \mathrm{let }\ (x_1, x_2) = x\ \mathrm{ in }\ e’$$e’$$A$$e’ \approx x_i$

$\forall A . (A \otimes A) \multimap A$$\lambda x . \bot \approx \lambda x . \mathrm{let }\ (x_1, x_2) = x\ \mathrm{ in }\ \bot$

Solicitó una referencia para este tipo de prueba, pero no estoy seguro de una buena. Este tipo de razonamiento es bien conocido en ciertos círculos y se remonta quizás hasta Gentzen. Me dicen que recuerda a la búsqueda de pruebas enfocadas para el cálculo posterior, pero no sé exactamente cuál es la conexión.

Dicho esto, no conozco ningún trabajo publicado moderno que explique bien este método relativamente simple. Es cierto que es un poco limitado en su aplicabilidad a idiomas más simples. Por otro lado, creo que ha sido eclipsado por "Theorems for Free!" et al y, como resultado, incluso muchos investigadores senior piensan inmediatamente en relaciones lógicas cuando escuchan la frase "teorema libre", sin darse cuenta de que técnicas como esta pueden ser un enfoque alternativo más simple para tales pruebas (especialmente en el contexto de los sistemas de tipo lineal).

$A$$f$$\forall A. (\forall B. B \multimap (B, B)) \multimap [A] \multimap [A]$$\forall B. B \multimap (B, B)$ existe ya que tendría que duplicar su entrada.