NICOP - Strongly Typed Numerical Computation (Tycoon)
Abstract
Numerical algorithms are used in many domains. For example, they are intensively used inscientific computing and physical simulatio""n for weather forecast, structural engineering,geophysics, astronomy and even finance. Other numerical algorithms, e.g. for digital"" signalprocessing, are also ubiquitous in critical embedded systems such as aircrafts, cars, spacevehicles or nuclear powerplants." Any computation done by these algorithms is approximate sinceit relies on floating-point numbers which represent with a finite number of digits the real numberswhose length is generally infinite. Roundoff errors necessarily arise during the computation andthes"e approximations may, in some cases, significantly corrupt the results of the computation.As more and more critical decisions and t""asks relying on complex computations are delegated tomachines, needs of design methods and verification and validation techniques s""trongly increase,to ensure that the numbers given by the computers may be trusted. While most of existing workconcerns verificatio""n and validation techniques, assisted design methods are strongly desiredsince it is extremely difficult to understand the reasons" why the implementation of a formula isnumerically inaccurate and how to improve it. This is because the floating-point arithmetic isparticularly not intuitive. The values have a finite number of digits and algebraic laws likeassociativity or commutativity do" not hold. For example, the evaluation by a computer ofmathematically equivalent expressions (e.g. x ~ (1 + x) and x + x2) possibly"" leads to very differentresults. It is then necessary to provide tools to the programmers, to help them to validate andincrease th""e numerical quality of their codes and, broadly, to develop more quickly more reliablenumerical codes.In the Tycoon Project, we ai""m at developing methods able to detect and correct numericalaccuracy errors at software development time, i.e. during the programmi""ng phase. From asoftware engineering point of view, the advantages of our approach are many, since it is wellknownthat late bug de"tection is time and money consuming. We also aim at using intensivelyused techniques recognized for their ability to avoid run-time errors. This choice is motivated byefficiency reasons as well as for end-user adoptability reasons. We plan to build upon the MLp"rogramming language. More precisely, we aim at developing a ML-like type system for floatingpointcomputations in which the type of" an arithmetic expression carries information on itsaccuracy. Type systems have been used in programming languages such as ML for a" long time,to reduce possibilities of bugs before running the programs.We plan to develop an innovative dependent type system toge""ther with a new type inferencealgorithm which, from the user point of view, will act like ML type system even if they strongly diff"erin their conception. We will design a core ML-like programming language based on our accuracyawaretype system. This language will take advantage of the type information to evaluate thearithmetic expressions. The objective is that the numerical values printed by the programs arecorrect roundoffs of the exact values that we would obtain if the computer used the arithmetic ofreal numbers." In other words, instead of printing both correct and incorrect digits of a floating-pointnumber as any program does currently, we" want our programs print numbers with possibly fewerdigits but which approximate correctly the exact result at the given precision." Doing so, the usermay trust the results of the programs, contrarily to what it should do for usual programs. Finally,we will prop""ose a set of elementary numerical algorithms (Simpson, Horner, etc.) written in ourlanguage and which guaranty the accuracy of thei"r results.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Mar 26, 2018
- Source ID
- N629091812068
Entities
People
- Matthieu Martel
Organizations
- Office of Naval Research
- United States Navy
- University of Perpignan