Predicatet transformers for nondeterministic quantum programs

Abstract

Nondeterminism has been introduced into quantum programming languages to model, for example, unspecified behavior. Weakest precondition transformers provide a formal framework for reasoning about program correctness with respect to a given postcondition. This thesis combines these ideas by introducing demonic and angelic interpretations of nondeterminism for quantum programs, together with corresponding weakest liberal precondition transformers. To capture angelic nondeterminism in a qualitative setting, we introduce predicates represented by sets of subspaces, where each subspace is represented by a projection. Such a predicate is satisfied whenever the quantum state belongs to one of the represented subspaces. We show, however, that natural definitions of the weakest liberal precondition transformer based on these predicates do not behave as desired for measurements and loops in the demonic setting. For this reason, the demonic weakest liberal precondition transformer is restricted to singleton postconditions. We further investigate the corresponding non-liberal weakest precondition transformers using termination spaces. This yields transformer rules for all language constructs except loops, for which deriving a transformer rule remains an open problem. Finally, we show that the resulting weakest precondition variants have the same relations as in the classical case.