scholarly journals Platform-independent Specification and Verification of the Standard Mathematical Square Root Function

2018 ◽  
Vol 25 (6) ◽  
pp. 637-666
Author(s):  
Nikolay V. Shilov ◽  
Dmitry A. Kondratyev ◽  
Igor S. Anureev ◽  
Eugene V. Bodin ◽  
Alexei V. Promsky
Keyword(s):  
Root Function ◽  
Square Root ◽  
Combined Approach ◽  
Real Numbers ◽  
Mathematical Functions ◽  
Square Roots ◽  
Computer Aided ◽  
Platform Independence ◽  
Fix Point ◽  
Specification And Verification

The project “Platform-independent approach to formal specification and verification of standard mathematical functions” is aimed onto the development of incremental combined approach to specification and verification of standard Mathematical functions like sqrt, cos, sin, etc. Platform-independence means that we attempt to design a relatively simple axiomatization of the computer arithmetics in terms of real arithmetics (i.e. the field \(\mathbb{R}\) of real numbers) but do not specify neither base of the computer arithmetics, nor a format of numbers representation. Incrementality means that we start with the most straightforward specification of the simplest case to verify the algorithm in real numbers and finish with a realistic specification and a verification of the algorithm in computer arithmetics. We call our approach combined because we start with manual (pen-and-paper) verification of the algorithm in real numbers, then use this verification as proof-outlines for a manual verification of the algorithm in computer arithmetics, and finish with a computer-aided validation of the manual proofs with a proof-assistant system (to avoid appeals to “obviousness” that are common in human-carried proofs). In the paper, we apply our platform-independent incremental combined approach to specification and verification of the standard Mathematical square root function. Currently a computer-aided validation was carried for correctness (consistency) of our fix-point arithmetics and for the existence of a look-up table with the initial approximations of the square roots for fix-point numbers.

scholarly journals Finding of principle square root of a real number by using interpolation method

2018 ◽  
Vol 7 (1) ◽  
pp. 77-83
Author(s):  
Rajendra Prasad Regmi
Keyword(s):  
Real Number ◽  
Positive Real Number ◽  
Interpolation Method ◽  
Square Root ◽  
Real Numbers ◽  
Positive Real ◽  
Unknown Quantity ◽  
Square Roots

There are various methods of finding the square roots of positive real number. This paper deals with finding the principle square root of positive real numbers by using Lagrange’s and Newton’s interpolation method. The interpolation method is the process of finding the values of unknown quantity (y) between two known quantities.

scholarly journals Platform-Independent Specification and Verification of the Standard Mathematical Square Root Function

2019 ◽  
Vol 53 (7) ◽  
pp. 595-616
Author(s):  
N. V. Shilov ◽  
D. A. Kondratyev ◽  
I. S. Anureev ◽  
E. V. Bodin ◽  
A. V. Promsky
Keyword(s):  
Root Function ◽  
Square Root ◽  
Specification And Verification

scholarly journals Algebraic singularities of scattering amplitudes from tropical geometry

2021 ◽  
Vol 2021 (4) ◽  
Author(s):  
James Drummond ◽  
Jack Foster ◽  
Ömer Gürdoğan ◽  
Chrysostomos Kalousios
Keyword(s):  
Scattering Amplitudes ◽  
Natural Language ◽  
Tropical Geometry ◽  
Cluster Algebras ◽  
Finite Alphabet ◽  
Square Root ◽  
Finite Sets ◽  
Yang Mills ◽  
Square Roots ◽  
Algebraic Singularities

Abstract We address the appearance of algebraic singularities in the symbol alphabet of scattering amplitudes in the context of planar $$ \mathcal{N} $$ N = 4 super Yang-Mills theory. We argue that connections between cluster algebras and tropical geometry provide a natural language for postulating a finite alphabet for scattering amplitudes beyond six and seven points where the corresponding Grassmannian cluster algebras are finite. As well as generating natural finite sets of letters, the tropical fans we discuss provide letters containing square roots. Remarkably, the minimal fan we consider provides all the square root letters recently discovered in an explicit two-loop eight-point NMHV calculation.

Correlation of Electrical, Structural, and Optical Properties of Erbium In Silicon

1993 ◽  
Vol 301 ◽  
Author(s):  
J. L. Benton ◽  
D. J. Eaglesham ◽  
M. Almonte ◽  
P. H. Citrin ◽  
M. A. Marcus ◽  
...  
Keyword(s):  
Root Function ◽  
Free Exciton ◽  
Excitation Power ◽  
Optically Active ◽  
Photoluminescence Intensity ◽  
Square Root ◽  
Structural And Optical Properties ◽  
X Ray ◽  
X Ray Absorption ◽  
Donor Activity

ABSTRACTAn understanding of the electrical, structural, and optical properites of Er in Si is necessary to evaluate this system as an opto-electronic material. Extended x-ray absorption fine structure, EXAFS, measurements of Er-implanted Si show that the optically active impurity complex is Er surrounded by an O cage of 6 atoms. The Er photoluminescence intensity is a square root function of excitation power, while the free exciton intensity increases linearly. The square root dependence of the 1.54μm-intensity is independent of measurement temperature and independent of co-implanted species. Ion-implantation of Er in Si introduces donor activity, but spreading resistance carrier concentration profiles indicate that these donors do not effect the optical activity of the Er.

scholarly journals Applications of Square Roots of Diffeomorphisms

Axioms ◽  
2019 ◽  
Vol 8 (2) ◽  
pp. 43
Author(s):  
Yoshihiro Sugimoto
Keyword(s):  
Smooth Manifold ◽  
Contact Manifold ◽  
Diffeomorphism Group ◽  
Square Root ◽  
Square Roots ◽  
Group Diff

In this paper, we prove that on any contact manifold ( M , ξ ) there exists an arbitrary C ∞ -small contactomorphism which does not admit a square root. In particular, there exists an arbitrary C ∞ -small contactomorphism which is not “autonomous”. This paper is the first step to study the topology of C o n t 0 ( M , ξ ) ∖ Aut ( M , ξ ) . As an application, we also prove a similar result for the diffeomorphism group Diff ( M ) for any smooth manifold M.

Fast algorithm for the three-dimensional Poisson equation in infinite domains

2020 ◽  
Author(s):  
Chunxiong Zheng ◽  
Xiang Ma
Keyword(s):  
Poisson Equation ◽  
Fast Algorithm ◽  
Root Function ◽  
Computational Cost ◽  
Three Dimensional ◽  
Chebyshev Approximation ◽  
Laplacian Operator ◽  
Square Root ◽  
Infinite Domain ◽  
Infinite Domains

Abstract This paper is concerned with a fast finite element method for the three-dimensional Poisson equation in infinite domains. Both the exterior problem and the strip-tail problem are considered. Exact Dirichlet-to-Neumann (DtN)-type artificial boundary conditions (ABCs) are derived to reduce the original infinite-domain problems to suitable truncated-domain problems. Based on the best relative Chebyshev approximation for the square-root function, a fast algorithm is developed to approximate exact ABCs. One remarkable advantage is that one need not compute the full eigensystem associated with the surface Laplacian operator on artificial boundaries. In addition, compared with the modal expansion method and the method based on Pad$\acute{\textrm{e}}$ approximation for the square-root function, the computational cost of the DtN mapping is further reduced. An error analysis is performed and numerical examples are presented to demonstrate the efficiency of the proposed method.

Design and Implementation of High-Level Numerical Analysis Functions Based on Computational Arrays for Applications in Engineering

2000 ◽  
Author(s):  
Harry H. Cheng ◽  
Xudong Hu ◽  
Bin Lin
Keyword(s):  
Numerical Analysis ◽  
Variable Number ◽  
Data Types ◽  
Real Numbers ◽  
Mathematical Functions ◽  
C Language ◽  
Complex Arithmetic ◽  
Design And Implementation ◽  
Complex Functions ◽  
High Level

Abstract This paper presents the design and implementation of high-level numerical analysis functions in CH, a superset of C language developed for the convenience of scientific and engineering computations. In CH, complex number is treated as a built-in data type, so that the syntaxes of complex arithmetic, relational operations, and built-in mathematical functions are the same as those for real numbers. The variable number of arguments is used in the built-in mathematical functions to simplify the computation of different branches of multi-valued complex functions. The computational arrays are introduced to handle the arrays in the numerical computations. Passing arrays of variable length by arrays of deferred-shape and arrays of assumed-shape to functions are discussed. These methods allow the arrays to be passed with their rank, dimensions and data types. A list of high-level numerical functions and two examples of the applications in the scientific and engineering are given in the paper.

scholarly journals Vector logic allows counterfactual virtualization by the square root of NOT

2020 ◽  
Author(s):  
Eduardo Mizraji
Keyword(s):  
Square Root ◽  
Mathematical Approach ◽  
Complex Matrix ◽  
Virtual Character ◽  
Truth Values ◽  
Square Roots ◽  
Counterfactual Conditionals ◽  
Basic Representation ◽  
Logical Functions ◽  
Matrix Vector

Abstract In this work, we investigate the representation of counterfactual conditionals using the vector logic, a matrix-vector formalism for logical functions and truth values. Inside this formalism, the counterfactuals can be transformed in complex matrices preprocessing an implication matrix with one of the square roots of NOT, a complex matrix. This mathematical approach puts in evidence the virtual character of the counterfactuals. This happens because this representation produces a valuation of a counterfactual that is the superposition of the two opposite truth values weighted, respectively, by two complex conjugated coefficients. This result shows that this procedure gives an uncertain evaluation projected on the complex domain. After this basic representation, the judgement of the plausibility of a given counterfactual allows us to shift the decision towards an acceptance or a refusal. This shift is the result of applying for a second time one of the two square roots of NOT.

scholarly journals Handling of Complex Numbers in the CHProgramming Language

1993 ◽  
Vol 2 (3) ◽  
pp. 77-106 ◽  
Author(s):  
Harry H. Cheng
Keyword(s):  
Variable Number ◽  
Language Design ◽  
Complex Numbers ◽  
Computer Language ◽  
Real Numbers ◽  
Mathematical Functions ◽  
Complex Arithmetic ◽  
Complex Functions ◽  
Complex Features ◽  
Branch Cuts

The handling of complex numbers in the CHprogramming language will be described in this paper. Complex is a built-in data type in CH. The I/O, arithmetic and relational operations, and built-in mathematical functions are defined for both regular complex numbers and complex metanumbers of ComplexZero, Complexlnf, and ComplexNaN. Due to polymorphism, the syntax of complex arithmetic and relational operations and built-in mathematical functions are the same as those for real numbers. Besides polymorphism, the built-in mathematical functions are implemented with a variable number of arguments that greatly simplify computations of different branches of multiple-valued complex functions. The valid lvalues related to complex numbers are defined. Rationales for the design of complex features in CHare discussed from language design, implementation, and application points of views. Sample CHprograms show that a computer language that does not distinguish the sign of zeros in complex numbers can also handle the branch cuts of multiple-valued complex functions effectively so long as it is appropriately designed and implemented.

Sign in / Sign up

Export Citation Format

Share Document