Lúdicos

En la teoría de la demostración , la ludica es un análisis de los principios que rigen las reglas de inferencia de la lógica matemática . Las características clave de la ludica incluyen la noción de conectores compuestos, el uso de una técnica conocida como enfoque o focalización (inventada por el científico informático Jean-Marc Andreoli ) y el uso de ubicaciones o loci sobre una base en lugar de proposiciones .

Más precisamente, la ludica intenta recuperar conectores lógicos conocidos y comportamientos de prueba siguiendo el paradigma de la computación interactiva, de forma similar a como se hace en la semántica de juegos, con la que guarda estrecha relación. Al abstraer la noción de fórmulas y centrarse en sus usos concretos —es decir, en ocurrencias distintas—, proporciona una sintaxis abstracta para la informática , ya que los loci pueden considerarse punteros en la memoria.

El principal logro de la ludística es el descubrimiento de una relación entre dos nociones naturales, pero distintas, de tipo o proposición.

La primera perspectiva, que podría denominarse interpretación de las proposiciones desde el punto de vista de la teoría de la demostración o al estilo de Gentzen , sostiene que el significado de una proposición surge de sus reglas de introducción y eliminación. La focalización refina este punto de vista al distinguir entre proposiciones positivas, cuyo significado surge de sus reglas de introducción, y proposiciones negativas, cuyo significado surge de sus reglas de eliminación. En los cálculos focalizados, es posible definir conectores positivos proporcionando únicamente sus reglas de introducción, y la forma de las reglas de eliminación viene determinada por esta elección. (Simétricamente, los conectores negativos pueden definirse en los cálculos focalizados proporcionando únicamente las reglas de eliminación, y las reglas de introducción vienen determinadas por esta elección).

La segunda perspectiva, que podría denominarse interpretación computacional o de Brouwer-Heyting-Kolmogorov de las proposiciones, parte de la idea de que primero se establece un sistema computacional y luego se les da una interpretación de realizabilidad a las proposiciones para dotarlas de contenido constructivo. Por ejemplo, un realizador para la proposición "A implica B" es una función computable que toma un realizador para A y lo utiliza para calcular un realizador para B. Los modelos de realizabilidad caracterizan los realizadores de las proposiciones en términos de su comportamiento visible, y no en términos de su estructura interna.

Girard demuestra que, para la lógica lineal afín de segundo orden , dado un sistema computacional con no terminación y paradas por error como efectos, la realizabilidad y la focalización dan el mismo significado a los tipos.

La ludica fue propuesta por el lógico Jean-Yves Girard . Su artículo introductorio, Locus solum: de las reglas de la lógica a la lógica de las reglas , presenta algunas características que podrían considerarse excéntricas para una publicación de lógica matemática (como las ilustraciones de mofetas). El propósito de estas características es reforzar el punto de vista de Jean-Yves Girard en el momento de su redacción. De este modo, ofrece a los lectores la posibilidad de comprender la ludica independientemente de sus conocimientos previos.

1. Girard, J.-Y., Locus solum : de las reglas de la lógica a la lógica de las reglas (.pdf), Estructuras matemáticas en informática , 11, 301 – 506, 2001.
2. Grupo de lectura de Girard en la Universidad Carnegie Mellon (una wiki sobre Locus Solum)