Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userThe Cayley-Dickson Construction in ACL2
87
0
0.0
(
0
)
Added by
EPTCS
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
The Cayley-Dickson Construction is a generalization of the familiar construction of the complex numbers from pairs of real numbers. The complex numbers can be viewed as two-dimensional vectors equipped with a multiplication. The construction can be used to construct, not only the two-dimensional Complex Numbers, but also the four-dimensional Quaternions and the eight-dimensional Octonions. Each of these vector spaces has a vector multiplication, v_1*v_2, that satisfies: 1. Each nonzero vector has a multiplicative inverse. 2. For the Euclidean length of a vector |v|, |v_1 * v_2| = |v_1| |v2|. Real numbers can also be viewed as (one-dimensional) vectors with the above two properties. ACL2(r) is used to explore this question: Given a vector space, equipped with a multiplication, satisfying the Euclidean length condition 2, given above. Make pairs of vectors into new vectors with a multiplication. When do the newly constructed vectors also satisfy condition 2?
rate research
Read More
We define in the setting of homotopy type theory an H-space structure on $mathbb S^3$. Hence we obtain a description of the quaternionic Hopf fibration $mathbb S^3hookrightarrowmathbb S^7twoheadrightarrowmathbb S^4$, using only homotopy invariant tools.
Iterative algorithms are traditionally expressed in ACL2 using recursion. On the other hand, Common Lisp provides a construct, loop, which -- like most programming languages -- provides direct support for iteration. We describe an ACL2 analogue loop$ of loop that supports efficient ACL2 programming and reasoning with iteration.
A perfect number is a positive integer n such that n equals the sum of all positive integer divisors of n that are less than n. That is, although n is a divisor of n, n is excluded from this sum. Thus 6 = 1 + 2 + 3 is perfect, but 12 < 1 + 2 + 3 + 4 + 6 is not perfect. An ACL2 theory of perfect numbers is developed and used to prove, in ACL2(r), this bit of mathematical folklore: Even if there are infinitely many perfect numbers the series of the reciprocals of all perfect numbers converges.
Given a field K, a quadratic extension field L is an extension of K that can be generated from K by adding a root of a quadratic polynomial with coefficients in K. This paper shows how ACL2(r) can be used to reason about chains of quadratic extension fields Q = K_0, K_1, K_2, ..., where each K_i+1 is a quadratic extension field of K_i. Moreover, we show that some specific numbers, such as the cube root of 2 and the cosine of pi/9, cannot belong to any of the K_i, simply because of the structure of quadratic extension fields. In particular, this is used to show that the cube root of 2 and cosine of pi/9 are not rational.
We report on a verification of the Fundamental Theorem of Algebra in ACL2(r). The proof consists of four parts. First, continuity for both complex-valued and real-valued functions of complex numbers is defined, and it is shown that continuous functions from the complex to the real numbers achieve a minimum value over a closed square region. An important case of continuous real-valued, complex functions results from taking the traditional complex norm of a continuous complex function. We think of these continuous functions as having only one (complex) argument, but in ACL2(r) they appear as functions of two arguments. The extra argument is a context, which is uninterpreted. For example, it could be other arguments that are held fixed, as in an exponential function which has a base and an exponent, either of which could be held fixed. Second, it is shown that complex polynomials are continuous, so the norm of a complex polynomial is a continuous real-valued function and it achieves its minimum over an arbitrary square region centered at the origin. This part of the proof benefits from the introduction of the context argument, and it illustrates an innovation that simplifies the proofs of classical properties with unbound parameters. Third, we derive lower and upper bounds on the norm of non-constant polynomials for inputs that are sufficiently far away from the origin. This means that a sufficiently large square can be found to guarantee that it contains the global minimum of the norm of the polynomial. Fourth, it is shown that if a given number is not a root of a non-constant polynomial, then it cannot be the global minimum. Finally, these results are combined to show that the global minimum must be a root of the polynomial. This result is part of a larger effort in the formalization of complex polynomials in ACL2(r).
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
