Users' manual for the Sollya tool - Release 2.9

Sylvain Chevillard (sylvain.chevillard@ens-lyon.org),
Christoph Lauter (christoph.lauter@ens-lyon.org)
and Mioara Joldeș (mioara.joldes@ens-lyon.fr).

License

The Sollya tool is Copyright © 2006-2011 by
Laboratoire de l'Informatique du Parallélisme - UMR CNRS - ENS Lyon - UCB Lyon 1 - INRIA 5668, Lyon, France, LORIA (CNRS, INPL, INRIA, UHP, U-Nancy 2), Nancy, France, Laboratoire d'Informatique de Paris 6, Équipe PEQUAN, UPMC Université Paris 06 - CNRS - UMR 7606 - LIP6, Paris, France, and by INRIA Sophia-Antipolis Méditerranée, APICS Team, Sophia-Antipolis, France. All rights reserved.

The Sollya tool is open software. It is distributed and can be used, modified and redistributed under the terms of the CeCILL-C licence available at http://www.cecill.info/ and reproduced in the COPYING file of the distribution. The distribution contains parts of other libraries as a support for but not integral part of Sollya. These libraries are reigned by the GNU Lesser General Public License that is available at http://www.gnu.org/licenses/ and reproduced in the COPYING file of the distribution.

This software (Sollya) is distributed WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Direct access to the list of available commands

1 - Compilation and installation of the Sollya tool

1.1 - Compilation dependencies

The Sollya distribution can be compiled and installed using the usual ./configure, make, make install procedure. Besides a C and a C++ compiler, Sollya needs the following software libraries and tools to be installed. The ./configure script checks for the installation of the libraries. However Sollya will build without error if some of its external tools are not installed. In this case an error will be displayed at runtime.

The use of the external tool rlwrap is highly recommended but not required. Use the -A option of rlwrap for correctly displayed ANSI X3.64/ ISO/IEC 6429 colored prompts (see below).

1.2 - Sollya command line options

Sollya can read input on standard input or in a file whose name is given as an argument when Sollya is invoked. The tool will always produce its output on standard output, unless specificly instructed by a particular Sollya command that writes to a file. The following lines are valid invocations of Sollya, assuming that bash is used as a shell:

 /% sollya
...
 /% sollya myfile.sollya
...
 /% sollya < myfile.sollya

If a file given as an input does not exist, an error message is displayed.

All configurations of the internal state of the tool are done by commands given on the Sollya prompt or in Sollya scripts. Nevertheless, some command line options are supported; they work at a very basic I/O-level and can therefore not be implemented as commands.

The following options are supported when calling Sollya:

2 - Introduction

Sollya is an interactive tool for handling numerical functions and working with arbitrary precision. It can evaluate functions accurately, compute polynomial approximations of functions, automatically implement polynomials for use in math libraries, plot functions, compute infinity norms, etc. Sollya is also a full-featured script programming language with support for procedures etc.

Let us begin this manual with an example. Sollya does not allow command line edition; since this may quickly become uncomfortable, we highly suggest to use the rlwrap tool with Sollya:

 /% rlwrap -A sollya
   >

Sollya manipulates only functions in one variable. The first time that an unbound variable is used, this name is fixed. It will be used to refer to the free variable. For instance, try

   > f = sin(x)/x;
   > g = cos(y)-1;
   Warning: the identifier "y" is neither assigned to, nor bound to a library function nor external procedure, nor equal to the current free variable.
   Will interpret "y" as "x".
   > g;
   cos(x) - 1

Now, the name 'x' can only be used to refer to the free variable:

   > x = 3;
   Warning: the identifier "x" is already bound to the free variable, to a library function, library constant or to an external procedure.
   The command will have no effect.
   Warning: the last assignment will have no effect.

If you really want to unbind 'x', you can use the rename command and change the name of the free variable:

   > rename(x,y);
   Information: the free variable has been renamed from "x" to "y".
   > g;
   cos(y) - 1
   > x=3;
   > x;
   3

As you have seen, you can name functions and easily work with them. The basic thing to do with a function is to evaluate it at some point:

   > f(-2);
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   0.45464871341284084769800993295587242135112748572394
   > evaluate(f,-2);
   0.45464871341284084769800993295587242135112748572394

The printed value is generally a faithful rounding of the exact value at the working precision (i.e. one of the two floating-point numbers enclosing the exact value). Internally Sollya represents numbers as floating-point numbers in arbitrary precision with radix 2: the fact that a faithful rounding is performed in binary does not imply much on the exactness of the digits displayed in decimal. The working precision is controlled by the global variable prec:

   > prec;
   165
   > prec=200;
   The precision has been set to 200 bits.
   > prec;
   200
   > f(-2);
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   0.4546487134128408476980099329558724213511274857239451341894865

Sometimes a faithful rounding cannot easily be computed. In such a case, a value is printed that was obtained using floating-point approximations without control on the final accuracy:

   > log2(5)/log2(17) - log(5)/log(17);
   Warning: rounding may have happened.
   If there is rounding, the displayed value is *NOT* guaranteed to be a faithful rounding of the true result.
   0

The philosophy of Sollya is: Whenever something is not exact, print a warning. This explains the warnings in the previous examples. If the result can be shown to be exact, there is no warning:

   > sin(0);
   0

Let us finish this Section with a small complete example that shows a bit of what can be done with Sollya:

   > restart;
   The tool has been restarted.
   > prec=50;
   The precision has been set to 50 bits.
   > f=cos(2*exp(x));
   > d=[-1/8;1/8];
   > p=remez(f,2,d);
   > derivativeZeros = dirtyfindzeros(diff(p-f),d);
   > derivativeZeros = inf(d).:derivativeZeros:.sup(d);
   > maximum=0;
   > for t in derivativeZeros do {
   >    r = evaluate(abs(p-f), t);
   >    if r > maximum then { maximum=r; argmaximum=t; };
   > };
   > print("The infinity norm of", p-f, "is", maximum, "and is reached at", argmaximum);
   The infinity norm of -0.416265572875373 + x * (-1.798067209218835 + x * (-3.89710727747639e-2)) - cos(2 * exp(x)) is 8.630659443624325e-4 and is reached at -5.801672331417684e-2

In this example, we define a function f, an interval d and we compute the best degree-2 polynomial approximation of f on d with respect to the infinity norm. In other words, max {|p(x)-f(x)|, x in d} is minimal amongst polynomials with degree not greater than 2. Then, we compute the list of the zeros of the derivative of p-f and add the bounds of d to this list. Finally, we evaluate |p-f| for each point in the list and store the maximum and the point where it is reached. We conclude by printing the result in a formatted way.

Let us mention as a sidenote that you do not really need to use such a script for computing an infinity norm; as we will see, the command dirtyinfnorm does this for you.

3 - General principles

The first purpose of Sollya is to help people using numerical functions and numerical algorithms in a safe way. It is first designed to be used interactively but it can also be used in scripts (remark: some of the behaviors of Sollya slightly change when it is used in scripts. For example, no prompt is printed).

One of the particularities of Sollya is to work with multi-precision arithmetic (it uses the MPFR library). For safety purposes, Sollya knows how to use interval arithmetic. It uses interval arithmetic to produce tight and safe results with the precision required by the user.

The general philosophy of Sollya is: When you can perform a computation exactly and sufficiently quickly, do it; when you cannot, do not, unless you have been explicitly asked for.

The precision of the tool is set by the global variable prec. In general, the variable prec determines the precision of the outputs of commands: more precisely, the command will internally determine how much precision should be used during the computations in order to ensure that the output is a faithfully rounded result with prec bits.

For decidability and efficiency reasons, this general principle cannot be applied every time, so be careful. Moreover certain commands are known to be unsafe: they give in general excellent results and give almost prec correct bits in output for everyday examples. However they are merely based on heuristics and should not be used when the result must be safe. See the documentation of each command to know precisely how confident you can be with their result.

A second principle (that comes together with the first one) is the following one: When a computation leads to inexact results, inform the user with a warning. This can be quite irritating in some circumstances: in particular if you are using Sollya within other scripts. The global variable verbosity lets you change the level of verbosity of Sollya. When the variable is set to 0, Sollya becomes completely silent on standard output and prints only very important messages on standard error. Increase verbosity if you want more information about what Sollya is doing. Please keep in mind that when you affect a value to a global variable, a message is always printed even if verbosity is set to 0. In order to silently affect a global variable, use !:

   > prec=30;
   The precision has been set to 30 bits.
   > prec=30!;
   >

For conviviality reasons, values are displayed in decimal by default. This lets a normal human being understand the numbers they manipulate. But since constants are internally represented in binary, this causes permanent conversions that are sources of roundings. Thus you are loosing in accuracy and Sollya is always complaining about inexact results. If you just want to store or communicate your results (to another tools for instance) you can use bit-exact representations available in Sollya. The global variable display defines the way constants are displayed. Here is an example of the five available modes:

   > prec=30!;
   > a = 17.25;
   > display=decimal;
   Display mode is decimal numbers.
   > a;
   1.725e1
   > display=binary;
   Display mode is binary numbers.
   > a;
   1.000101_2 * 2^(4)
   > display=powers;
   Display mode is dyadic numbers in integer-power-of-2 notation.
   > a;
   69 * 2^(-2)
   > display=dyadic;
   Display mode is dyadic numbers.
   > a;
   69b-2
   > display=hexadecimal;
   Display mode is hexadecimal numbers.
   > a;
   0x1.14p4

Please keep in mind that it is possible to maintain the general verbosity level at some higher setting while deactivating all warnings on roundings. This feature is controlled using the roundingwarnings global variable. It may be set to on or off. By default, the warnings are activated (roundingwarnings = on) when Sollya is connected on standard input to a pseudo-file that represents a terminal. They are deactivated when Sollya is connected on standard input to a real file. See roundingwarnings for further details; the behavior is illustrated with examples there.

As always, the symbol e means (* 10^x). The same way the symbol b means (* 2^x). The symbol p means (* 16^x) and is used only with the 0x prefix. The prefix 0x indicates that the digits of the following number until a symbol p or white-space are hexadecimal. The suffix _2 indicates to Sollya that the previous number has been written in binary. Sollya can parse these notations even if you are not in the corresponding display mode, so you can always use them.

You can also use memory-dump hexadecimal notation frequently used to represent IEEE 754 double and single precision numbers. Since this notation does not allow for exactly representing numbers with arbitrary precision, there is no corresponding display mode. However, the commands printdouble respectively printsingle round the value to the nearest double respectively single. The number is then printed in hexadecimal as the integer number corresponding to the memory representation of the IEEE 754 double or single number:

   > printdouble(a);
   0x4031400000000000
   > printsingle(a);
   0x418a0000

Sollya can parse these memory-dump hexadecimal notation back in any display mode. The difference of this memory-dump notation with the hexadecimal notation (as defined above) is made by the presence or absence of a p indicator.

4 - Variables

As already explained, Sollya can manipulate variate functional expressions in one variable. These expressions contain a unique free variable the name of which is fixed by its first usage in an expression that is not a left-hand-side of an assignment. This global and unique free variable is a variable in the mathematical sense of the term.

Sollya also provides variables in the sense programming languages give to the term. These variables, which must be different in their name from the global free variable, may be global or declared and attached to a block of statements, i.e. a begin-end-block. These programming language variables may hold any object of the Sollya language, as for example functional expressions, strings, intervals, constant values, procedures, external functions and procedures, etc.

Global variables need not to be declared. They start existing, i.e. can be correctly used in expressions that are not left-hand-sides of assignments, when they are assigned a value in an assignment. Since they are global, this kind of variables is recommended only for small Sollya scripts. Larger scripts with code reuse should use declared variables in order to avoid name clashes for example in loop variables.

Declared variables are attached to a begin-end-block. The block structure builds scopes for declared variables. Declared variables in inner scopes shadow (global and declared) variables of outer scopes. The global free variable, i.e. the mathematical variable for variate functional expressions in one variable, cannot be shadowed. Variables are declared using the var keyword. See section var for details on its usage and semantic.

The following code examples illustrate the use of variables.

   > f = exp(x);
   > f;
   exp(x)
   > a = "Hello world";
   > a;
   Hello world
   > b = 5;
   > f(b);
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   1.48413159102576603421115580040552279623487667593878e2
   > {var b; b = 4; f(b); };
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   5.45981500331442390781102612028608784027907370386137e1
   > {var x; x = 3; };
   Warning: the identifier "x" is already bound to the current free variable.
   It cannot be declared as a local variable. The declaration of "x" will have no effect.
   Warning: the identifier "x" is already bound to the free variable, to a library function, library constant or to an external procedure.
   The command will have no effect.
   Warning: the last assignment will have no effect.
   > {var a, b; a=5; b=3; {var a; var b; b = true; a = 1; a; b;}; a; b; };
   1
   true
   5
   3
   > a;
   Hello world

Let us state that a variable identifier, just as every identifier in Sollya, contains at least one character, starts with a ASCII letter and continues with ASCII letters or numerical digits.

5 - Data types

Sollya has a (very) basic system of types. If you try to perform an illicit operation (such as adding a number and a string, for instance), you will get a typing error. Let us see the available data types.

5.1 - Booleans

There are two special values true and false. Boolean expressions can be constructed using the boolean connectors && (and), || (or), ! (not), and cosmparisons.

The comparison operators <, <=, > and >= can only be used between two numbers or constant expressions.

The comparison operators == and != are polymorphic. You can use them to compare any two objects, like two strings, two intervals, etc. As a matter of fact, polymorphism is allowed on both sides: it is possible to compare objects of different type. Such objects of different type, as they can never be syntactically equal, will always compare unequal (see exception for error, section error) and never equal. It is important to remember that testing the equality between two functions will return true if and only if the expression trees representing the two functions are exactly the same. See error for an exception concerning the special object error. Example:

   > 1+x==1+x;
   true

5.2 - Numbers

Sollya represents numbers as binary multi-precision floating-point values. For integer values and values in dyadic, binary, hexadecimal or memory dump notation, it automatically uses a precision needed for representing the value exactly (unless this behaviour is overridden using the syntax given below). Additionally, automatic precision adaption takes place for all integer values (even in decimal notation) written without the exponent sign e or with the exponent sign e and an exponent sufficiently small that they are less than 10^999. Otherwise the values are represented with the current precision prec. When a number must be rounded, it is rounded to the precision prec before the expression get evaluated:

   > prec=12!;
   > 4097.1;
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   4098
   > 4098.1;
   Warning: Rounding occurred when converting the constant "4098.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   4098
   > 4097.1+1;
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   4099

As a matter of fact, each variable has its own precision that corresponds to its intrinsic precision or, if it cannot be represented, to the value of prec when the variable was set. Thus you can work with variables having a precision higher than the current precision.

The same way, if you define a function that refers to some constant, this constant is stored in the function with the current precision and will keep this value in the future, even if prec becomes smaller.

If you define a function that refers to some variable, the precision of the variable is kept, independently of the current precision:

   > prec = 50!;
   > a = 4097.1;
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 50 bits.
   If safe computation is needed, try to increase the precision.
   > prec = 12!;
   > f = x + a;
   > g = x + 4097.1;
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   > prec = 120;
   The precision has been set to 120 bits.
   > f;
   4.097099999999998544808477163314819335e3 + x
   > g;
   4098 + x

In some rare cases, it is necessary to read in decimal constants with a particular precision being used in the conversion to the binary floating-point format, which Sollya uses. Setting prec to that precision may prove to be an insufficient means for doing so, for example when several different precisions have to be used in one expression. For these rare cases, Sollya provides the following syntax: decimal constants may be written %precision%constant, where precision is a constant integer, written in decimal, and constant is the decimal constant. Sollya will convert the constant constant with precision precision, regardless of the global variable prec and regardless if constant is an integer or would otherwise be representable.

   > prec = 24;
   The precision has been set to 24 bits.
   > a = 0.1;
   Warning: Rounding occurred when converting the constant "0.1" to floating-point with 24 bits.
   If safe computation is needed, try to increase the precision.
   > b = 33554433;
   > prec = 64;
   The precision has been set to 64 bits.
   > display = binary;
   Display mode is binary numbers.
   > a;
   1.10011001100110011001101_2 * 2^(-4)
   > 0.1;
   Warning: Rounding occurred when converting the constant "0.1" to floating-point with 64 bits.
   If safe computation is needed, try to increase the precision.
   1.100110011001100110011001100110011001100110011001100110011001101_2 * 2^(-4)
   > %24%0.1;
   Warning: Rounding occurred when converting the constant "0.1" to floating-point with 24 bits.
   If safe computation is needed, try to increase the precision.
   1.10011001100110011001101_2 * 2^(-4)
   > c = 33554433;
   > b;
   1.0000000000000000000000001_2 * 2^(25)
   > c;
   1.0000000000000000000000001_2 * 2^(25)
   > %24%33554433;
   Warning: Rounding occurred when converting the constant "33554433" to floating-point with 24 bits.
   If safe computation is needed, try to increase the precision.
   1_2 * 2^(25)
   >
   >

Sollya is an environment that uses floating-point arithmetic. The IEEE 754-2008 standard on floating-point arithmetic does not only define floating-point numbers that represent real numbers but also floating-point data representing infinities and Not-a-Numbers (NaNs). Sollya also supports infinities and NaNs in the spirit of the IEEE 754-2008 standard without taking the standard's choices literally.

The evaluation of an expression involving a NaN or the evaluation of a function at a point being NaN always results in a NaN.

Infinities are considered to be the limits of expressions tending to infinity. They are supported as bounds of intervals in some cases. However, particular commands might prohibit their use even though there might be a mathematical meaning attached to such expressions. For example, while Sollya will evaluate expressions such as the limit of e^x when x goes to -infinity, expressed e.g. through evaluate(exp(x),[-infty;0]), it will not accept to compute the (finite) value of the integral of e^x between -infinity and 0.

The following examples give an idea of what can be done with Sollya infinities and NaNs. Here is what can be done with infinities:

   > f = exp(x) + 5;
   > f(-infty);
   5
   > evaluate(f,[-infty;infty]);
   [5;@Inf@]
   > f(infty);
   Warning: the given expression is undefined or numerically unstable.
   @NaN@
   > [-infty;5] * [3;4];
   [-@Inf@;20]
   > -infty < 5;
   true
   > log(0);
   Warning: the given expression is undefined or numerically unstable.
   @NaN@
   > [log(0);17];
   Warning: the given expression is not a constant but an expression to evaluate
   and a faithful evaluation is not possible.
   Will use a plain floating-point evaluation, which might yield a completely wrong value.
   Warning: inclusion property is satisfied but the diameter may be greater than the least possible.
   [-@Inf@;17]
   >

And the following example illustrates NaN behavior.

   > 3/0;
   Warning: the given expression is undefined or numerically unstable.
   @NaN@
   > (-3)/0;
   Warning: the given expression is undefined or numerically unstable.
   @NaN@
   > infty/infty;
   Warning: the given expression is undefined or numerically unstable.
   @NaN@
   > infty + infty;
   Warning: the given expression is undefined or numerically unstable.
   @Inf@
   > infty - infty;
   Warning: the given expression is undefined or numerically unstable.
   @NaN@
   > f = exp(x) + 5;
   > f(NaN);
   @NaN@
   > NaN == 5;
   false
   > NaN == NaN;
   false
   > NaN != NaN;
   false
   > X = "Vive la Republique!";
   > !(X == X);
   false
   > X = 5;
   > !(X == X);
   false
   > X = NaN;
   > !(X == X);
   true
   >

5.3 - Rational numbers and rational arithmetic

The Sollya tool is mainly based on floating-point arithmetic: wherever possible, floating-point algorithms, including algorithms using interval arithmetic, are used to produce approximate but safe results. For some particular cases, floating-point arithmetic is not sufficient: some algorithms just require natural and rational numbers to be handled exactly. More importantly, for these applications, it is required that rational numbers be displayed as such.

Sollya implements a particular mode that offers a lightweight support for rational arithmetic. When needed, it can be enabled by assigning on to the global variable rationalmode. It is disabled by assigning off; the default is off.

When the mode for rational arithmetic is enabled, Sollya's behavior will change as follows:

Even when rationalmode is on, Sollya will not be able to exhibit integer ratios between transcendental quantities. For example, Sollya will not display 1/6 for arcsin(1/2)/pi but 0.16666... Sollya's evaluator for rational arithmetic is only able to simplify rational expressions based on addition, subtraction, multiplication, division, negation, perfect squares (for square root) and integer powers.

The following example illustrates what can and what cannot be done with Sollya's mode for rational arithmetic:

   > 1/3 - 1/7;
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   0.19047619047619047619047619047619047619047619047619
   > rationalmode = on;
   Rational mode has been activated.
   > 1/3 - 1/7;
   4 / 21
   > (2 + 1/7)^2 + (6/7)^2 + 2 * (2 + 1/7) * 6/7;
   9
   > rationalmode = off;
   Rational mode has been deactivated.
   > (2 + 1/7)^2 + (6/7)^2 + 2 * (2 + 1/7) * 6/7;
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   9
   > rationalmode = on;
   Rational mode has been activated.
   > asin(1)/pi;
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   0.5
   > sin(1/6 * pi);
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   0.5
   > exp(1/7 - 3/21) / 7;
   1 / 7
   > rationalmode = off;
   Rational mode has been deactivated.
   > exp(1/7 - 3/21) / 7;
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   0.142857142857142857142857142857142857142857142857145
   > print(1/7 - 3/21);
   1 / 7 - 3 / 21
   > rationalmode = on;
   Rational mode has been activated.
   > print(1/7 - 3/21);
   0

5.4 - Intervals and interval arithmetic

Sollya can manipulate intervals that are closed subsets of the real numbers. Several ways of defining intervals exist in Sollya. There is the most common way where intervals are composed of two numbers or constant expressions representing the lower and the upper bound. These values are separated either by commas or semi-colons. Interval bound evaluation is performed in a way that ensures the inclusion property: all points in the original, unevaluated interval will be contained in the interval with its bounds evaluated to floating-point numbers.

   > d=[1;2];
   > d2=[1,1+1];
   > d==d2;
   true
   > prec=12!;
   > 8095.1;
   Warning: Rounding occurred when converting the constant "8095.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   8096
   > [8095.1; 8096.1];
   Warning: Rounding occurred when converting the constant "8095.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   Warning: Rounding occurred when converting the constant "8096.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   [8094;8098]

Sollya has a mode for printing intervals that are that thin that their bounds have a number of decimal digits in common when printed. That mode is called midpointmode; see below for an introduction and section midpointmode for details. As Sollya must be able to parse back its own output, a syntax is provided to input intervals in midpoint mode. However, please pay attention to the fact that the notation used in midpoint mode generally increases the width of intervals: hence when an interval is displayed in midpoint mode and read again, the resulting interval may be wider than the original interval.

   > midpointmode = on!;
   > [1.725e4;1.75e4];
   0.17~2/5~e5
   > 0.17~2/5~e5;
   0.17~2/5~e5
   > midpointmode = off!;
   > 0.17~2/5~e5;
   [17200;17500]

In some cases, intervals become infinitely thin in theory, in which case one tends to think of point intervals even if their floating-point representation is not infinitely thin. Sollya provides a very covenient way for input of such point intervals. Instead of writing [a;a], it is possible to just write [a]. Sollya will expand the notation while making sure that the inclusion property is satisfied:

   > [3];
   [3;3]
   > [1/7];
   Warning: the given expression is not a constant but an expression to evaluate. A faithful evaluation will be used.
   [0.14285713;0.14285716]
   > [exp(8)];
   Warning: the given expression is not a constant but an expression to evaluate. A faithful evaluation will be used.
   [2.980957e3;2.9809589e3]

When the mode midpointmode is set to on (see midpointmode), Sollya will display intervals that are provably reduced to one point in this extended interval syntax. It will use midpointmode syntax for intervals that are sufficiently thin but not reduced to one point (see section midpointmode for details):

   > midpointmode = off;
   Midpoint mode has been deactivated.
   > [17;17];
   [17;17]
   > [exp(pi);exp(pi)];
   Warning: the given expression is not a constant but an expression to evaluate. A faithful evaluation will be used.
   [2.31406926327792690057290863679485473802661062425987e1;2.31406926327792690057290863679485473802661062426015e1]
   > midpointmode = on;
   Midpoint mode has been activated.
   > [17;17];
   [17]
   > [exp(pi);exp(pi)];
   Warning: the given expression is not a constant but an expression to evaluate. A faithful evaluation will be used.
   0.23140692632779269005729086367948547380266106242~5/7~e2
   >

Sollya intervals are internally represented with floating-point numbers as bounds; rational numbers are not supported here. If bounds are defined by constant expressions, these are evaluated to floating-point numbers using the current precision. Numbers or variables containing numbers keep their precision for the interval bounds.

Constant expressions get evaluated to floating-point values immediately; this includes pi and rational numbers, even when rationalmode is on (see section Rational numbers and rational arithmetic for this mode).

   > prec = 300!;
   > a = 4097.1;
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 300 bits.
   If safe computation is needed, try to increase the precision.
   > prec = 12!;
   > d = [4097.1; a];
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   > prec = 300!;
   > d;
   [4096;4.0971e3]
   > prec = 30!;
   > [-pi;pi];
   Warning: the given expression is not a constant but an expression to evaluate. A faithful evaluation will be used.
   Warning: the given expression is not a constant but an expression to evaluate. A faithful evaluation will be used.
   [-3.141592659;3.141592659]

You can get the upper-bound (respectively the lower-bound) of an interval with the command sup (respectively inf). The middle of the interval can be computed with the command mid. Let us also mention that these commands can also be used on numbers (in that case, the number is interpreted as an interval containing only one single point. In that case the commands inf, mid and sup are just the identity):

   > d=[1;3];
   > inf(d);
   1
   > mid(d);
   2
   > sup(4);
   4

Let us mention that the mid operator never provokes a rounding. It is rewritten as an unevaluated expression in terms of inf and sup.

Sollya permits intervals to also have non-real bounds, such as infinities or NaNs. When evaluating certain expressions, in particular given as interval bounds, Sollya will itself generate intervals containing infinities or NaNs. When evaluation yields an interval with a NaN bound, the given expression is most likely undefined or numerically unstable. Such results should not be trusted; a warning is displayed.

While computations on intervals with bounds being NaN will always fail, Sollya will try to interpret infinities in the common way as limits. However, this is not guaranteed to work, even if it is guaranteed that no unsafe results will be produced. See also section Numbers for more detail on infinities in Sollya. The behavior of interval arithmetic on intervals containing infinities or NaNs is subject to debate; moreover, there is no complete consensus on what should be the result of the evaluation of a function f over an interval I containing points where f is not defined. Sollya has its own philosophy regarding these questions. This philosophy is explained in Appendix 9 at the end of this document.

   > evaluate(exp(x),[-infty;0]);
   [0;1]
   > dirtyinfnorm(exp(x),[-infty;0]);
   Warning: a bound of the interval is infinite or NaN.
   This command cannot handle such intervals.
   @NaN@
   >
   > f = log(x);
   > [f(0); f(1)];
   Warning: the given expression is not a constant but an expression to evaluate
   and a faithful evaluation is not possible.
   Will use a plain floating-point evaluation, which might yield a completely wrong value.
   Warning: inclusion property is satisfied but the diameter may be greater than the least possible.
   [-@Inf@;0]
   >

Sollya internally uses interval arithmetic extensively to provide safe answers. In order to provide for algorithms written in the Sollya language being able to use interval arithmetic, Sollya offers native support of interval arithmetic. Intervals can be added, subtracted, multiplied, divided, raised to powers, for short, given in argument to any Sollya function. The tool will apply the rules of interval arithmetic in order to compute output intervals that safely encompass the hull of the image of the function on the given interval:

   > [1;2] + [3;4];
   [4;6]
   > [1;2] * [3;4];
   [3;8]
   > sqrt([9;25]);
   [3;5]
   > exp(sin([10;100]));
   [0.36787942;2.7182819]

When such expressions involving intervals are given, Sollya will follow the rules of interval arithmetic in precision prec for immediately evaluating them to interval enclosures. While Sollya's evaluator always guarantees the inclusion property, it also applies some optimisations in some cases in order to make the image interval as thin as possible. For example, Sollya will use a Taylor expansion based evaluation if a composed function, call it f, is applied to an interval. In other words, in this case Sollya will behave as if the evaluate command (see section evaluate) were implicitly used. In most cases, the result will be different from the one obtained by replacing all occurences of the free variable of a function by the interval the function is to be evaluated on:

   > f = x - sin(x);
   > [-1b-10;1b-10] - sin([-1b-10;1b-10]);
   [-1.95312484477957829894e-3;1.95312484477957829894e-3]
   > f([-1b-10;1b-10]);
   [-1.55220421701117626897e-10;1.55220421701117626897e-10]
   > evaluate(f,[-1b-10;1b-10]);
   [-1.55220421701117626897e-10;1.55220421701117626897e-10]

5.5 - Functions

Sollya knows only about functions with one single variable. The first time in a session that an unbound name is used (without being assigned) it determines the name used to refer to the free variable.

The basic functions available in Sollya are the following:

The constant pi is available through the keyword pi as a 0-ary function:

   > display=binary!;
   > prec=12!;
   > a=pi;
   > a;
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   1.10010010001_2 * 2^(1)
   > prec=30!;
   > a;
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   1.10010010000111111011010101001_2 * 2^(1)

The reader may wish to see Sections library and function for ways of dynamically adding other base functions to Sollya.

5.6 - Strings

Anything written between quotes is interpreted as a string. The infix operator @ concatenates two strings. To get the length of a string, use the length function. You can access the i-th character of a string using brackets (see the example below). There is no character type in Sollya: the i-th character of a string is returned as a string itself.

   > s1 = "Hello "; s2 = "World!";
   > s = s1@s2;
   > length(s);
   12
   > s[0];
   H
   > s[11];
   !

Strings may contain the following escape sequences: \\, \“, \?, \', \n, \t, \a, \b, \f, \r, \v, \x[hexadecimal number] and \[octal number]. Refer to the C99 standard for their meaning.

5.7 - Particular values

Sollya knows about some particular values. These values do not really have a type. They can be stored in variables and in lists. A (possibly not exhaustive) list of such values is the following one:

5.8 - Lists

Objects can be grouped into lists. A list can contain elements with different types. As for strings, you can concatenate two lists with @. The function length also gives the length of a list.

You can prepend an element to a list using .: and you can append an element to a list using :.\\ The following example illustrates some features:

   > L = [| "foo" |];
   > L = L:.1;
   > L = "bar".:L;
   > L;
   [|"bar", "foo", 1|]
   > L[1];
   foo
   > L@L;
   [|"bar", "foo", 1, "bar", "foo", 1|]

Lists can be considered arrays and elements of lists can be referenced using brackets. Possible indices start at 0. The following example illustrates this point:

   > L = [|1,2,3,4,5|];
   > L;
   [|1, 2, 3, 4, 5|]
   > L[3];
   4

Please be aware of the fact that the complexity for accessing an element of the list using indices is O(n), where n is the length of the whole list.

Lists may contain ellipses indicated by ,..., between elements that are constant and evaluate to integers that are incrementally ordered. Sollya translates such ellipses to the full list upon evaluation. The use of ellipses between elements that are not constants is not allowed. This feature is provided for ease of programming; remark that the complexity for expanding such lists is high. For illustration, see the following example:

   > [|1,...,5|];
   [|1, 2, 3, 4, 5|]
   > [|-5,...,5|];
   [|-5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5|]
   > [|3,...,1|];
   Warning: at least one of the given expressions or a subexpression is not correctly typed
   or its evaluation has failed because of some error on a side-effect.
   error
   > [|true,...,false|];
   Warning: at least one of the given expressions or a subexpression is not correctly typed
   or its evaluation has failed because of some error on a side-effect.
   error

Lists may be continued to infinity by means of the ... indicator after the last element given. At least one element must explicitly be given. If the last element given is a constant expression that evaluates to an integer, the list is considered as continued to infinity by all integers greater than that last element. If the last element is another object, the list is considered as continued to infinity by re-duplicating this last element. Let us remark that bracket notation is supported for such end-elliptic lists even for implicitly given elements. However, evaluation complexity is high. Combinations of ellipses inside a list and in its end are possible. The usage of lists described here is best illustrated by the following examples:

   > L = [|1,2,true,3...|];
   > L;
   [|1, 2, true, 3...|]
   > L[2];
   true
   > L[3];
   3
   > L[4];
   4
   > L[1200];
   1200
   > L = [|1,...,5,true...|];
   > L;
   [|1, 2, 3, 4, 5, true...|]
   > L[1200];
   true

5.9 - Structures

In a similar way as in lists, Sollya allows data to be grouped in - untyped - structures. A structure forms an object to which other objects can be added as elements and identified by their names. The elements of a structure can be retrieved under their name and used as usual. The following sequence shows that point:

   > s.a = 17;
   > s.b = exp(x);
   > s.a;
   17
   > s.b;
   exp(x)
   > s.b(1);
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   2.71828182845904523536028747135266249775724709369998
   > s.d.a = [-1;1];
   > s.d.b = sin(x);
   > inf(s.d.a);
   -1
   > diff(s.d.b);
   cos(x)

Structures can also be defined literally using the syntax illustrated in the next example. They will also be printed in that syntax.

   > a = { .f = exp(x), .dom = [-1;1] };
   > a;
   { .f = exp(x), .dom = [-1;1] }
   > a.f;
   exp(x)
   > a.dom;
   [-1;1]
   > b.f = sin(x);
   > b.dom = [-1b-5;1b-5];
   > b;
   { .dom = [-3.125e-2;3.125e-2], .f = sin(x) }
   > { .f = asin(x), .dom = [-1;1] }.f(1);
   Warning: rounding has happened. The value displayed is a faithful rounding of the true result.
   1.57079632679489661923132169163975144209858469968754

If the variable a is bound to an existing structure, it is possible to use the ``dot notation'' a.b to assign the value of the field b of the structure a. This works even if b is not yet a field of a: in this case a new field is created inside the structure a.

Besides, the dot notation can be used even when a is unassigned. In this case a new structure is created with a field b, and this structure is bound to a. However, the dot notation cannot be used if a is already bound to something that is not a structure.

These principles apply recursively: for instance, if a is a structure that contains only one field d, the command a.b.c = 3 creates a new field named b inside the structure a; this field itself is a structure containing the field c. The command a.d.c = 3 is allowed if a.d is already a structure, but forbidden otherwise (e.g. if a.d was equal to sin(x)). This is summed up in the following example.

   > restart;
   The tool has been restarted.
   > a.f = exp(x);
   > a.dom = [-1;1];
   > a.info.text = "My akrnoximation problem";
   > a;
   { .info = { .text = "My akrnoximation problem" }, .dom = [-1;1], .f = exp(x) }
   >
   > a.info.text = "My approximation problem";
   > a;
   { .info = { .text = "My approximation problem" }, .dom = [-1;1], .f = exp(x) }
   >
   > b = exp(x);
   > b.a = 5;
   Warning: cannot modify an element of something that is not a structure.
   Warning: the last assignment will have no effect.
   > b;
   exp(x)
   >
   > a.dom.a = -1;
   Warning: cannot modify an element of something that is not a structure.
   Warning: the last assignment will have no effect.
   > a;
   { .info = { .text = "My approximation problem" }, .dom = [-1;1], .f = exp(x) }

When printed, the elements of a structure are not sorted in any manner. They get printed in an arbitrary order that just maintains the order given in the definition of literate structures. That said, when compared, two structures compare equal iff they contain the same number of identifiers, with the same names and iff the elements of corresponding names all compare equal. This means the order does not matter in comparisons and otherwise does only for printing.

The following example illustrates this matter:

   > a = { .f = exp(x), .a = -1, .b = 1 };
   > a;
   { .f = exp(x), .a = -1, .b = 1 }
   > a.info = "My function";
   > a;
   { .info = "My function", .f = exp(x), .a = -1, .b = 1 }
   >
   > b = { .a = -1, .f = exp(x), .info = "My function", .b = 1 };
   > b;
   { .a = -1, .f = exp(x), .info = "My function", .b = 1 }
   >
   > a == b;
   true
   >
   > b.info = "My other function";
   > a == b;
   false
   >
   > b.info = "My function";
   > a == b;
   true
   > b.something = true;
   > a == b;
   false

6 - Iterative language elements: assignments, conditional statements and loops

6.1 - Blocks

Statements in Sollya can be grouped in blocks, so-called begin-end-blocks. This can be done using the key tokens { and }. Blocks declared this way are considered to be one single statement. As already explained in section Variables, using begin-end-blocks also opens the possibility of declaring variables through the keyword var.

6.2 - Assignments

Sollya has two different assignment operators, = and :=. The assignment operator = assigns its right-hand-object ``as is'', i.e. without evaluating functional expressions. For instance, i = i + 1; will dereferentiate the identifier i with some content, notate it y, build up the expression (function) y + 1 and assign this expression back to i. In the example, if i stood for the value 1000, the statement i = i + 1; would assign ``1000 + 1'' -- and not ``1001'' -- to i. The assignment operator := evaluates constant functional expressions before assigning them. On other expressions it behaves like =. Still in the example, the statement i := i + 1; really assigns 1001 to i.

Both Sollya assignment operators support indexing of lists or strings elements using brackets on the left-hand-side of the assignment operator. The indexed element of the list or string gets replaced by the right-hand-side of the assignment operator. When indexing strings this way, that right-hand side must evaluate to a string of length 1. End-elliptic lists are supported with their usual semantic for this kind of assignment. When referencing and assigning a value in the implicit part of the end-elliptic list, the list gets expanded to the corresponding length.

The following examples well illustrate the behavior of assignment statements:

   > autosimplify = off;
   Automatic pure tree simplification has been deactivated.
   > i = 1000;
   > i = i + 1;
   > print(i);
   1000 + 1
   > i := i + 1;
   > print(i);
   1002
   > L = [|1,...,5|];
   > print(L);
   [|1, 2, 3, 4, 5|]
   > L[3] = L[3] + 1;
   > L[4] := L[4] + 1;
   > print(L);
   [|1, 2, 3, 4 + 1, 6|]
   > L[5] = true;
   > L;
   [|1, 2, 3, 5, 6, true|]
   > s = "Hello world";
   > s;
   Hello world
   > s[1] = "a";
   > s;
   Hallo world
   > s[2] = "foo";
   Warning: the string to be assigned is not of length 1.
   This command will have no effect.
   > L = [|true,1,...,5,9...|];
   > L;
   [|true, 1, 2, 3, 4, 5, 9...|]
   > L[13] = "Hello";
   > L;
   [|true, 1, 2, 3, 4, 5, 9, 10, 11, 12, 13, 14, 15, "Hello"...|]

The indexing of lists on left-hand sides of assignments is reduced to the first order. Multiple indexing of lists of lists on assignment is not supported for complexity reasons. Multiple indexing is possible in right-hand sides.

   > L = [| 1, 2, [|"a", "b", [|true, false|] |] |];
   > L[2][2][1];
   false
   > L[2][2][1] = true;
   Warning: the first element of the left-hand side is not an identifier.
   This command will have no effect.
   > L[2][2] = "c";
   Warning: the first element of the left-hand side is not an identifier.
   This command will have no effect.
   > L[2] = 3;
   > L;
   [|1, 2, 3|]

6.3 - Conditional statements

Sollya supports conditional statements expressed with the keywords if, then and optionally else. Let us mention that only conditional statements are supported and not conditional expressions.

The following examples illustrate both syntax and semantic of conditional statements in Sollya. Concerning syntax, be aware that there must not be any semicolon before the else keyword.

   > a = 3;
   > b = 4;
   > if (a == b) then print("Hello world");
   > b = 3;
   > if (a == b) then print("Hello world");
   Hello world
   > if (a == b) then print("You are telling the truth") else print("Liar!");
   You are telling the truth

6.4 - Loops

Sollya supports three kinds of loops. General while-condition loops can be expressed using the keywords while and do. One has to be aware of the fact that the condition test is executed always before the loop, there is no do-until-condition loop. Consider the following examples for both syntax and semantic:

   > verbosity = 0!;
   > prec = 30!;
   > i = 5;
   > while (expm1(i) > 0) do { expm1(i); i := i - 1; };
   1.474131591e2
   5.359815e1
   1.908553692e1
   6.3890561
   1.718281827
   > print(i);
   0

The second kind of loops are loops on a variable ranging from a numerical start value and a end value. These kind of loops can be expressed using the keywords for, from, to, do and optionally by. The by statement indicates the width of the steps on the variable from the start value to the end value. Once again, syntax and semantic are best explained with an example:

   > for i from 1 to 5 do print ("Hello world",i);
   Hello world 1
   Hello world 2
   Hello world 3
   Hello world 4
   Hello world 5
   > for i from 2 to 1 by -0.5 do print("Hello world",i);
   Hello world 2
   Hello world 1.5
   Hello world 1

The third kind of loops are loops on a variable ranging on values contained in a list. In order to ensure the termination of the loop, that list must not be end-elliptic. The loop is expressed using the keywords for, in and do as in the following examples:

   > L = [|true, false, 1,...,4, "Hello", exp(x)|];
   > for i in L do i;
   true
   false
   1
   2
   3
   4
   Hello
   exp(x)

For both types of for loops, assigning the loop variable is allowed and possible. When the loop terminates, the loop variable will contain the value that made the loop condition fail. Consider the following examples:

   > for i from 1 to 5 do { if (i == 3) then i = 4 else i; };
   1
   2
   5
   > i;
   6

7 - Functional language elements: procedures

Sollya has some elements of functional languages. In order to avoid confusion with mathematical functions, the associated programming objects are called procedures in Sollya.

Sollya procedures are common objects that can be, for example, assigned to variables or stored in lists. Procedures are declared by the proc keyword; see section proc for details. The returned procedure object must then be assigned to a variable. It can hence be applied to arguments with common application syntax. The procedure keyword provides an abbreviation for declaring and assigning a procedure; see section procedure for details.

Sollya procedures can return objects using the return keyword at the end of the begin-end-block of the procedure. Section return gives details on the usage of return. Procedures further can take any type of object in argument, in particular also other procedures that are then applied to arguments. Procedures can be declared inside other procedures.

Common Sollya procedures are declared with a certain number of formal parameters. When the procedure is applied to actual parameters, a check is performed if the right number of actual parameters is given. Then the actual parameters are applied to the formal parameters. In some cases, it is required that the number of parameters of a procedure be variable. Sollya provides support for the case with procedures with an arbitrary number of actual arguments. When the procedure is called, those actual arguments are gathered in a list which is applied to the only formal list parameter of a procedure with an arbitrary number of arguments. See section procedure for the exact syntax and details; an example is given just below.

Let us remark that declaring a procedure does not involve any evaluation or other interpretation of the procedure body. In particular, this means that constants are evaluated to floating-point values inside Sollya when the procedure is applied to actual parameters and the global precision valid at this moment.

Sollya procedures are well illustrated with the following examples:

   > succ = proc(n) { return n + 1; };
   > succ(5);
   6
   > 3 + succ(0);
   4
   > succ;
   proc(n)
   {
   nop;
   return (n) + (1);
   }

   > add = proc(m,n) { var res; res := m + n; return res; };
   > add(5,6);
   11
   > hey = proc() { print("Hello world."); };
   > hey();
   Hello world.
   > print(hey());
   Hello world.
   void
   > hey;
   proc()
   {
   print("Hello world.");
   return void;
   }

   > fac = proc(n) { var res; if (n == 0) then res := 1 else res := n * fac(n - 1); return res; };
   > fac(5);
   120
   > fac(11);
   39916800
   > fac;
   proc(n)
   {
   var res;
   if (n) == (0) then
   res := 1
   else
   res := (n) * (fac((n) - (1)));
   return res;
   }

   > sumall = proc(args = ...) { var i, acc; acc = 0; for i in args do acc = acc + i; return acc; };
   > sumall;
   proc(args = ...)
   {
   var i, acc;
   acc = 0;
   for i in args do
   acc = (acc) + (i);
   return acc;
   }
   > sumall();
   0
   > sumall(1);
   1
   > sumall(1,5);
   6
   > sumall(1,5,9);
   15
   > sumall @ [|1,5,9,4,8|];
   27
   >

Sollya also supports external procedures, i.e. procedures written in C (or some other language) and dynamically bound to Sollya identifiers. See externalproc for details.

8 - Commands and functions

The list of commands of Sollya is available in two flavours:

9 - Appendix: interval arithmetic philosophy in Sollya

Although it is currently based on the MPFI library, Sollya has its own way of interpreting interval arithmetic when infinities or NaN occur, or when a function is evaluated on an interval containing points out of its domain, etc. This philosophy may differ from the one applied in MPFI. It is also possible that the behavior of Sollya does not correspond to the behavior that one would expect, e.g. as a natural consequence of the IEEE-754 standard.

The topology that we consider is always the usual topology of R bar: R U {-infinity, +infinity}. For any function, if one of its arguments is empty (respectively NaN), we return empty (respectively NaN).

9.1 - Univariate functions

Let f be a univariate basic function and I an interval. We denote by J the result of the interval evaluation of f over I in Sollya. If I is completely included in the domain of f, J will usually be the smallest interval (at the current precision) containing the exact image f(I) However, in some cases, it may happen that J is not as small as possible. It is guaranteed however, that J tends to f(I) when the precision of the tool tends to infinity.

When f is not defined at some point x but is defined on a neighborhood of x, we consider that the ``value'' of f at x is the convex hull of the limit points of f around x. For instance, consider the evaluation of f= tan on [0, Pi]. It is not defined at Pi/2 (and only at this point). The limit points of f around Pi/2 are -infinity and +infinity, so, we return [-infinity, +infinity]. Another example: f=sin on [+infinity]. The function has no limit at this point, but all points of [-1, 1] are limit points. So, we return [-1,1].

Finally, if I contains a subinterval on which f is not defined, we return [NaN, NaN] (example: sqrt([-1, 2])).

9.2 - Bivariate functions

Let f be a bivariate function and I1 and I2 be intervals. If I1=[x] and I2=[y] are both point-intervals, we return the convex hull of the limit points of f around (x, y) if it exists. In particular, if f is defined at (x, y) we return its value (or a small interval around it, if it is not exactly representable). As an example [1]/[+infinity] returns [0]. Also, [1]/[0] returns [-infinity, +infinity] (note that Sollya does not consider signed zeros). If it is not possible to give a meaning to the expression f(I1, I2), we return NaN: for instance [0]/[0] or [0]*[+infinity].

If one and only one of the intervals is a point-interval (say I1 = [x]), we consider the partial function g: y -> f(x,y) and return the value that would be obtained when evaluating g on I2. For instance, in order to evaluate [0]/I2, we consider the function g defined for every y != 0 by g(y)=0/y=0. Hence, g(I2) = [0] (even if I2 contains 0, by the argument of limit-points). In particular, please note that [0]/[-1, 1] returns [0] even though [0]/[0] returns NaN. This rule even holds when g can only be defined as limit points: for instance, in the case I1/[0] we consider g: x -> x/0. This function cannot be defined stricto sensu, but we can give it a meaning by considering 0 as a limit. Hence g is multivalued and its value is {-infinity, +infinity} for every x. Hence, I1/[0] returns [-infinity, +infinity] when I1 is not a point-interval.

Finally, if neither I1 nor I2 are point-intervals, we try to give a meaning to f(I1, I2) by an argument of limit-points when possible. For instance [1, 2] / [0, 1] returns [1, +infinity].

As a special exception to these rules, [0]^[0] returns [1].