¿Los tipos recursivos MALL + sin restricciones son completos de Turing?

Si observa los combinadores recursivos en el cálculo lambda sin tipo, como el combinador Y o el combinador omega: Está claro que todos estos combinadores terminan duplicando una variable en algún lugar de su definición.

\begin{array}{lcl} ω & = & (λ X . X X) (λ X . X X) \\ Y & = & λ F . (λ X . F (X X)) (λ X . F (X X)) \end{array}

$\begin{array}{lcl} \omega & = & (\lambda x.\,x\;x)\;(\lambda x.\,x\;x)\\ Y & = & \lambda f.\,(\lambda x.\,f\;(x\;x))\; (\lambda x.\,f\;(x\;x)) \\ \end{array}$

Además, todos estos combinadores se pueden escribir en el cálculo lambda de tipo simple, si lo extiende con los tipos recursivos , donde se permite que ocurra negativamente en el tipo recursivo. $\mu\alpha.\,A(\alpha)$ $\alpha$

Sin embargo, ¿qué sucede si agrega tipos recursivos completos (de ocurrencia negativa) al fragmento exponencial libre de lógica lineal (es decir, MALL)?

¡Entonces no tienes una exponencial para contraerte. Puede codificar el tipo de exponenciales usando algo como pero no veo cómo definir la regla de introducción para ello, ya que parece requerir un combinador de punto fijo para definir. ¡Y estaba tratando de definir exponenciales, obtener contracción, obtener un combinador de punto fijo! $!A$

! UN ≜ μ α . yo Y UN Y (α \otimes α)

$!A \triangleq \mu\alpha.\;I \;\&\; A \;\&\; (\alpha \otimes \alpha)$

¿Es el caso de que MALL más tipos recursivos sin restricciones todavía se está normalizando?

lo.logic pl.programming-languages linear-logic Neel Krishnaswami
fuente

Estaba pensando en esto el otro día, y pasé unas horas jugando con algunas ideas, pero no pude encontrar una manera de expresar un valor recursivo ni convencerme de que no era posible. ¡Mi intuición es que no lo es! Sin embargo, no consideré la otra dirección, ¡si asumes la regla de introducción! y tipos recursivos, ¿eso le permite definir un combinador de punto fijo?

CA McCann

Siempre pensé que un -term en el que cada variable ocurre como máximo una vez es digitable en el fragmento simplemente tipado. Eso demostraría que no puede definir un combinador de punto fijo en el que las variables se usen linealmente.

λ

$\lambda$

Andrej Bauer

Creo que sólo ha contestado a la pregunta de MLL, pero los aditivos hacerlo permite a las variables pueden duplicar (linealidad implica entonces ocurrencias individuales en secuencias de reducción, más o menos).

A & B

$A & B$

Neel Krishnaswami

Respuestas:

Si se omiten las conmutaciones aditivas en MALL, es fácil demostrar que el tamaño de una prueba disminuye con cada paso de eliminación de corte. Si se permiten conmutaciones aditivas, la prueba no es tan fácil, pero se proporcionó en el documento original de "Lógica lineal". Se llama Teorema de normalización pequeña (Corolario 4.22, p71), que dice que mientras la regla contracción-promoción no esté involucrada (que es el caso en MALL) la normalización se mantiene. El argumento no se basa en fórmulas en sí mismas, podrían ser infinitas (por ejemplo, definidas recursivamente).

Significa que no es posible codificar una promoción para el tipo en MALL, ya que permitiría los combinadores de punto fijo. Se necesitaría una construcción de recursión adicional para eso. $\mu\alpha.\;I \;\&\; A \;\&\; (\alpha \otimes \alpha)$

Nota: ¡Creo que es posible usar MALL junto con un principio de coinducción (introducción de 's dual) para mantener el sistema normalizándose y obtener una promoción para esta codificación . Permitir tipos recursivos en MALL + coinducción haría que Turing se completara. Pero mientras MALL se considere solo, permitir tipos recursivos no es un gran problema. $\mu$ $!A$

Stéphane Gimenez
fuente

Observe también que el tipo sugerido se menciona brevemente en la página 101 (última página) del documento.

Stéphane Gimenez