Un marco semántico que interpreta la reducción de pruebas (eliminación de cortes) como un flujo dinámico o interacción de información, a menudo modelado por operadores, trazas o máquinas de fichas que siguen el movimiento de la información a través de una red de prueba.

Principio

Sustituir la reducción sintáctica estática por un proceso dinámico semántico donde caminos de interacción, composición de operadores o movimiento de fichas codifican el comportamiento computacional de las pruebas y ponen de manifiesto invariantes preservados por la eliminación de cortes.

Demostración

En pruebas de lógica lineal, representar los cortes como conexiones en una red de prueba y modelar la eliminación de cortes mediante fichas que recorren la red o componiendo operadores lineales cuya traza registra el flujo de información, caracterizando la normalización como dinámica de estilo matricial.

Aplicación incorrecta

Usar un modelo de interacción que ignore restricciones estructurales (por ejemplo no tener en cuenta la sensibilidad a recursos en lógica lineal) puede producir modelos que no reflejen la normalización proof-teórica y ofrezcan invariantes engañosos.

Consecuencia

Va más allá de las identidades sintácticas estáticas para ofrecer cuentas operacionales de la normalización, produce nuevos invariantes (fórmulas de ejecución, trazas), conecta con la teoría de operadores y modelos de máquinas, y sugiere implementaciones semánticas de la computación extraída de pruebas.

Inversión

La inversión es ver la eliminación de cortes puramente como reglas locales de reescritura sintáctica sin enfatizar el flujo dinámico global; tal visión pierde invariantes globales y conexiones con la semántica por operadores.

Límite

Se aplica mejor a sistemas con representaciones tipo circuito o red de pruebas (proof nets, grafos de interacción) y donde la dinámica pueda darse una semántica por operadores o fichas; es menos aplicable directamente a sistemas que carecen de una representación composicional adecuada.

Tensión semántica

Aparece tensión entre presentaciones algebraicas/por operadores que enfatizan propiedades espectrales o de traza y presentaciones combinatorias/de fichas que enfatizan el movimiento paso a paso; ambas capturan la interacción pero resaltan invariantes diferentes.

Síntesis

La Geometría de la Interacción reconceptualiza la eliminación de cortes como flujo de información: las pruebas se convierten en redes por las que se mueven y relacionan fichas u operadores, produciendo una semántica operacional que descubre invariantes dinámicos y unifica la reducción sintáctica con el comportamiento en teoría de operadores.