A formal language for expressing quantum predicates

Dural, Umut Yigit; Gehnen, Christina; Katoen, Joost-Pieter; Unruh, Dominique

doi:10.18154/RWTH-2026-06832

A formal language for expressing quantum predicates

Dural, Umut Yigit

2026

VerantwortlichkeitsangabeUmut Yiğit Dural

ImpressumAachen : RWTH Aachen University 2026

Umfang1 Online-Ressource : Illustrationen

Masterarbeit, RWTH Aachen University, 2025

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2026

Genehmigende Fakultät
Fak09

Hauptberichter/Gutachter
Unruh, Dominique (Thesis advisor)^RWTH* ; Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Gehnen, Christina (Consultant)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2025-11-20

Online
DOI: 10.18154/RWTH-2026-06832
URL: https://publications.rwth-aachen.de/record/1038900/files/1038900.pdf

Einrichtungen

Lehrstuhl für Quanteninformationssysteme (Informatik 15) (125910)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
We develop a formal language, a syntax, for specifying quantum predicates, which are yes/no properties of quantum systems. Specifically we study classical-quantum predicates using projector-based Birkhoff-von Neumann quantum logic. We give an extensional definition of a weakest precondition calculus that preserves projector-based predicates fora simple loop-free classical-quantum programming language. We prove that our weakest precondition calculus is relatively complete in the sense of Cook for the classical-quantum programming language we specify. To achieve this, we show that for any post condition expressible in our formal language, the corresponding weakest precondition with respect to any program is also expressible in our formal language. This result establishes a foundation for reasoning about classical-quantum programs using an intensional approach.

OpenAccess:
PDF