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 diferently 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 dificulty 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.
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 CEUR 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.
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
. A complete orthomodular is a complete ortholattice satisfying the orthomodular
for any , ∈
law
(
Many equivalent definitions of the orthomodular law are known [ 12, Lemma 19]. One of them is that ⪯ implies = ∨ (¬ ∧ ) . 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 ∈ } ⋁ Γ = ⋂{ ∈ C(ℋ ) ∶ ⋃ Γ ⊆ } 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 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 , , ∈ 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 {, , } .
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 significant among them. These are defined by if then else ∶= (?; ) ∪ (¬?; ), 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: ⇤(, ) the weakest precondition ensuring that will hold after executing . Then, {} {} represents is expressed as ⪯
⇤(, ) . This function ⇤ is subject to some conditions described in the following.
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 = ; for each ≥ 0 ;
(
. ⇤(, ) ∧
⇤(, ) ; ⇤(, ⇤(, )) ; ⇤(, ) ∧
⇤(, ) ;
⋀{⇤( , ) ∶ ≥ 0} , where is defined recursively by 0 = skip and
Note that ⇤( ∗, ) exists owing to the completeness of ( , ⪯, ¬) . The condition (
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, ⇤(?, ) = law. Thus, ⇤(, ) is regarded as the (material) implication in classical logic.
∪ holds by the distributive 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, ⇤( ?, ) as the implication in quantum logic. In fact, ⇤( ?, ) is called the Sasaki hook [16], which is known
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. 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.
(
(
(
It follows from the conditions (
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 ℋ.
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:
(
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 significance.
• 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 diferent 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].
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 :
(
Proof.
(
Suppose that ¬ ¬ = and ¬ ¬ = . Then, it sufices 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 ∈ ⇒ ) ⇒ )
⇔ ∈ ¬ ¬ ( ∩ ).
(
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,
⨄ Γ ∶= ⋂{ ∈ ℱ ∶ ⋃ Γ ⊆ }.
Theorem 5.4. (ℱ ) = ( ℱ, ⊆, ¬ ) is a complete ortholattice.
Proof. By Corollary 5.3, ( ℱ, ⊆) is a complete lattice. The conditions (
(
Then, ∈ and ∈ ¬ , and thus but it contradicts to the condition that is irreflexive.
Hence, ∩ ¬ = ∅ .
(
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
(
It is not obvious that there exist ⇤ℛ(, ) this, we show some lemmas.
Lemma 5.6.
(
in ℱ for any ∈ ℱ and ∈ Π ℒ. Before proving
Proof. (
(
⇤ℛ(, ⇤ℛ(, )) . ⇤ℛ(skip, ) = { ∈ ∶ ∈ = { ∈ ∶ ∈ for any ∈ satisfying skip} for any ∈ } = . ⇤ℛ(abort, ) = { ∈ ∶ ∈ = .
for any ∈ satisfying abort}
(
⇤ℛ( ∗, ) = { ∈ ∶ ∀ ∈ ((
⋃≥0 ) ⇒ ∈ )} = ⋂{⇤ℛ( , ) ∶ ≥ 0} is obtained in a similar way as in the case of ∪ .
The following proof of Lemma 5.7 is attributed to the work of [20] by changing the notations.
(
∈ ∩ (¬ ⊎ ) . That is, ? .
(⋆) ∈ ∩ ¬ ( ∩ )
(
By (⋆), ∈ ¬ ( ∩ ) . That is, ̸ implies ∉ ∩ It implies that ∉
or ∉ 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 ∈ . for any ∈ . Hence, ∉ ∩ by ̸ . but the former must be false by ? . Therefore, ∉ is ̸ ̸
? / ∃✏ o ?
? / ∃✏ 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 ∈ Π ℒ.
(
abort, ⇤ℛ(abort, ) = ∈
Lemma 5.2 (
⇤ℛ(, ). For the ⊆-part, suppose that ∈ ¬ ¬ ⇤ℛ(, ) . Then, ∈ ¬ ¬ ⇤ℛ(, ) ⇔ ∀ ∈ ((∀ ∈ 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 sufices to show that ∀ ∈ ( ⇏ ∃ ∈ ( ∈ ⇤ℛ(, ) and ))̸.
It is satisfied by choosing as if ∈ ⇤ℛ(, ) .
(
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 sufices to
show that ∈ ∩ ⇤ℛ(?, ) implies ∈ . Because ∈ , it follows from Lemma 5.7 (
Finally, we prove that (ℱ ℛ) is a QD-algebra. The only remaining thing to be shown is
the conditions (
⇤ℛ(, ) . ⇤ℛ(, ∩ ) = { ∈ ∶ ∀ ∈ ( = { ∈ ∶ ∀ ∈ ( = { ∈ ∶ ∀ ∈ (( = { ∈ ∶ ∀ ∈ ( = ⇤ℛ(, ) ∩ ⇤ℛ(, ).
⇒ ∈ ∩ )} ⇒ ∈ and ∈ )} ⇒ ∈ ) ⇒ ∈ ) and ( ⇒ ∈ ))} and ∀ ∈ ( ⇒ ∈ )}
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 QDalgebra (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.
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.