A HOL-Light Library for Vectors of Complex Numbers
Sanaz Khan Afshar and
Vincent Aravantinos
(Hardware Verification Group,
Concordia University)
DOWNLOAD
Despite
the rich libraries on complex numbers and real vector analysis, no
concrete work has been developed on the formalization of complex
vector analysis. In many engineering problems, the unknown parameters
are complex-valued vectors and, often, the task of the system
designer is to find the values of these complex parameters which
optimize a chosen criterion function. Examples of areas include
optics[1], electric circuits[2], telecommunications[3], acoustics[4],
control theory[5], and electrostatics[6].
Therefore,
we tackle the formalization of complex vector analysis. This is done
using the HOL-Light theorem prover since it already has good support
for complex number arithmetic and a general notion of vector.
Vectors
of N elements of a set S are defined as functions from [1..N] to S:
i.e. a vector V is actually a function that takes a number between 1
and N and returns the element corresponding to that value. In
HOL-Light, this is written as lambda
i.V where
V is the expression (generally containing i) that allows to compute
the value of the ith
element.
For instance, the null vector is formalized by lambda
i.0 (note
that this is the null vector of integers; the null vector of real
numbers is formalized by lambda
i.&0,
and the null vector of complex numbers by lambda
i.Cx(&0)).
The vector containing 1 as its first element, 2 as its second
element, and so forth, is formalized by lambda
i.i.
Any expression can be used as V, e.g. the vector for which the ith
element
contains i2
is
lambda
i.i*i.
The ith
element
of a vector v can be retrieved using the notation v$i.
For instance, if v is lambda
i.i*i,
then v$1=1,
v$2=4,
etc. This allows us to define addition, negation, subtraction, and
scalar multiplication – which are necessary to formalize complex
vector spaces – as presented in Table 1.
Those
definitions are fairly standard and one might wonder how this differs
from, say, the corresponding definitions for real vectors. To answer
this wonder, it is important to notice that HOL-Light only provides
the type of vectors and the operations lambda
and
&,
but it does not provide any algebraic operations nor properties about
vectors. Otherwise stated: we have vectors but we do not have any
properties about them. The reason is that the vectors in HOL-Light
are vectors of any type (i.e. integers, real numbers, etc.). But the
algebraic properties of vectors depend strongly on the type of their
elements (e.g. every vector of real numbers has an inverse with
respect to vector addition, which is not the case of vectors of
natural numbers). Consequently the properties of real vectors are not
the same as the ones of complex vectors, for instance. This is why,
even though a library of real vector analysis already exists, we need
to develop our own library of complex vectors.
In
particular, the general notion of vector which is provided in
HOL-Light does not denote, in general, elements of a vector space
(contrarily to what their name suggests). Namely, vectors in
HOL-Light are just functions from [1..N] to a set S. Whereas a vector
space is a set S together with a field F and two binary operators
that satisfy eight axioms [7]. Consequently, we need to prove that
taking the field of complex for F and the above addition and scalar
multiplication for the two binary operators indeed satisfy the
corresponding axioms. Those are listed in Table 2 and have all been
formalized and proved in HOL-Light.
We
also developed a simple algorithm which is able to prove various
basic results about complex vectors in an automatized way. This
algorithm is able to prove all the above eight axioms, plus many
other basic but useful facts.
Cross
and Dot Product
The
cross product and the dot product are frequently used in vector
analysis. In particular, in the analysis of optical devices, the
electric field, magnetic field and the wavevector are all orthogonal
and related by the cross product. In HOL-Light, we called the cross
product ccross (generally, all the notions for complex vectors
are given the same name as their real counterparts, with a 'c', for
"complex"); Table 3 shows its formal definition and some of
its basic properties which we developed in HOL-Light.
In
order to formalize the derivation of functions of complex-valued
vectors, we will also need the concept of norm (which is needed to
define limits and differentiation). We define norms using the
definition of dot product, written cdot in HOL-Light. Table 4
gives the formal definition of cdot and some of its major
properties, that we all proved in HOL-Light. At first we defined dot
product over complex vectors with size N but, in our context, only
dimension three is useful. Thus we developed all definitions and
theorems in this dimension which greatly simplifies the formal
development of the theory. Finally we formally defined the concepts
of orthogonality and collinearity between two complex vectors.
References
[1]
M. Born, E. Wolf, and A. B. Bhatia. Principles of Optics:
Electromagnetic Theory of Propagation, Interference and Diffraction
of Light. Cambridge University Press, 2002.
[2]
F.J. Gonzalez-Vazquez. The differentiation of functions of
conjugate complex variables: application to power network analysis.
IEEE Transactions on Education, pages 286–291, 1988.
[3]
N. A. Golias, T.V. Yioultsis, and T.D. Tsiboukis. Vector complex
eigenmode analysis of microwave cavities. Microwaves, Antennas and
Propagation, IEE Proceedings, pages 457–461, 1995.
[4]
D. Havelock, S. Kuwano, and M. Vorlander. Handbook of signal
processing in acoustics. Springer, 2008.
[5]
A. Hjorungnes, D. Gesbert, and D.P. Palomar. Unified theory of
complex-valued matrix differentiation. In IEEE International
Conference on Acoustics, Speech and Signal Processing, pages III–345
–III–348, 2007.
[6]
B. M. Kolundzija and A. R. Djordjevic. Electromagnetic modelling of
composite metallic and dielectric structures. Artech House, 2002.
[7]
J. C. Tallack. Introduction to vector analysis. Cambridge University
Press, 1970.