En su respuesta a esta pregunta , Stephane Giménez me señaló un algoritmo de normalización de tiempo polinómico para pruebas en lógica lineal. La prueba en el documento de Girard utiliza redes de prueba, que son un aspecto de la lógica lineal que realmente no conozco mucho.
Ahora, he tratado de leer documentos sobre redes de prueba antes (como las notas de Pierre-Louis Curien sobre ellos), pero realmente no los he entendido. Entonces mi pregunta es: ¿cómo debo pensar en ellos? Por "cómo pensar en ellos", me refiero tanto a la intuición informal detrás de ellos (por ejemplo, cómo se comportan computacionalmente o cómo se relacionan con las secuenciantes), y también qué teoremas sobre ellos debo probar para que realmente los entienda.
Al responder a esta pregunta, puede suponer (1) Conozco bien la teoría de la prueba de la lógica lineal (incluidas cosas como cómo funciona la prueba de eliminación de cortes y también en forma focalizada), (2) su semántica categórica en términos de espacios de coherencia o por convolución diaria, y (3) los rudimentos muy básicos de la construcción de GoI.
fuente
Respuestas:
Las redes de prueba son interesantes esencialmente por tres razones:
1) IDENTIDAD DE PRUEBAS. Proporcionan una respuesta al problema "¿Cuándo son dos pruebas iguales"? En el cálculo secuencial puede tener muchas pruebas diferentes de la misma proposición que difieren solo porque el cálculo secuencial impone un orden entre las reglas de deducción, incluso cuando esto no es necesario. Por supuesto, se puede agregar una relación de equivalencia en las pruebas de cálculo posteriores, pero luego se debe demostrar que la eliminación de cortes se comporta correctamente en las clases de equivalencia, y también es necesario recurrir al módulo de reescritura, que es bastante más técnico que la reescritura simple. Las redes de prueba resuelven el problema de tratar con clases de equivalencia al proporcionar una sintaxis donde cada clase de equivalencia se contrae en un solo objeto. De todos modos, esta situación es un poco idealista, ya que por muchas razones las redes de prueba a menudo se extienden con alguna forma de equivalencia.
2) NO HAY PASOS COMUNITARIOS DE ELIMINACIÓN DE CORTE. La eliminación de cortes en las redes de prueba adquiere un sabor bastante diferente al de los cálculos posteriores porque los pasos conmutativos de eliminación de cortes desaparecen. La razón es que en las redes de prueba las reglas de deducción están conectadas solo por su relación causal. Los casos conmutativos se generan por el hecho de que una regla puede estar oculta por otra regla causalmente no relacionada. Esto no puede suceder en redes de prueba, donde las reglas causalmente no relacionadas están muy separadas. Dado que la mayoría de los casos de eliminación de cortes son conmutativos, se obtiene una sorprendente simplificación de la eliminación de cortes. Esto ha sido particularmente útil para estudiar cálculos lambda con sustituciones explícitas (porque exponenciales = sustituciones explícitas). Nuevamente, esta situación se idealiza ya que algunas presentaciones de redes de prueba requieren pasos conmutativos. Sin embargo,
3) CRITERIOS DE CORRECCIÓN. Las redes de prueba se pueden definir mediante la traducción de pruebas de cálculo posteriores, pero por lo general no se acepta un sistema de redes de prueba como tal a menos que se proporcione un criterio de corrección, es decir, un conjunto de principios teóricos de grafos que caracterizan el conjunto de gráficos obtenidos al traducir un prueba de cálculo posterior. La razón por la cual se requiere un criterio de corrección es que el lenguaje gráfico libre generado por el conjunto de constructores de red de prueba (llamados enlaces) contiene "demasiados gráficos", en el sentido de que algunos gráficos no corresponden a ninguna prueba. La relevancia del enfoque de criterios de corrección generalmente se malinterpreta por completo. Es importante porque proporciona definiciones no inductivas de lo que es una prueba, y ofrece perspectivas sorprendentemente diferentes sobre la naturaleza de las deducciones. El hecho de que la caracterización no sea inductiva generalmente se critica, mientras que es exactamente lo que es interesante. Por supuesto, no es fácilmente susceptible de formalización, pero, una vez más, esta es su fortaleza: las redes de prueba proporcionan ideas que no están disponibles a través de la perspectiva inductiva habitual de las pruebas y los términos. Un teorema fundamental para las redes de prueba es el teorema de secuenciación, que dice que cualquier gráfico que satisfaga el criterio de corrección puede descomponerse inductivamente como una prueba de cálculo secuencial (traduciéndose de nuevo al gráfico correcto).
Permítanme concluir que no es preciso decir que las redes de prueba son una versión clásica y lineal de la deducción natural. El punto es que resuelven (o intentan resolver) el problema de la identidad de las pruebas y que la deducción natural resuelve con éxito el mismo problema para una lógica intuicionista mínima. Pero las redes de prueba se pueden hacer también para sistemas intuicionistas y para sistemas no lineales. En realidad, funcionan mejor para los sistemas intuicionistas que para los sistemas clásicos.
fuente
Girard notó que la deducción natural es asimétrica exactamente de esta manera. Es por eso que coincide con la lógica intuicionista. Las redes de prueba representan un intento de Girard de inventar una forma simétrica de deducción natural.
Algo que me perdí en mi respuesta original: las redes de prueba son una forma de escribir pruebas, y sabemos que las pruebas son programas. Por lo tanto, las redes de prueba también son una forma de escribir programas.
La notación funcional tradicional para escribir programas es asimétrica, al igual que la deducción natural. Por lo tanto, las redes de prueba apuntan a una forma de escribir programas de forma simétrica . Así es como los cálculos de proceso entran en escena.
Otra forma de representar la simetría es a través de la programación lógica, que he explorado en dos documentos: una base escrita para programas de lógica direccional y aspectos de orden superior de la programación lógica.
fuente
Me concentro en cómo las redes de prueba están relacionadas con el cálculo posterior, dejando cosas más dinámicas.
Redes de prueba pruebas de cálculo secuenciales abstractas: una red de pruebas representa un conjunto de pruebas de cálculo secuenciales. Las redes de prueba olvidan las diferencias sin importancia entre las pruebas de cálculo posteriores (como qué fórmula se descompone debajo de cuál). El teorema importante aquí es la "secuenciación", que convierte una red de prueba en una prueba de cálculo secuencial.
fuente
Esto se relaciona principalmente con la parte de "cómo se comportan computacionalmente" de su pregunta. Una forma de comprender bien las redes de prueba desde la perspectiva computacional es observar interpretaciones ligeramente más concretas (por ejemplo, proceso algebraico).
Quizás te interese lo siguiente:
El artículo de Abramsky (la sección CLL sobre expresiones de prueba): Interpretaciones computacionales de lógica lineal . Este documento también presenta algunos resultados que están cerca de los correspondientes para redes de prueba, por lo que podría ayudar en el segundo aspecto de su pregunta.
El documento de Honda y Laurent que muestra cómo un tipo específico de Redes de Prueba, llamadas Redes de Prueba Polarizadas, corresponde a los procesos de cálculo Pi, y que Martin Berger menciona anteriormente: Una correspondencia exacta entre un cálculo pi tipificado y una prueba polarizada. redes
(aquí anuncio sin vergüenza mi propio trabajo) El borrador: Redes de prueba en forma algebraica de proceso
También hay algunos trabajos relacionados con redes de prueba y cálculo lambda, que también dan intuiciones sustanciales. Por ejemplo, lo siguiente de Delia Kesner y Stéphane Lengrand:
También le puede interesar este tipo de trabajo (muy orientado a aspectos teóricos) que se basa en Estructuras de Prueba para probar en detalle la propiedad de Normalización Fuerte de LL, por Michele Pagani y Lorenzo Tortora de Falco.
En general, ¿qué teoremas debería uno estudiar? Bueno, no soy una autoridad, pero es posible que desee ver la "secuenciación" (relacionando las redes de prueba y las pruebas secuenciales; vea el documento original de TCS sobre LL) y la fuerte prueba de normalización (bastante involucrada, como se esperaba, pero muchas importantes Los teoremas de PN están relacionados con él [o, usado para probarlo]).
Si está familiarizado con el enfoque, también le puede interesar este artículo de Andreoli:
Espero que esto ayude. Una vez más, estas referencias son realmente no exhaustivas.
mejor, Dimitris
fuente
Recientemente ha habido un trabajo interesante para hacer que la relación entre la red de prueba y los cálculos enfocados sea más estricta, utilizando variantes "multi-enfocadas" donde puede tener varios agujeros izquierdos simultáneos, y estudiando pruebas "enfocadas al máximo". Si elige el cálculo correctamente, las pruebas centradas al máximo pueden corresponder a las redes a prueba de MLL o, en lógica clásica, a las pruebas de expansión ( El isomorfismo entre pruebas de expansión y pruebas secuenciales de enfoque múltiple, Kaustuv Chaudhuri, Stefan Hetzl y Dale Miller, 2013)
fuente
Puede consultar mi artículo " Una encuesta de redes de prueba y matrices para lógicas subestructurales ".
Abstracto:
fuente