## [Geometría de la Interacción](/es/node/60976) Definición 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 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 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 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 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 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 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 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 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.