An Algebra of Quantum Programs with the Kleene
Star Operator
Tsubasa Takagi1,2
1
    Japan Advanced Institute of Science and Technology, Nomi, Japan
2
    Research Fellow of Japan Society for the Promotion of Science


                                         Abstract
                                         Dynamic Algebra is an algebra that extends the expressive power of Hoare logic and has been used
                                         in formal verification of programs. However, quantum programs (programs executed by a quantum
                                         computer) behave differently from classical programs. Therefore, it is natural to extend dynamic algebra
                                         based on classical logic (Boolean lattice) to quantum dynamic algebra based on quantum logic (complete
                                         orthomodular lattice). Nevertheless, quantum dynamical algebra has not been formulated to date because
                                         of the difficulty in dealing with repeated execution of quantum programs, which the Kleene star operator
                                         represents. In this paper, we formulate an algebra of quantum programs with the Kleene star operator by
                                         using an algebraic specification that directly represents the iteration of quantum programs. In addition,
                                         we discuss how to construct the algebra from a transition system representing program execution.

                                         Keywords
                                         Quantum Program, Dynamic Algebra, Orthomodular Lattice, Kripke Frame




1. Introduction
Dynamic Quantum Logic (DQL) [1] is a logic for formal verification of quantum programs.
Specifically, some quantum protocols, such as Quantum Teleportation [2], Quantum Secret
Sharing [2], Quantum Search Algorithm [3], the quantum leader election protocol [3, 4], and
the BB84 quantum key distribution protocol [4] have been verified by using DQL (see also [5]).
DQL is a dynamical extension of the traditional quantum logic [6], and is based on the idea of
propositional dynamic logic (PDL) [7]. By incorporating program constructs 𝑎; 𝑏 (composition),
𝑎 ∪ 𝑏 (non-deterministic choice), 𝑝? (quantum test) into quantum logic as a modal logic, DQL
makes it possible to deal with quantum programs.
   However, the previous studies of DQL have not discussed the Kleene star operator (iteration)
of a quantum program. This is because it was not necessary to use the Kleene star operator to
construct a prototype of DQL in the earlier stage. Baltag and Smets, the initiators of DQL, stated
that “Notice that we did not include iteration (Kleene star) among our program constructs: this
is only because we do not need it for any of the applications in this paper” in [2]. It does not
mean that it is not worth adding the Kleene star operator to DQL. Using the Kleene star operator
is necessary to deal with quantum while loops. For example, quantum while loops are used

International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols 2022
Envelope-Open tsubasa@jaist.ac.jp (T. Takagi)
Orcid 0000-0001-9890-1015 (T. Takagi)
                                       © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073
                                       CEUR Workshop Proceedings (CEUR-WS.org)




                                                                                                           2
in the quantum walk algorithm [8] for repeatedly choosing quantum programs corresponding
to “Left” or “Right.” Moreover, it is significant to discuss the Kleene star operator of quantum
programs for connecting DQL to a considerable amount of previous research on finite quantum
automata (see [9] for example).
   In this paper, we define an algebra of regular quantum programs with the Kleene star operator
and call it quantum dynamic algebra (QD-algebra). The algebra is constructed by combining
the algebra of quantum mechanics (called complete orthomodular lattice) with dynamic algebra
[10].
   QD-algebra is used for giving algebraic semantics to DQL. However, algebraic semantics is
not suited to express a state transition system (in that transitions represent program execution)
in general because algebra merely defines various conditions, and the notion of states does not
appear explicitly. To overcome this problem, we propose a specific QD-algebra that is associated
with a state transition system called a QD-frame (Definition 4.3) and call it a characteristic
algebra (Definition 5.5). Characteristic algebra gives relational semantics (namely, Kripke
semantics) to DQL.


2. Preliminaries
Various algebras for quantum mechanics have already been well studied since 1936 [6]. The
starting point for the study of algebra for quantum mechanics is a complete orthomodular
lattice that characterizes the lattice of all closed subspaces of a Hilbert space (Theorem 2.3). For
more details, see [11].

Definition 2.1. A lattice (𝑃, ⪯) is a poset that a two-element set {𝑝, 𝑞} has the infimum (greatest
lower bound) 𝑝 ∧ 𝑞 and supremum (least upper bound) 𝑝 ∨ 𝑞 for any 𝑝, 𝑞 ∈ 𝑃. A lattice (𝑃, ⪯) is
said to be complete if each subset Γ of 𝑃 has the infimum ⋀ Γ and supremum ⋁ Γ.

  In the sequel, the least element ⋀ 𝑃 and greatest element ⋁ 𝑃 in a complete lattice (𝑃, ⪯) are
denoted as ⋏ and ⋎, respectively.

Definition 2.2. A complete ortholattice is a triple (𝑃, ⪯, ¬) that consists of a complete lattice
(𝑃, ⪯) and function ¬ ∶ 𝑃 → 𝑃 such that
  (1) 𝑝 ∧ ¬𝑝 = ⋏, 𝑝 ∨ ¬𝑝 = ⋎,
  (2) ¬¬𝑝 = 𝑝, and
  (3) 𝑝 ⪯ 𝑞 implies 𝑞 ⪯ 𝑝,
for any 𝑝, 𝑞 ∈ 𝑃. A complete orthomodular is a complete ortholattice satisfying the orthomodular
law
  (4) 𝑝 ∧ (¬𝑝 ∨ (𝑝 ∧ 𝑞)) ⪯ 𝑞.

  Many equivalent definitions of the orthomodular law are known [12, Lemma 19]. One of
them is that 𝑝 ⪯ 𝑞 implies 𝑞 = 𝑝 ∨ (¬𝑝 ∧ 𝑞).




                                                 3
Example 2.1 (Powerset Lattice). Let ℘(𝑆) be the powerset of a set 𝑆. Then, (℘(𝑆), ⊆, 𝑐 ) is a
complete orthomodular lattice and is called the powerset lattice of 𝑆, where 𝑐 denotes the set
complementation in 𝑆. A powerset lattice is complete because ⋀ Γ = ⋂𝑝∈Γ 𝑝 and ⋁ Γ = ⋃𝑝∈Γ 𝑝
exist for each Γ ⊆ ℘(𝑆). Hereafter, we shall use the symbols ⋂ Γ and ⋃ Γ for the infimum and
supremum of a set Γ in a powerset lattice, respectively.
Example 2.2 (Hilbert Lattice). Let ℋ be a Hilbert space, and C(ℋ ) be the set of all closed
subspaces of ℋ. Then, (C(ℋ ), ⊆, ⟂ ) is a complete orthomodular lattice [11, Proposition 4.5] and
is called a Hilbert lattice. Here, for each 𝑉 ∈ C(ℋ ), 𝑉 ⟂ is defined as the orthogonal complement

                                 {𝑤 ∈ ℋ ∶ 𝑤 ⟂ 𝑣 for any 𝑣 ∈ 𝑉 }

of 𝑉, where ⟂ denotes the orthogonality relation on ℋ. An orthogonal complement of a closed
subspace is always a closed subspace. A Hilbert lattice is complete because ⋀ Γ = ⋂ Γ and

                                ⋁ Γ = ⋂{𝑉 ∈ C(ℋ ) ∶ ⋃ Γ ⊆ 𝑉 }

exist for each Γ ⊆ C(ℋ ). It is known that ⋁ Γ = ((⋃ Γ)⟂ )⟂ .
  Note that the least element ⋀ C(ℋ ) is the singleton {0} of the zero vector (origin) 0, and the
greatest element ⋁ C(ℋ ) is ℋ. The supremum 𝑉 ∨ 𝑊 of {𝑉 , 𝑊 } ⊆ C(ℋ ) is the closed subspace
𝑉 + 𝑊 generated by
                                𝑉 + 𝑊 ∶= {𝑣 + 𝑤 ∶ 𝑣 ∈ 𝑉 , 𝑤 ∈ 𝑊 }.
  The following theorem states that the orthomodularity characterizes Hilbert spaces among
inner product spaces.

Theorem 2.3 (The Amemiya-Araki Theorem [13]). Let 𝑋 be an inner product space. The triple
(C(𝑋 ), ⊆, ⟂ ) is a complete orthomodular lattice if and only if 𝑋 is a Hilbert space, where C(𝑋 )
stands for the set of all subspaces of 𝑋 satisfying (𝑋 ⟂ )⟂ = 𝑋.

Definition 2.4. A complete orthomodular lattice (𝑃, ⪯, ¬) is called a complete Boolean lattice
if (𝑃, ⪯) is distributive. That is, the distributive law

                                   𝑝 ∧ (𝑞 ∨ 𝑟) = (𝑝 ∧ 𝑞) ∨ (𝑝 ∧ 𝑟)

holds for any 𝑝, 𝑞, 𝑟 ∈ 𝑃.

  For example, a powerset lattice is a complete Boolean lattice, but a Hilbert lattice is not. In
fact, a counter-example to the distributive law in a Hilbert lattice is as follows: let 𝑉 , 𝑊 be
one-dimensional subspaces of ℋ, and 𝑈 be a one-dimensional subspace of 𝑉 + 𝑊, then

                                     𝑈 ∩ (𝑉 + 𝑊 ) = 𝑈 ≠ {0}

but
                              (𝑈 ∩ 𝑉 ) + (𝑈 ∩ 𝑊 ) = {0} + {0} = {0}.

Definition 2.5. A non-empty subset 𝑄 of 𝑃 is called a sublattice of a lattice (𝑃, ⪯) if 𝑝∧𝑞, 𝑝∨𝑞 ∈ 𝑄
for any 𝑝, 𝑞 ∈ 𝑄.




                                                 4
  Let Sub(𝒫 ) be the set of all sublattices of a lattice 𝒫 = (𝑃, ⪯), and ⟨𝑋 ⟩ be the set

                                    ⋂{𝑄 ∈ Sub(𝒫 ) ∶ 𝑋 ⊆ 𝑄}

for each non-empty set 𝑋. Then, ⟨𝑋 ⟩ is the smallest sublattice of 𝒫 containing 𝑋 and is called
the sublattice of 𝒫 generated by 𝑋.
   The next theorem tells us when the distributive law partially holds in a complete orthomodular
lattice. 𝑝 is said to commute with 𝑞, denoted 𝑝𝐶𝑞, if 𝑝 = (𝑝 ∧ 𝑞) ∨ (𝑝 ∧ ¬𝑞).

Theorem 2.6 (The Foulis-Holland Theorem [14, 15]). Let (𝑃, ⪯, ¬) be a (complete) orthomodular
lattice. For any 𝑝, 𝑞, 𝑟 ∈ 𝑃, 𝑝𝐶𝑞 and 𝑝𝐶𝑟 jointly imply that (⟨{𝑝, 𝑞, 𝑟}⟩, ⪯) is distributive, where
⟨{𝑝, 𝑞, 𝑟}⟩ is the sublattice of (𝑃, ⪯) generated by {𝑝, 𝑞, 𝑟}.


3. Quantum Dynamic Algebra
In this section, we formulate a quantum dynamic algebra (QD-algebra), an algebra of DQL
with the Kleene star operator. The QD-algebra specifies all properties (namely, axioms) that
DQL is supposed to satisfy. The advantage of using algebra rather than logic is that algebra
can naturally express infinitary conjunction and disjunction as infimum and supremum of an
infinite set. Infinitary conjunction is used to characterize ⇤(𝑎∗ , 𝑝) in Definition 3.2.
   The most basic components (called atomic programs) of a quantum program are unitary
operators on a given Hilbert space. In this paper, we do not specify unitary operators but instead,
deal with them as mere symbols. Thus, no assumptions are imposed on atomic programs
henceforth.
   Regular quantum programs are formed from the atomic programs and elements in the domain
of a complete orthomodular lattice by using the program constructs ; (sequential composition),
∪ (non-deterministic choice), ∗ (iteration), and ? (test). These notations are used in Propositional
Dynamic Logic (PDL).

Definition 3.1. Let Π0 be a set of atomic programs. For any complete ortholattice ℒ = (𝑃, ⪯, ¬),
the set Πℒ of all regular quantum programs is generated by the grammar

                       Πℒ ∋ 𝑎 ∶∶= skip ∣ abort ∣ 𝜋 ∣ 𝑎; 𝑎 ∣ 𝑎 ∪ 𝑎 ∣ 𝑎∗ ∣ 𝑝?,

where 𝜋 ∈ Π0 and 𝑝 ∈ 𝑃.

   Unlike classical programs, the guard clause 𝑝? in the quantum if-then-else program (while-do
program) is evaluated in a complete orthomodular lattice that may not be a complete Boolean
lattice. That is,
                                (𝑝 ∧ (𝑞 ∨ 𝑟))? ≠ ((𝑝 ∧ 𝑞) ∨ (𝑝 ∧ 𝑟))?
in general.
   Πℒ includes various programs, but the if-then and while-do programs are particularly signif-
icant among them. These are defined by

                             if 𝑝 then 𝑎 else 𝑏 ∶= (𝑝?; 𝑎) ∪ (¬𝑝?; 𝑏),




                                                 5
                                  while 𝑝 do 𝑎 ∶= (𝑝?; 𝑎)∗ ; ¬𝑝?,

which means that the right-hand side of ∶= is abbreviated as the left-hand side of ∶=.
   It is worth paying attention to a precondition and postcondition of programs to verify them,
as Hoare Logic does. A regular quantum program 𝑎 ∈ Πℒ is said to be partially correct with
respect to a precondition 𝑝 ∈ 𝑃 and postcondition 𝑞 ∈ 𝑃 (denoted {𝑝} 𝑎 {𝑞}) if, whenever 𝑎 is
executed in a state satisfying 𝑝 and it halts in states 𝑠, then 𝑞 is satisfied in any such states 𝑠.
Because partial correctness does not guarantee that the program halts, the correctness is called
partial.
   We introduce a function ⇤ ∶ Πℒ ×𝑃 → 𝑃 to express the partial correctness: ⇤(𝑎, 𝑝) represents
the weakest precondition ensuring that 𝑝 will hold after executing 𝑎. Then, {𝑝} 𝑎 {𝑞} is expressed
as 𝑝 ⪯ ⇤(𝑎, 𝑞). This function ⇤ is subject to some conditions described in the following.

Definition 3.2. A quantum dynamic algebra (QD-algebra) is a quadruple (𝑃, ⪯, ¬, ⇤) that
consists of a complete orthomodular lattice (𝑃, ⪯, ¬) and function (scalar multiplication) ⇤ ∶
Πℒ × 𝑃 → 𝑃 satisfying the following conditions:
  (1) ⇤(skip, 𝑝) = 𝑝;
  (2) ⇤(abort, 𝑝) = ⋎;
  (3) ⇤(𝑎, ⋎) = ⋎;
  (4) ⇤(𝑎, 𝑝 ∧ 𝑞) = ⇤(𝑎, 𝑝) ∧ ⇤(𝑎, 𝑞);
  (5) ⇤(𝑎; 𝑏, 𝑝) = ⇤(𝑎, ⇤(𝑏, 𝑝));
  (6) ⇤(𝑎 ∪ 𝑏, 𝑝) = ⇤(𝑎, 𝑝) ∧ ⇤(𝑏, 𝑝);
  (7) ⇤(𝑎∗ , 𝑝) = ⋀{⇤(𝑎𝑖 , 𝑝) ∶ 𝑖 ≥ 0}, where 𝑎𝑖 is defined recursively by 𝑎0 = skip and
      𝑎𝑖+1 = 𝑎𝑖 ; 𝑎 for each 𝑖 ≥ 0;
  (8) ⇤(𝑝?, 𝑞) = ¬𝑝 ∨ (𝑝 ∧ 𝑞).

   Note that ⇤(𝑎∗ , 𝑝) exists owing to the completeness of (𝑃, ⪯, ¬). The condition (7) of Definition
3.2 is called ∗-continuity.
Example 3.1 (Powerset Dynamic Algebra). A powerset lattice (℘(𝑆), ⊆, 𝑐 , ⇤) with a function ⇤
satisfying the conditions of Definition 3.2 is a QD-algebra and is called a powerset QD-algebra.
Because a power lattice is a complete Boolean lattice, ⇤(𝑝?, 𝑞) = 𝑝 𝑐 ∪ 𝑞 holds by the distributive
law. Thus, ⇤(𝑝, 𝑞) is regarded as the (material) implication in classical logic.
Example 3.2 (Hilbert Dynamic Algebra). A Hilbert lattice (C(ℋ ), ⊆, ⟂ , ⇤) with a function ⇤
satisfying the conditions of Definition 3.2 is a QD-algebra and is called a Hilbert Dynamic
algebra. In a Hilbert Dynamic algebra, ⇤(𝑉 ?, 𝑊 ) is called the Sasaki hook [16], which is known
as the implication in quantum logic. In fact, ⇤(𝑉 ?, 𝑊 ) is the inverse image

                                𝑃𝑉−1 (𝑊 ) ∶= {𝑣 ∈ ℋ ∶ 𝑃𝑉 (𝑣) ∈ 𝑊 }

of 𝑊 under the projection 𝑃𝑉 ∶ ℋ → ℋ onto 𝑉 [17]. Interpreting a quantum test as a projection
is the key idea of DQL [1].
  Another significant example of QD-algebra is a characteristic algebra. We define the algebra
and prove that a characteristic algebra is a QD-algebra in Section 5.




                                                 6
Definition 3.3. Two regular quantum programs 𝑎, 𝑏 ∈ Πℒ are said to be inseparable, denoted
𝑎 ≈ 𝑏, if ⇤(𝑎, 𝑝) = ⇤(𝑏, 𝑝) for any 𝑝 ∈ 𝑃. A QD-algebra is said to be separable if ≈ is the identity
relation. That is, 𝑎 ≈ 𝑏 implies 𝑎 = 𝑏.

  The separability of a QD-algebra (𝑃, ⪯, ¬, ⇤) is required for ⇤(𝑎, −) ∶ 𝑃 → 𝑃 to satisfy
function extensionality. If not separable, it is possible that ⇤(𝑎, 𝑝) = ⇤(𝑏, 𝑝) for any 𝑝 ∈ 𝑃 but
⇤(𝑎, −) ≠ ⇤(𝑏, −).

Theorem 3.4. The following inseparability equations hold.
  (1) 𝑎; (𝑏; 𝑐) ≈ (𝑎; 𝑏); 𝑐.
  (2) 𝑎 ∪ (𝑏 ∪ 𝑐) ≈ (𝑎 ∪ 𝑏) ∪ 𝑐.
  (3) 𝑎; skip ≈ skip; 𝑎 ≈ 𝑎.
  (4) 𝑎 ∪ abort ≈ abort ∪ 𝑎 ≈ 𝑎.
  (5) 𝑎; (𝑏 ∪ 𝑐) ≈ (𝑎; 𝑏) ∪ (𝑎; 𝑐).
  (6) (𝑎 ∪ 𝑏); 𝑐 ≈ (𝑎; 𝑐) ∪ (𝑏; 𝑐).
  (7) 𝑎 ∪ 𝑏 ≈ 𝑏 ∪ 𝑎.
  (8) 𝑎; abort ≈ abort; 𝑎 ≈ abort.
  (9) 𝑎 ∪ 𝑎 ≈ 𝑎.
 (10) skip ≈ ⋎?.
 (11) abort ≈ ⋏?.
 (12) 𝑝? ≈ if 𝑝 then skip else abort.

Proof. Straightforward.

  It follows from the conditions (1)–(9) that (Πℒ , ∪, ; ) is an idempotent semiring with addition
∪ ∶ Πℒ → Πℒ and multiplication ; ∶ Πℒ → Πℒ if (𝑃, ⪯, ¬, ⇤) is separable. Evidently, abort is
the additive identity, and skip is the multiplicative identity of this semiring.


4. Quantum Dynamic Frame
So far, we have not mentioned the notion of states and the relations between them at all.
However, it is helpful to intuitively understand the properties of regular quantum programs by
representing their execution by relations.
  An orthoframe (also called an orthogonality space [18]) is used for giving Kripke (or relational)
semantics to orthologic (the smallest quantum logic) [19]. Henceforth, we write 𝑠𝑅𝑡̸ for the
condition (𝑠, 𝑡) ∉ 𝑅.

Definition 4.1. An orthoframe (𝑆, 𝑅) is a pair of a non-empty set 𝑆 of states and relation 𝑅 on
𝑆 that is irreflexive (𝑠𝑅𝑠̸ for any 𝑠 ∈ 𝑆) and symmetric (𝑠𝑅𝑡 implies 𝑡𝑅𝑠 for any 𝑠, 𝑡 ∈ 𝑆).

Example 4.1 (Hilbert Frame). Let ℋ be a Hilbert space, Pure(ℋ ) be the set of all pure states (unit
vectors) in ℋ, and ⟂ be the orthogonality relation on ℋ. Then, (Pure(ℋ ), ⟂) is an orthoframe,
and is called a Hilbert frame. Note that (ℋ , ⟂) is not an orthoframe because ⟂ is not irreflexive.
A counter-example is that 0 ⟂ 0, where 0 denotes the zero vector (origin) of ℋ.




                                                 7
  The notion of the orthogonal complement of a closed subspace is generalized as follows: the
orthogonal complement 𝑇 ⟂ of 𝑇 ⊆ 𝑆 is defined as

                                     {𝑠 ∈ 𝑆 ∶ 𝑠𝑅𝑡 for any 𝑡 ∈ 𝑇 }.

Here, 𝑇 may be empty, and ∅⟂ = 𝑆 by definition.
  The notion of a closed subspace is also generalized by using the above generalization of an
orthogonal complement. Recall that 𝑉 ⊆ ℋ is a closed subspace if and only if (𝑉 ⟂ )⟂ = 𝑉.

Definition 4.2. 𝑇 ⊆ 𝑆 is said to be orthoclosed in an orthoframe (𝑆, 𝑅) if (𝑇 ⟂ )⟂ = 𝑇.

   A relation 𝑅𝑎 on 𝑆 can be defined for each 𝑎 ∈ Πℒ by interpreting 𝑅𝑎 as the execution process
of a program 𝑎. That is, 𝑠𝑅𝑎 𝑡 is intended that 𝑡 is accessible from 𝑠 by executing 𝑎. For this reason,
we extend an orthoframe by adding relations for programs.

Definition 4.3. A quantum dynamic frame (QD-frame) is a triple (𝑆, 𝑅, ℛ) that consists of
an orthoframe (𝑆, 𝑅) and family ℛ ∶= {𝑅𝑎 }𝑎∈Πℒ of relations on 𝑆 satisfying the following
conditions:
  (1) 𝑠𝑅skip 𝑡 if and only if 𝑠 = 𝑡;
  (2) 𝑅abort = ∅;
  (3) 𝑠𝑅𝑎;𝑏 𝑡 if and only if 𝑠𝑅𝑎 𝑢 and 𝑢𝑅𝑏 𝑡 for some 𝑢 ∈ 𝑆;
  (4) 𝑠𝑅𝑎∪𝑏 𝑡 if and only if 𝑠(𝑅𝑎 ∪ 𝑅𝑏 )𝑡;
  (5) 𝑠𝑅𝑎∗ 𝑡 if and only if 𝑠(⋃𝑖≥0 𝑅𝑖 )𝑡, where 𝑅0 ∶= 𝑅skip and 𝑅𝑖+1 ∶= 𝑅𝑖 ; 𝑅 for each 𝑖 ≥ 0;
  (6) 𝑠𝑅𝑝? 𝑡 if and only if 𝑡 ∈ 𝑝 ∧ (¬𝑝 ∨ 𝑞) for any 𝑞 satisfying 𝑠 ∈ 𝑞.

  The above condition of 𝑅𝑝? is borrowed from [20].
Example 4.2 (Hilbert QD-frame). Let {𝑈𝜋 }𝜋∈Π0 be a family of unitary operators (quantum gates)
on ℋ. The graph 𝐺(𝑈𝜋 ) of 𝑈𝜋 is defined by

                                𝐺(𝑈𝜋 ) = {(𝑠, 𝑈𝜋 (𝑠)) ∶ 𝑠 ∈ Pure(ℋ )}.

Then, for any Hilbert frame (Pure(ℋ ), ⟂), the QD-frame (Pure(ℋ ), ⟂, ℛ), called a Hilbert
QD-frame, is uniquely constructed from {𝑅𝜋 }𝜋∈Π0 = {𝐺(𝑈𝜋 )}𝜋∈Π0 .
  Among various QD-frames, those satisfying the following properties are of particular signifi-
cance.

Definition 4.4.

    • A QD-frame (𝑆, 𝑅, ℛ) is said to be self-adjoint if 𝑅𝑝? is self-adjoint for each 𝑝 ∈ 𝑃: for any
      𝑠, 𝑡, 𝑢 ∈ 𝑆, 𝑠𝑅𝑝? 𝑡 and 𝑡𝑅𝑢̸ jointly imply that 𝑢𝑅𝑝? 𝑣 and 𝑠𝑅𝑣̸ for some 𝑣 ∈ 𝑆.
    • A QD-frame (𝑆, 𝑅, ℛ) is said to be orthostable if for any 𝑠, 𝑡 ∈ 𝑆 and 𝜋 ∈ Π0 , 𝑠𝑅𝜋 𝑡 implies
      that there exists 𝑢 ∈ 𝑆 such that 𝑠𝑅𝑢̸ and for any 𝑣 ∈ 𝑆, 𝑢𝑅𝑣̸ implies 𝑣𝑅𝜋 𝑡.

  The self-adjointness of a frame is also defined in [21] and [20] for different kinds of frames.
The self-adjointness of a quantum transition frame is defined in [21], and that of a DO-frame is
defined in [20].




                                                  8
5. Characteristic Algebra
Now we construct a characteristic algebra from a QD-frame (orthoframe). Moreover, we prove
that a characteristic algebra of an orthostable self-adjoint QD-frame is a QD-algebra. Before
embarking on this proof, we show that a characteristic algebra of an orthoframe is an ortholattice.
Definition 5.1. A characteristic algebra 𝐶(ℱ ) of an orthoframe ℱ = (𝑆, 𝑅) is a triple (𝑃ℱ , ⊆, ¬𝑅 )
that consists of the set 𝑃ℱ of all orthoclosed sets in ℱ, set inclusion relation ⊆ on 𝑃ℱ , and function
¬𝑅 ∶ 𝑃ℱ → 𝑃ℱ such that
                                   ¬𝑅 𝑝 = {𝑠 ∈ 𝑆 ∶ 𝑠𝑅𝑡 for any 𝑡 ∈ 𝑝}.
  Note that ¬𝑅 𝑝 = 𝑝 ⟂ by the definition of ⟂ . Hence,

                                   ¬𝑅 ¬𝑅 (¬𝑅 𝑝) = ¬𝑅 (¬𝑅 ¬𝑅 𝑝) = ¬𝑅 𝑝

if 𝑝 ∈ 𝑃ℱ . In other words, ¬𝑅 𝑝 ∈ 𝑃ℱ if 𝑝 ∈ 𝑃ℱ . This guarantees that ¬𝑅 ∶ 𝑃ℱ → 𝑃ℱ is
well-defined.
Lemma 5.2. 𝑃ℱ is a topped intersection structure on 𝑆:
  (1) ⋂ Γ ∈ 𝑃ℱ for any Γ ⊆ 𝑃ℱ , and
  (2) 𝑆 ∈ 𝑃ℱ .
Proof.      (1) We only prove the case that the number of elements in Γ is 2. The general case is
         obtained by a similar argument.
         Suppose that ¬𝑅 ¬𝑅 𝑝 = 𝑝 and ¬𝑅 ¬𝑅 𝑞 = 𝑞. Then, it suffices to show that

                                              ¬𝑅 ¬𝑅 (𝑝 ∩ 𝑞) = 𝑝 ∩ 𝑞.

         For the ⊆-part, suppose by contradiction that 𝑠 ∈ ¬𝑅 ¬𝑅 (𝑝 ∩ 𝑞) but 𝑠 ∉ 𝑝 ∩ 𝑞. Then, either
         𝑠 ∉ 𝑝 or 𝑠 ∉ 𝑞. Without loss of generality, we can assume 𝑠 ∉ 𝑝, and thus 𝑠 ∉ ¬𝑅 ¬𝑅 𝑝. In
         other words, 𝑠𝑅𝑡̸ for some 𝑡 ∈ ¬𝑅 𝑝. Hence, 𝑠𝑅𝑡̸ and 𝑡𝑅𝑢 for any 𝑢 ∈ 𝑝. By strengthening
         the condition of 𝑢, we can state that 𝑠𝑅𝑡̸ and 𝑡𝑅𝑢 for any 𝑢 ∈ 𝑝 ∩ 𝑞. It is equivalent to say
         that 𝑠𝑅𝑡̸ and 𝑡 ∈ ¬𝑅 (𝑝 ∩ 𝑞). However, the supposition 𝑠 ∈ ¬𝑅 ¬𝑅 (𝑝 ∩ 𝑞) means that 𝑠𝑅𝑢 for
         any 𝑢 ∈ ¬𝑅 (𝑝 ∩ 𝑞), which leads to a contradiction.
         The ⊇-part is proved as follows:

                 𝑠 ∈ 𝑝 ∩ 𝑞 ⇔ 𝑠 ∈ ¬ 𝑅 ¬𝑅 𝑝 ∩ ¬ 𝑅 ¬𝑅 𝑞
                           ⇔ ∀𝑡 ∈ 𝑆 (𝑡 ∈ ¬𝑅 𝑝 ⇒ 𝑠𝑅𝑡) and ∀𝑡 ∈ 𝑆 (𝑡 ∈ ¬𝑅 𝑞 ⇒ 𝑠𝑅𝑡)
                           ⇔ ∀𝑡 ∈ 𝑆 ((𝑡 ∈ ¬𝑅 𝑝 ⇒ 𝑠𝑅𝑡) and (𝑡 ∈ ¬𝑅 𝑞 ⇒ 𝑠𝑅𝑡))
                           ⇔ ∀𝑡 ∈ 𝑆 ((𝑡 ∈ ¬𝑅 𝑝 or 𝑡 ∈ ¬𝑅 𝑞) ⇒ 𝑠𝑅𝑡)
                           ⇔ ∀𝑡 ∈ 𝑆 ((∀𝑢 ∈ 𝑆 (𝑢 ∈ 𝑝 ⇒ 𝑡𝑅𝑢) or ∀𝑢 ∈ 𝑆 (𝑢 ∈ 𝑞 ⇒ 𝑡𝑅𝑢)) ⇒ 𝑠𝑅𝑡)
                           ⇒ ∀𝑡 ∈ 𝑆 ((∀𝑢 ∈ 𝑆 (𝑢 ∈ 𝑝 ⇒ 𝑡𝑅𝑢, or 𝑢 ∈ 𝑞 ⇒ 𝑡𝑅𝑢)) ⇒ 𝑠𝑅𝑡)
                           ⇔ ∀𝑡 ∈ 𝑆 ((∀𝑢 ∈ 𝑆, 𝑢 ∈ 𝑝 and 𝑢 ∈ 𝑞 ⇒ 𝑡𝑅𝑢) ⇒ 𝑠𝑅𝑡)
                           ⇔ ∀𝑡 ∈ 𝑆 ((∀𝑢 ∈ 𝑝 ∩ 𝑞, 𝑡𝑅𝑢) ⇒ 𝑠𝑅𝑡)
                           ⇔ 𝑠 ∈ ¬𝑅 ¬𝑅 (𝑝 ∩ 𝑞).




                                                       9
  (2) It suffices to show that ¬𝑅 ¬𝑅 𝑆 = 𝑆. It follows from (i) 𝑆 ⟂ = ∅ and (ii) ∅⟂ = 𝑆. (i) follows
      because no 𝑠 ∈ 𝑆 satisfies that 𝑠𝑅𝑡 for any 𝑡 ∈ 𝑆. If there would be such 𝑠, then 𝑠𝑅𝑠 but 𝑅 is
      irreflexive by definition, a contradiction. (ii) is immediate.


  In general, a topped intersection structure ordered by inclusion is a complete lattice [22,
Corollary 2.32]. Thus, the following corollary is obtained.

Corollary 5.3. (𝑃ℱ , ⊆) is a complete lattice, where the infimum and supremum of Γ ⊆ 𝑃ℱ in
(𝑃ℱ , ⊆) are ⋂ Γ and the smallest orthoclosed set ⨄ Γ containing ⋃ Γ, respectively.

  Symbolically,
                                 ⨄ Γ ∶= ⋂{𝑝 ∈ 𝑃ℱ ∶ ⋃ Γ ⊆ 𝑝}.
We shall denote by 𝑝 ⊎ 𝑞 the supremum of {𝑝, 𝑞}.

Theorem 5.4. 𝐶(ℱ ) = (𝑃ℱ , ⊆, ¬𝑅 ) is a complete ortholattice.

Proof. By Corollary 5.3, (𝑃ℱ , ⊆) is a complete lattice. The conditions (1)–(3) of an ortholattice
lattice (Definition 2.2) are proved as follows.
  (1) Proof of 𝑝 ∩ ¬𝑅 𝑝 = ∅ and 𝑝 ⊎ ¬𝑅 𝑝. Suppose for the sake of contradiction that 𝑠 ∈ 𝑝 ∩ ¬𝑅 𝑝.
      Then, 𝑠 ∈ 𝑝 and 𝑠 ∈ ¬𝑅 𝑝, and thus 𝑠𝑅𝑠 but it contradicts to the condition that 𝑅 is irreflexive.
      Hence, 𝑝 ∩ ¬𝑅 𝑝 = ∅.
  (2) Proof of ¬𝑅 ¬𝑅 𝑝 = 𝑝. It immediately follows from 𝑝 ∈ 𝑃ℱ .
  (3) Proof of 𝑝 ⊆ 𝑞 implies ¬𝑅 𝑞 ⊆ ¬𝑅 𝑝. Suppose that 𝑝 ⊆ 𝑞 and 𝑠 ∈ ¬𝑅 𝑞. Then, 𝑡 ∈ 𝑝 implies
      𝑡 ∈ 𝑞, and 𝑡 ∈ 𝑞 implies 𝑠𝑅𝑡. Thus, 𝑡 ∈ 𝑝 implies 𝑠𝑅𝑡, which is equivalent to 𝑠 ∈ ¬𝑅 𝑝.
      Consequently, 𝑝 ⊆ 𝑞 implies ¬𝑅 𝑞 ⊆ ¬𝑅 𝑝.


   The notion of characteristic algebra of an orthoframe is extended to that of an orthostable
self-adjoint QD-frame. Because 𝐶(ℱ ) is a complete ortholattice by Theorem 5.4, Π𝐶(ℱ ) is
well-defined.

Definition 5.5. Let ℱ = (𝑆, 𝑅) be an orthoframe. A characteristic algebra 𝐶(ℱℛ ) of an
orthostable self-adjoint QD-frame ℱℛ = (𝑆, 𝑅, ℛ) is a quadruple (𝑃ℱ , ⊆, ¬𝑅 , ⇤ℛ ) that consists
of the set 𝑃ℱ of all orthoclosed sets in ℱ, set inclusion relation ⊆ on 𝑃ℱ , and functions ¬𝑅 ∶
𝑃ℱ → 𝑃ℱ and ⇤ℛ ∶ Π𝐶(ℱ ) × 𝑃ℱ → 𝑃ℱ such that
  (1) ¬𝑅 𝑝 = 𝑝 ⟂ , which means ¬𝑅 𝑝 = {𝑠 ∈ 𝑆 ∶ 𝑠𝑅𝑡 for any 𝑡 ∈ 𝑝}, and
  (2) ⇤ℛ (𝑎, 𝑝) = {𝑠 ∈ 𝑆 ∶ 𝑡 ∈ 𝑝 for any 𝑡 ∈ 𝑆 satisfying 𝑠𝑅𝑎 𝑡}.

   It is not obvious that there exist ⇤ℛ (𝑎, 𝑝) in 𝑃ℱ for any 𝑝 ∈ 𝑃ℱ and 𝑎 ∈ Πℒ . Before proving
this, we show some lemmas.

Lemma 5.6.
  (1) ⇤ℛ (skip, 𝑝) = 𝑝.




                                                 10
  (2) ⇤ℛ (abort, 𝑝) = 𝑆.
  (3) ⇤ℛ (𝑎; 𝑏, 𝑝) = ⇤ℛ (𝑎, ⇤ℛ (𝑏, 𝑝)).
  (4) ⇤ℛ (𝑎 ∪ 𝑏, 𝑝) = ⇤ℛ (𝑎, 𝑝) ∩ ⇤ℛ (𝑏, 𝑝).
  (5) ⇤ℛ (𝑎∗ , 𝑝) = ⋂{⇤ℛ (𝑎𝑖 , 𝑝) ∶ 𝑖 ≥ 0}.

Proof.      (1) Proof of ⇤ℛ (skip, 𝑝) = 𝑝.

                       ⇤ℛ (skip, 𝑝) = {𝑠 ∈ 𝑆 ∶ 𝑡 ∈ 𝑝 for any 𝑡 ∈ 𝑆 satisfying 𝑠𝑅skip 𝑡}
                                      = {𝑠 ∈ 𝑆 ∶ 𝑠 ∈ 𝑝 for any 𝑠 ∈ 𝑆} = 𝑝.

  (2) Proof of ⇤ℛ (abort, 𝑝) = 𝑆.

                      ⇤ℛ (abort, 𝑝) = {𝑠 ∈ 𝑆 ∶ 𝑡 ∈ 𝑝 for any 𝑡 ∈ 𝑆 satisfying 𝑠𝑅abort 𝑡}
                                      = 𝑆.

  (3) Proof of ⇤ℛ (𝑎; 𝑏, 𝑝) = ⇤ℛ (𝑎, ⇤ℛ (𝑏, 𝑝)).

                    ⇤ℛ (𝑎; 𝑏, 𝑝) = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 (∃𝑢 ∈ 𝑆 (𝑠𝑅𝑎 𝑢 and 𝑢𝑅𝑏 𝑡) ⇒ 𝑡 ∈ 𝑝)}
                                = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 (∀𝑢 ∈ 𝑆 not (𝑠𝑅𝑎 𝑢 and 𝑢𝑅𝑏 𝑡) or 𝑡 ∈ 𝑝)}
                                = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆, ∀𝑢 ∈ 𝑆 (not (𝑠𝑅𝑎 𝑢 and 𝑢𝑅𝑏 𝑡) or 𝑡 ∈ 𝑝)}
                                = {𝑠 ∈ 𝑆 ∶ ∀𝑢 ∈ 𝑆, ∀𝑡 ∈ 𝑆 (not (𝑠𝑅𝑎 𝑢 and 𝑢𝑅𝑏 𝑡) or 𝑡 ∈ 𝑝)}
                                = {𝑠 ∈ 𝑆 ∶ ∀𝑢 ∈ 𝑆, ∀𝑡 ∈ 𝑆 (not 𝑠𝑅𝑎 𝑢 or not 𝑢𝑅𝑏 𝑡 or 𝑡 ∈ 𝑝)}
                                = {𝑠 ∈ 𝑆 ∶ ∀𝑢 ∈ 𝑆 (not 𝑠𝑅𝑎 𝑢 or ∀𝑡 ∈ 𝑆 (not 𝑢𝑅𝑏 𝑡 or 𝑡 ∈ 𝑝))}
                                = {𝑠 ∈ 𝑆 ∶ ∀𝑢 ∈ 𝑆 (𝑠𝑅𝑎 𝑢 ⇒ ∀𝑡 ∈ 𝑆 (𝑢𝑅𝑏 𝑡 ⇒ 𝑡 ∈ 𝑝))}
                                = {𝑠 ∈ 𝑆 ∶ ∀𝑢 ∈ 𝑆 (𝑠𝑅𝑎 𝑢 ⇒ 𝑢 ∈ ⇤ℛ (𝑏, 𝑝))}
                                = ⇤ℛ (𝑎, ⇤ℛ (𝑏, 𝑝)).

  (4) Proof of ⇤ℛ (𝑎 ∪ 𝑏, 𝑝) = ⇤ℛ (𝑎, 𝑝) ∩ ⇤ℛ (𝑏, 𝑝).

                  ⇤ℛ (𝑎 ∪ 𝑏, 𝑝) = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 (𝑠(𝑅𝑎 ∪ 𝑅𝑏 )𝑡 ⇒ 𝑡 ∈ 𝑝)}
                                = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 (𝑠𝑅𝑎 𝑡 or 𝑠𝑅𝑏 𝑡 ⇒ 𝑡 ∈ 𝑝)}
                                = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 ((𝑠𝑅𝑎 𝑡 ⇒ 𝑡 ∈ 𝑝) and (𝑠𝑅𝑏 𝑡 ⇒ 𝑡 ∈ 𝑝))}
                                = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 (𝑠𝑅𝑎 𝑡 ⇒ 𝑡 ∈ 𝑝) and ∀𝑡 ∈ 𝑆 (𝑠𝑅𝑏 𝑡 ⇒ 𝑡 ∈ 𝑝)}
                                = ⇤ℛ (𝑎, 𝑝) ∩ ⇤ℛ (𝑏, 𝑝).

  (5) Proof of ⇤ℛ (𝑎∗ , 𝑝) = ⋂{⇤ℛ (𝑎𝑖 , 𝑝) ∶ 𝑖 ≥ 0}.

                             ⇤ℛ (𝑎∗ , 𝑝) = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 (𝑠(⋃𝑖≥0 𝑅𝑎𝑖 )𝑡 ⇒ 𝑡 ∈ 𝑝)}
                                         = ⋂{⇤ℛ (𝑎𝑖 , 𝑝) ∶ 𝑖 ≥ 0}

         is obtained in a similar way as in the case of 𝑎 ∪ 𝑏.




                                                   11
  The following proof of Lemma 5.7 is attributed to the work of [20] by changing the notations.

Lemma 5.7. If (𝑆, 𝑅, ℛ) is self-adjoint, then
  (1) 𝑠 ∈ 𝑝 implies that 𝑠𝑅𝑝? 𝑠, and
  (2) ⇤ℛ (𝑝?, 𝑞) = ¬𝑅 𝑝 ⊎ (𝑝 ∩ 𝑞).

Proof.    (1) If 𝑠 ∈ 𝑞, then 𝑠 ∈ ¬𝑅 𝑝 ∪ 𝑞 ⊆ ¬𝑅 𝑝 ⊎ 𝑞. Thus, 𝑠 ∈ 𝑝 and 𝑠 ∈ 𝑞 jointly imply that
      𝑠 ∈ 𝑝 ∩ (¬𝑅 𝑝 ⊎ 𝑞). That is, 𝑠𝑅𝑝? 𝑠.
  (2) For the ⊆-part, suppose that 𝑠 ∉ ¬𝑅 (𝑝 ∩ ¬𝑅 (𝑝 ∩ 𝑞)). Then, there exists 𝑡 ∈ 𝑆 such that
        (⋆) 𝑡 ∈ 𝑝 ∩ ¬𝑅 (𝑝 ∩ 𝑞)
      but 𝑠𝑅𝑡.̸ Thus, 𝑡𝑅𝑝? 𝑡 by 𝑡 ∈ 𝑝 (Lemma 5.7 (1)). Because 𝑡𝑅𝑝? 𝑡 and 𝑡𝑅𝑠̸ (the symmetry of 𝑅 ̸
      follows from that of 𝑅), it follows from the self-adjointness of 𝑅𝑝? that 𝑠𝑅𝑝? 𝑢 and 𝑡𝑅𝑢̸ for
      some 𝑢 ∈ 𝑆.
                                                               𝑅𝑝?
                                                       𝑡             /𝑡

                                                  𝑅̸                          𝑅̸
                                                           ✏   𝑅𝑝?    ✏
                                                   ∃𝑢 o              𝑠
         By (⋆), 𝑡 ∈ ¬𝑅 (𝑝 ∩ 𝑞). That is, 𝑡𝑅𝑣̸ implies 𝑣 ∉ 𝑝 ∩ 𝑞 for any 𝑣 ∈ 𝑆. Hence, 𝑢 ∉ 𝑝 ∩ 𝑞 by 𝑡𝑅𝑢.̸
         It implies that 𝑢 ∉ 𝑝 or 𝑢 ∉ 𝑞 but the former must be false by 𝑠𝑅𝑝? 𝑢. Therefore, 𝑢 ∉ 𝑞 is
         obtained. It means that 𝑠𝑅𝑝? 𝑢 and 𝑢 ∉ 𝑞 for some 𝑢 ∈ 𝑆. Equivalently, 𝑠 ∉ ⇤ℛ (𝑝?, 𝑞).
         For the ⊇-part, suppose that 𝑠 ∉ ⇤ℛ (𝑝?, 𝑞). Then, there exists 𝑡 ∈ 𝑆 such that 𝑠𝑅𝑝? 𝑡 but
         𝑡 ∉ 𝑞. Thus, 𝑡 ∉ ¬𝑅 ¬𝑅 𝑞 by 𝑞 ∈ 𝑃ℱ . Hence, 𝑢 ∈ ¬𝑅 𝑞 but 𝑡𝑅𝑢̸ for some 𝑢 ∈ 𝑆. Because 𝑠𝑅𝑝? 𝑡
         and 𝑡𝑅𝑢,̸ it follows from the self-adjointness of 𝑅𝑝? that 𝑢𝑅𝑝? 𝑣 and 𝑠𝑅𝑣̸ for some 𝑣 ∈ 𝑆.

                                                               𝑅𝑝?
                                                   𝑠                 /𝑡

                                                  𝑅̸                          𝑅̸
                                                       ✏       𝑅𝑝?        ✏
                                                   ∃𝑣 o              𝑢

         Therefore, 𝑣 ∈ 𝑝 ∩ (¬𝑅 𝑝 ⊎ ¬𝑅 𝑞) by 𝑢𝑅𝑝? 𝑣 and 𝑢 ∈ ¬𝑅 𝑞. Consequently, it follows from 𝑠𝑅𝑣̸
         that
                   𝑠 ∉ ¬𝑅 (𝑝 ∩ (¬𝑅 𝑝 ⊎ ¬𝑅 𝑞)) = ¬𝑅 𝑝 ⊎ (¬𝑅 ¬𝑅 𝑝 ∩ ¬𝑅 ¬𝑅 𝑞) = ¬𝑅 𝑝 ⊎ (𝑝 ∩ 𝑞).


Theorem 5.8. If (𝑆, 𝑅, ℛ) is an orthostable self-adjoint QD-frame, then 𝑃ℱ is closed under ⇤ℛ :
𝑝 ∈ 𝑃ℱ implies ⇤ℛ (𝑎, 𝑝) ∈ 𝑃ℱ for each 𝑎 ∈ Πℒ .

Proof. We prove by structural induction on 𝑎 ∈ Πℒ .
  (1) The base cases, namely 𝑎 = skip, 𝑎 = abort, or 𝑎 = 𝜋 ∈ Π0 . For 𝑎 = skip, ⇤ℛ (skip, 𝑝) =
      𝑝 ∈ 𝑃ℱ by Lemma 5.6 (1). For 𝑎 = abort, ⇤ℛ (abort, 𝑝) = 𝑆 ∈ 𝑃ℱ by Lemma 5.6 (2) and
      Lemma 5.2 (2). For 𝑎 = 𝜋 ∈ Π0 , it suffices to show that

                                         ¬𝑅 ¬𝑅 ⇤ℛ (𝜋, 𝑝) = ⇤ℛ (𝜋, 𝑝).




                                                       12
      For the ⊆-part, suppose that 𝑠 ∈ ¬𝑅 ¬𝑅 ⇤ℛ (𝜋, 𝑝). Then,

           𝑠 ∈ ¬𝑅 ¬𝑅 ⇤ℛ (𝜋, 𝑝) ⇔ ∀𝑡 ∈ 𝑆 ((∀𝑢 ∈ ⇤ℛ (𝜋, 𝑝), 𝑡𝑅𝑢) ⇒ 𝑠𝑅𝑡)
                               ⇔ ∀𝑡 ∈ 𝑆 ((∀𝑢 ∈ 𝑆 ((∀𝑣 ∈ 𝑆 (𝑢𝑅𝜋 𝑣 ⇒ 𝑣 ∈ 𝑝)) ⇒ 𝑡𝑅𝑢)) ⇒ 𝑠𝑅𝑡)
                               ⇔ ∀𝑡 ∈ 𝑆 (𝑠𝑅𝑡̸ ⇒ ∃𝑢 ∈ 𝑆 (∀𝑣 ∈ 𝑆 (𝑢𝑅𝜋 𝑣 ⇒ 𝑣 ∈ 𝑝) and 𝑡𝑅𝑢))
                                                                                     ̸        (I)

     Assume that 𝑠𝑅𝜋 𝑡, and then we prove 𝑡 ∈ 𝑝 to show 𝑠 ∈ ⇤ℛ (𝜋, 𝑝). Because (𝑆, 𝑅, ℛ) is
     orthostable, there exists 𝑢 ′ ∈ 𝑆 such that
       (II) 𝑠𝑅𝑢̸ ′ and
      (III) ∀𝑣 ∈ 𝑆 (𝑢 ′ 𝑅𝑣̸ ⇒ 𝑣𝑅𝜋 𝑡).
     By (I) and (II), there exists 𝑢 ∈ 𝑆 such that
     (IV) ∀𝑣 ∈ 𝑆 (𝑢𝑅𝜋 𝑣 ⇒ 𝑣 ∈ 𝑝) and
       (V) 𝑢 ′ 𝑅𝑢.̸
     By (III) and (V), 𝑢𝑅𝜋 𝑡. Therefore, 𝑡 ∈ 𝑝 by (IV). We then prove the ⊇-part. Because 𝑅 is
     symmetric, 𝑅 ̸ is also symmetric. Thus, it suffices to show that

                            ∀𝑡 ∈ 𝑆 (𝑠𝑅𝑡̸ ⇒ ∃𝑢 ∈ 𝑆 (𝑢 ∈ ⇤ℛ (𝜋, 𝑝) and 𝑢𝑅𝑡)).
                                                                        ̸

      It is satisfied by choosing 𝑠 as 𝑢 if 𝑠 ∈ ⇤ℛ (𝜋, 𝑝).
  (2) The case of 𝑎 = 𝑏; 𝑐. ⇤ℛ (𝑎; 𝑏, 𝑝) = ⇤ℛ (𝑎, ⇤ℛ (𝑏, 𝑝)) ∈ 𝑃ℱ by Lemma 5.6 (3) and the
      induction hypothesis.
  (3) The case of 𝑎 = 𝑏 ∪ 𝑐. ⇤ℛ (𝑎 ∪ 𝑏, 𝑝) = ⇤ℛ (𝑎, 𝑝) ∩ ⇤ℛ (𝑏, 𝑝) ∈ 𝑃ℱ by Lemma 5.6 (4), Lemma
      5.2 (1), and the induction hypothesis.
  (4) The case of 𝑎 = 𝑏 ∗ . ⇤ℛ (𝑎∗ , 𝑝) = ⋂{⇤ℛ (𝑎𝑖 , 𝑝) ∶ 𝑖 ≥ 0} ∈ 𝑃ℱ by Lemma 5.6 (5), Lemma 5.2
      (1), and the induction hypothesis.
  (5) The case of 𝑎 = 𝑝?. ⇤ℛ (𝑝?, 𝑞) = ¬𝑅 𝑝 ⊎ (𝑝 ∩ 𝑞) ∈ 𝑃ℱ by Lemma 5.7 (2) and the definition
      of ⊎.


Theorem 5.9. The characteristic algebra 𝐶(ℱℛ ) of an orthostable self-adjoint QD-frame ℱℛ =
(𝑆, 𝑅, ℛ) is a QD-algebra.

Proof. (𝑃ℱ , ⊆) is a complete ortholattice with the infimum ⋂ Γ and supremum ⨄ Γ for each
Γ ⊆ 𝑃ℱ by Theorem 5.4.
  Moreover, (𝑃ℱ , ⊆) is an orthomodular lattice. To show the orthomodular law, it suffices to
show that 𝑠 ∈ 𝑝 ∩ ⇤ℛ (𝑝?, 𝑞) implies 𝑠 ∈ 𝑞. Because 𝑠 ∈ 𝑝, it follows from Lemma 5.7 (1) that
𝑠𝑅𝑝? 𝑠. Therefore, 𝑠 ∈ ⇤ℛ (𝑝?, 𝑞) implies 𝑠 ∈ 𝑞.
  Finally, we prove that 𝐶(ℱℛ ) is a QD-algebra. The only remaining thing to be shown is
the conditions (1)–(8) of Definition 3.2 but all of them except for (3) ⇤ℛ (𝑎, 𝑆) = 𝑆 and (4)
⇤ℛ (𝑎, 𝑝 ∩ 𝑞) = ⇤ℛ (𝑎, 𝑝) ∩ ⇤ℛ (𝑎, 𝑞) have already been shown in Lemma 5.6.
  (3) Proof of ⇤ℛ (𝑎, 𝑆) = 𝑆. Immediate.




                                               13
  (4) Proof of ⇤ℛ (𝑎, 𝑝 ∩ 𝑞) = ⇤ℛ (𝑎, 𝑝) ∩ ⇤ℛ (𝑎, 𝑞).

               ⇤ℛ (𝑎, 𝑝 ∩ 𝑞) = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 (𝑠𝑅𝑎 𝑡 ⇒ 𝑡 ∈ 𝑝 ∩ 𝑞)}
                             = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 (𝑠𝑅𝑎 𝑡 ⇒ 𝑡 ∈ 𝑝 and 𝑡 ∈ 𝑞)}
                             = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 ((𝑠𝑅𝑎 𝑡 ⇒ 𝑡 ∈ 𝑝) and (𝑠𝑅𝑎 𝑡 ⇒ 𝑡 ∈ 𝑞))}
                             = {𝑠 ∈ 𝑆 ∶ ∀𝑡 ∈ 𝑆 (𝑠𝑅𝑎 𝑡 ⇒ 𝑡 ∈ 𝑝) and ∀𝑡 ∈ 𝑆 (𝑠𝑅𝑎 𝑡 ⇒ 𝑡 ∈ 𝑞)}
                             = ⇤ℛ (𝑎, 𝑝) ∩ ⇤ℛ (𝑎, 𝑞).




6. Conclusion
In this paper, we formulated an algebra of regular quantum programs with the Kleene star
operator called QD-algebra by combining complete orthomodular lattice and dynamic algebra.
Moreover, to relate a QD-algebra to a state transition system induced by transitions of programs,
we defined a specific QD-algebra associated with relations called characteristic algebra. Our
main result is that a characteristic algebra of an orthostable self-adjoint QD-frame is a QD-
algebra (Theorem 5.9).
   The contribution of this paper is to give the semantics of the full-fledged DQL. The semantics
proposed so far are those of DQL lacking the Kleene star operator. However, the Kleene star
operator is indispensable to express practical quantum programs, especially quantum while
programs. Therefore, the semantics proposed in this paper is useful for the formal verification
of meaningful quantum programs.


Acknowledgments
The author would like to thank Prof. Kazuhiro Ogata for helpful feedback on this manuscript.
This work was supported by Grant-in-Aid for JSPS Research Fellow Grant Number 22J23575.


References
 [1] A. Baltag, S. Smets, Quantum logic as a dynamic logic, Synthese 179 (2011) 285–306.
 [2] A. Baltag, S. Smets, LQP: the dynamic logic of quantum information, Mathematical
     structures in computer science 16 (2006) 491–525.
 [3] A. Baltag, J. Bergfeld, K. Kishida, J. Sack, S. Smets, S. Zhong, PLQP & company: decidable
     logics for quantum algorithms, International Journal of Theoretical Physics 53 (2014)
     3628–3647.
 [4] J. M. Bergfeld, J. Sack, Deriving the correctness of quantum protocols in the probabilistic
     logic for quantum programs, Soft Computing 21 (2017) 1421–1441.
 [5] A. Baltag, S. Smets, Reasoning about quantum information: An overview of quantum
     dynamic logic, Applied Sciences 12 (2022) 4458.
 [6] G. Birkhoff, J. von Neumann, The logic of quantum mechanics, Annals of mathematics 57
     (1936) 823–843.




                                                14
 [7] D. Harel, D. Kozen, J. Tiuryn, Dynamic Logic, MIT Press, 2000.
 [8] A. Ambainis, E. Bach, A. Nayak, A. Vishwanath, J. Watrous, One-dimensional quantum
     walks, in: Proceedings of the thirty-third annual ACM symposium on Theory of computing,
     2001, pp. 37–49.
 [9] M. Hirvensalo, Quantum automata theory–a review, Algebraic Foundations in Computer
     Science (2011) 146–167.
[10] V. Pratt, Dynamic algebras: Examples, constructions, applications, Studia Logica 50 (1991)
     571–605.
[11] M. Rédei, Quantum logic in algebraic approach, volume 91 of Fundamental Theories of
     Physics, Springer, 1998.
[12] M. L. D. Chiara, R. Giuntini, Quantum logics, in: Handbook of Philosophical Logic,
     volume 6, 2nd ed., Kluwer Academic Publishers, 2002, pp. 129–228.
[13] I. Amemiya, H. Araki, A remark on piron’s paper, Publications of the Research Institute
     for Mathematical Sciences 2 (1966) 423–427.
[14] D. J. Foulis, A note on orthomodular lattices, Portugaliae mathematica 21 (1962) 65–72.
[15] S. S. Holland, A radon-nikodym theorem in dimension lattices, Transactions of the
     American Mathematical Society 108 (1963) 66–87.
[16] L. Herman, E. L. Marsden, R. Piziak, Implication connectives in orthomodular lattices,
     Notre Dame Journal of Formal Logic 16 (1975) 305–328.
[17] G. M. Hardegree, The conditional in quantum logic, Synthese 29 (1974) 63–80.
[18] D. J. Foulis, C. H. Randall, Lexicographic orthogonality, Journal of Combinatorial Theory,
     Series A 11 (1971) 157–162.
[19] R. I. Goldblatt, Semantic analysis of orthologic, Journal of Philosophical Logic 3 (1974)
     19–35.
[20] T. Kawano, Advanced Kripke frame for quantum logic, in: International Workshop on
     Logic, Language, Information, and Computation, 2018, pp. 237–249.
[21] A. Baltag, S. Smets, Complete axiomatizations for quantum actions, International Journal
     of Theoretical Physics 44 (2005) 2267–2282.
[22] B. A. Davey, H. A. Priestley, Introduction to lattices and order, 2nd ed., Cambridge university
     press, 2002.




                                                15