A Hierarchy of Quantum Semantics

Several domains [1,4,12,16] can be used to define the semantics of quantum programs. Among them Abramsky [1] has introduced a semantics based on probabilistic power domains, whereas the one by Selinger [16] associates with every program a completely positive map. In this paper, we mainly introduce a semantical domain based on admissible transformations, i. e. multisets of linear operators. In order to establish a comparison with existing domains, we introduce a simple quantum imperative language (QIL), equipped with three different denotational semantics, called pure, observable, and admissible respectively. The pure semantics is a natural extension of probabilistic (classical) semantics and is similar to the semantics proposed by Abramsky [1]. The observable semantics, ` a la Selinger [16], associates with any program a superoperator over density matrices. Finally, we introduce an admissible semantics which associates with any program an admissible transformation. These semantics are not equivalent, but exact abstraction [7] or interpretation relations are established between them, leading to a hierarchy of quantum semantics.