IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation

Dieses Kapitel führt eine Beweissprache für die intuitionistische multiplikative additive lineare Logik (IMALL) ein, die um eine Modalität erweitert wird, die den Übergang von reinen zu gemischten Zuständen in der Quantenberechnung erfasst. Die Forschung definiert die Logik - IMALL, indem IMALL auf transparente Weise um eine Modalität erweitert wird, die sowohl reine als auch gemischte Berechnungen innerhalb eines einheitlichen logischen Rahmens unterstützt. Die Proof Language bietet drei wesentliche Vorteile gegenüber typischen Quantenlambda-Kalkulationen: Sie ermöglicht eine reichere linear-algebraische Struktur, erlaubt den Ausdruck echter Quantenkontrollflüsse und verzichtet auf die Notwendigkeit einer externen globalen Konfiguration. Das Kapitel stellt auch ein denotationales Modell vor, das von früheren Arbeiten inspiriert wurde, das das Design der Sprache validiert und ein Angemessenheitstheorem unterstützt. Darüber hinaus wird die Ausdruckskraft der Sprache anhand von Beispielen wie Quantenteleportation und Quantenschalter demonstriert, was ihre Fähigkeit unterstreicht, paradigmatische Quantenphänomene auf natürliche Weise zu erfassen. Die Struktur des Aufsatzes umfasst Abschnitte über Syntax, Ableitungsregeln, Cut-Eliminierung, kategorisches Modell, denotationale Semantik und Kodierung von Quantencomputern und bietet einen umfassenden Überblick über die neue Beweissprache und ihre Anwendungen in der Quantenberechnung.