Was ist Lineare Logik ?

?
Was ist Lineare Logik ?
Lineare Logik
• Keine alternative Logik
• Einführung neuer logischer
Verbindungen
Jean-Yves Girard
• Erweiterung der klass. Logik
?
Unterschied zur
klassischen Logik?
Aktionen vs. Situationen
Stabile Wahrheit der klassischen Logik:
Wenn A und A fi B, dann B
und A bleibt erhalten
Gut in Mathematik
Oft falsch in Realität
Aktionen vs. Situationen
Vorgang ändert die Bedingungen (Reaktion)
Implikation kann nicht beliebig oft wiederholt werden
Wenn A und A fi B, dann B
und A bleibt nicht zwangsläufig erhalten
Lineare Implikation
Aktionen vs. Situationen
A
Aktionen
B
Reaktion
nicht beliebig oft wiederholbar
Aktionen vs. Situationen
Situation
Aktion ist beliebig oft wiederholbar
Exponential
!A
Aktionen vs. Situationen
Übersetzung
Lineare Logik beinhaltet die klassische Logik
?
Verbindungen der
Linearen Logik ?
Konjunktionen & Disjunktionen
Zwei Konjunktionen:
(times)
& (with)
Zwei Disjunktionen:
(plus)
(par)
&
Konjunktionen
Aktionen
A
B
C
Konjunktionen
(times)
Beide Aktionen werden ausgeführt
&
ZU WENIG GELD !
Konjunktionen
und
Konjunktionen
& (with)
Man wählt, welche Aktion ausgeführt wird
oder
Disjunktionen
(plus)
Man kennt die Möglichkeiten,
darf aber nicht entscheiden
?
Disjunktionen
(par)
&
Man gibt , was man bekommt !
&
Lineare Negation
Dualitäten
&
Zustände & Übergänge
H2 und H2 und O2 impliziert H2O und H2O
Gilt auch für Hilberträume, Zustände
Contraction & Weakening
Klassische Eigenschaften
weakening
contraction
Schwierigkeiten in Lineare Logik !
?
Was ist Sequent Calculus ?
Linear Sequent Calculus
Syntax + Semantik zur Beweisanalyse
Sequenz
Bedeutung
A1 und ... und AN
impliziert
B1 oder ... oder BN
Linear Sequent Calculus
Regeln
weakening
contraction
exchange
?
Wie funktioniert Linearer
Sequent Calculus ?
Linear Sequent Calculus
Weakening in Linearer Logik
Weakening
Weakening
Lineare Logik
A,B sind beide realisiert
Linear Sequent Calculus
Contraction in Linearer Logik
weakening
weakening
contraction
Linear Sequent Calculus
Regeln für linearen Sequent Calculus
Identity
Cut
Permutation
Linear Sequent Calculus
times
with
par
true / false
Linear Sequent Calculus
Probleme mit cuts
Es kann bei Permutation von Regeln zu
Problemen mit Cuts kommen
Analogie
Vertauschbarkeit von
Operatoren in der QM
Cut Elimination
Theorem
Es gibt einen Algorithmus, der jeden Beweis der Sequenz G der
linearen Logik in einen cut-freien Beweis der gleichen Sequenz
umwandelt.
Ohne Theorem
Nur formales System
Keine Logik !
Sequent Calculus ohne Cut-Eliminiation
ist wie ein Auto ohne Motor !
?
Was sind Proof Structures ?
Proof Structures
Identity Links
Umgehen diverser Subtilitäten
Neuer Syntax
Axiom Link
A
A^
(Verschränktes Paar)
Cut Link
A
A^
(Bell-Messung)
Times Link
Par Link
&
Proof Structures
Kurzschlüsse
A
A^
Verboten !
Proof Structures
Beispiel
&
Proof Structures
Cut-Elimination für Proof Structures
Zusammenfassung
•Ressourcenintensive Logik
(QM ist ressourcenintensiv)
•Cut-Freiheit der Beweise
•Proof-Structure im Sinne einer Programmiersprache
interpretierbar
(physikalischer Prozess : Ausführung des Programms)

Download Report