¿Puede el cálculo lambda afín resolver todos los problemas en P?

En Temas avanzados en tipos y lenguajes de programación se menciona, en el capítulo sobre sistemas de tipos subestructurales, que un cálculo lambda afín "cuidadosamente elaborado" con un combinador de recursión para listas solo puede escribir términos que tienen tiempo de ejecución polinómico (no presentar la prueba debido a la complejidad). Esto sería muy interesante si también pudiéramos resolver todos los problemas en P. Podría intentar encontrar una solución a un problema P-completo utilizando el cálculo presentado por No estoy seguro de que esto realmente pruebe algo. No me parece que signifique que puede preformar todas las reducciones necesarias para usar una solución a un problema P-completo (aunque ciertamente parece probable).

Si no se sabe que un cálculo lambda afín pueda resolver exactamente los problemas en P, ¿hay algún cálculo conocido que pueda resolver exactamente los problemas en P?

Editar: ¡ mi suposición en el primer párrafo a continuación es incorrecta! Ugo Dal Lago me señaló un artículo posterior de Martin Hofmann (aparecido en POPL 2002), del cual no estaba al tanto, mostrando (como corolario de resultados más generales) que el sistema del libro ATTPL está completo para ( a pesar de no poder calcular todas las funciones en F P ). Entonces, para mi sorpresa, la respuesta a la pregunta principal es sí.$\mathsf P$$\mathsf{FP}$

En cuanto al sistema que usted se refiere (del libro ATTPL), estoy bastante seguro de que no puede decidir en todos los idiomas . Ciertamente no puede calcular todas las funciones en F P : como se menciona en las notas de ese capítulo, ese sistema está tomado del documento LICS 1999 de Martin Hofmann ("Tipos lineales y cálculo de tiempo polinomial sin aumento de tamaño"), en el que se muestra que las funciones representables son polytime y no aumentan el tamaño$\mathsf P$$\mathsf{FP}$, que excluye muchas funciones polytime. También parece dar una seria limitación al tamaño de la cinta de las máquinas de Turing que puede simular en ese idioma. En el documento, Hofmann muestra que puede codificar el cálculo del espacio lineal; Supongo que no podrá hacer mucho más, es decir , la clase correspondiente a ese sistema es, aproximadamente, los problemas que se pueden resolver simultáneamente en polytime y en el espacio lineal.

En cuanto a su segunda pregunta, hay varios -calculi que puede resolver exactamente los problemas en P . Algunos de ellos se mencionan en las notas del capítulo ATTPL al que se refiere (Sección 1.6): cálculo λ escalonado de Leivant (vea su documento POPL 1993, o el documento con Jean-Yves Marion "Caracterizaciones de cálculo Lambda de Poly-Time" ", Fundamenta Informaticae 19 (1/2): 167-184, 1993), que se relaciona con la caracterización de Bellantoni y Cook de F P ; y los cálculos λ derivados de la lógica lineal ligera de Girard ( Information and Computation , 143: 175–204, 1998) o de la lógica lineal suave de Lafont ( Theoretical Computer Science$\lambda$$\mathsf P$$\lambda$$\mathsf{FP}$$\lambda$318 (1-2): 163-180, 2004). Los sistemas de tipos que surgen de estos dos últimos sistemas lógicos y que aseguran la terminación de polytime (sin dejar de ser completa) se pueden encontrar en:

Patrick Baillot, Kazushige Terui. Tipos de luz para el cálculo del tiempo polinómico en cálculo lambda. Información y cálculo 207 (1): 41-62, 2009.

Marco Gaboardi, Simona Ronchi Della Rocca. De lógicas ligeras a tareas de tipo: un estudio de caso. Diario lógico de la IGPL 17 (5): 499-530, 2009.

Encontrarás muchas otras referencias en esos dos documentos.

Para concluir, permítanme ampliar el comentario de Neel Krishnaswami. La situación es un poco sutil. Todos los cálculos de anteriores pueden verse como restricciones de cálculos más generales, en los que puede calcular mucho más que las funciones de polytime, por ejemplo, el sistema F. En otras palabras, define una propiedad Φ de los programas del sistema F P : string → bool tal que:$\lambda$$\Phi$$P:\texttt{string}\rightarrow\texttt{bool}$

solidez: implica que el lenguaje decidido por P está en P ;$\Phi(P)$$P$$\mathsf P$

integridad: para cada , hay un programa del sistema F P que decide L tal que Φ ( P ) .$L\in\mathsf P$$P$$L$$\Phi(P)$

El interés es que la propiedad expresada por es puramente sintáctica y, en particular, decidible. Por lo tanto, la integridad solo puede mantenerse en un sentido extensional: si L es su lenguaje favorito en P y si P es su algoritmo favorito para decidir L expresado en el sistema F, puede ser que Φ ( P ) no se mantenga. Todo lo que sabes es que hay algún otro programa del sistema F P 'que decide L y tal que Φ ( P ' ) se cumple. Desafortunadamente, puede suceder que P $\Phi$$L$$\mathsf P$$P$$L$$\Phi(P)$$P'$$L$$\Phi(P')$$P'$es mucho más que su ideado . De hecho, la integridad se prueba codificando máquinas de Turing polinomialmente sincronizadas como términos del sistema F que satisfacen Φ . Por lo tanto, la única forma garantizada de resolver L usando su algoritmo favorito es implementar ese algoritmo en una máquina de Turing y luego traducirlo en el sistema F usando la codificación dada en la prueba de integridad (¡su propia codificación puede no funcionar!). No es exactamente la solución más elegante en términos de programación ... Por supuesto, en muchos casos el programa "natural" P satisface Φ . Sin embargo, en muchos otros casos no lo hace: en el artículo de LICS 1999 mencionado anteriormente, Hofmann da el tipo de inserción como ejemplo.$P$$\Phi$$L$$P$$\Phi$

Existen sistemas de tipos intencionalmente completos , que pueden escribir exactamente los programas de polytime del lenguaje más amplio (sistema F en mi ejemplo anterior). Por supuesto, son indecidibles en general. Ver

Ugo Dal Lago, Marco Gaboardi. Tipos dependientes lineales y completitud relativa. Métodos lógicos en informática 8 (4), 2011.