Ein semantischer Rahmen, der Beweisreduktion (Cut-Elimination) als dynamischen Fluss oder Interaktion von Information interpretiert, oft modelliert durch Operatoren, Spuren oder Tokenmaschinen, die die Bewegung von Information durch ein Beweisnetz verfolgen.

Prinzip

Statische syntaktische Reduktion durch einen semantischen dynamischen Prozess ersetzen, bei dem Interaktionspfade, Operatorzusammensetzung oder Token-Bewegung das rechnerische Verhalten von Beweisen kodieren und Invarianten der Cut-Elimination hervorheben.

Demonstration

In Beweisen der linearen Logik werden Schnitte als Verbindungen in einem Proof-Net dargestellt und Cut-Elimination modelliert durch Token, die das Netz durchlaufen, oder durch die Komposition linearer Operatoren, deren Spur den Informationsfluss aufzeichnet und Normalisierung als matrixartige Dynamik charakterisiert.

Fehlanwendung

Ein Interaktionsmodell zu verwenden, das strukturelle Einschränkungen ignoriert (z. B. Ressourcensensitivität der linearen Logik nicht berücksichtigen), kann Modelle erzeugen, die die beweistheoretische Normalisierung nicht widerspiegeln und irreführende Invarianten liefern.

Konsequenz

Geht über statische Beweisidentitäten hinaus, liefert operationale Beschreibungen der Normalisierung, erzeugt neue Invarianten (Ausführungsformeln, Spuren), verbindet mit Operatorentheorie und Maschinenmodellen und schlägt semantische Implementierungen von aus Beweisen gewonnener Berechnung vor.

Umkehrung

Die Umkehrung ist die Betrachtung der Cut-Elimination rein als syntaktische, lokale Umschrreibungsregeln ohne Betonung des globalen dynamischen Flusses; diese Sicht verpasst globale Invarianten und Verbindungen zur Operatorensemantik.

Abgrenzung

Am besten anwendbar auf Systeme mit schaltkreis- oder netzartigen Repräsentationen von Beweisen (Proof-Nets, Interaktionsgraphen) und wenn Dynamik durch Operator- oder Tokensemantik gegeben werden kann; weniger direkt anwendbar auf Systeme ohne geeignete kompositionelle Repräsentation.

Semantische Spannung

Es besteht Spannung zwischen algebraischen/Operator-Präsentationen, die spektrale oder Spur-Eigenschaften betonen, und kombinatorischen/Token-Präsentationen, die schrittweisen Bewegungsablauf hervorheben; beide erfassen Interaktion, aber betonen unterschiedliche Invarianten.

Synthese

Die Geometrie der Interaktion stellt Cut-Elimination als Informationsfluss dar: Beweise werden zu Netzen, durch die Token oder Operatoren wandern und interagieren, was eine operationale Semantik erzeugt, die dynamische Invarianten offenlegt und syntaktische Reduktion mit operatorentheoretischem Verhalten vereint.