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.
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.
GMP
MPFR
MPFI
fplll
libxml2
gnuplot (external tool)
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).
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:
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:
--donotmodifystacksize: When invoked, Sollya trys to increase
the stack size that is available to a user process to the maximum size
supported by the kernel. On some systems, the correspondent ioctl
does not work properly. Use the option to prevent Sollya from changing the
stack size.
--flush: When this option is given, Sollya will flush
all its input and output buffers after parsing and executing each
command resp. sequence of commands. This option is needed when pipes
are used to communicate with Sollya from another program.
--help: Prints help on the usage of the tool and quits.
--nocolor: Sollya supports coloring of the output
using ANSI X3.64/ ISO/IEC 6429 escape sequences. Coloring is
deactivated when Sollya is connected on standard input to a file
that is not a terminal. This option forces the deactivation of ANSI
coloring. This might be necessary on very old grey-scale terminals or when
encountering problems with old versions of rlwrap.
--noprompt: Sollya prints a prompt symbol when
connected on standard input to a pseudo-file that is a terminal. The
option deactivates the prompt.
--oldautoprint: The behaviour of an undocumented
feature for displaying values has changed in Sollya from version 1.1
to version 2.0. The old feature is deprecated. If you wish to use it
nevertheless, use this deprecated option.
--oldrlwrapcompatible: This option is deprecated. It
makes Sollya emit a non ANSI X3.64 compliant coloring escape
sequence for making it compatible with versions of rlwrap
that do not support the -A option. The option is considered
a hack since it is known to garble the output of the tool under
some particular circumstances.
--warninfile[append] <file>: Normally, Sollya emits
warning and information messages together with all other displayed
information on either standard output or standard error. This option
allows all warning and information messages to get redirected to a
file. The filename to be used must be given after the option. When
--warninfile is used, the existing content (if any) of the
file is first removed before writing to the file. With
--warninfileappend, the messages are appended to an
existing file. Even if coloring is used for the displaying all other
Sollya output, no coloring sequences are ever written to the
file. Let us emphasize on the fact that any file of a unixoid system
can be used for output, for instance also a named pipe. This allows
for error messaging to be performed on a separate terminal. The use
of this option is mutually exclusive with the
--warnonstderr option.
--warnonstderr: Normally, Sollya prints warning and
information messages on standard output, using a warning color
when coloring is activated. When this option is given, Sollya will
output all warning and information messages on standard error. Coloring
will be used even on standard error, when activated. The use of
this option is mutually exclusive with the --warninfile[append]
option.
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:
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
Now, the name 'x' can only be used to refer to the free variable:
If you really want to unbind 'x', you can use the rename command and change the name of the free variable:
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:
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:
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:
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:
Let us finish this Section with a small complete example that shows a bit of what can be done with Sollya:
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.
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 !:
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:
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:
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.
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.
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.
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.
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:
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:
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:
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.
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.
infty, -infty, @Inf@ and -@Inf@.
NaN and @NaN@. Sollya does not have support for NaN
payloads, signaling or quiet NaNs or signs of NaNs. Signaling NaNs
are supported on input for single and double precision memory
notation (see section General Principles). However, they
immediately get converted to plain Sollya NaNs.
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:
And the following example illustrates NaN behavior.
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:
autosimplify is on, which is
the default, Sollya will additionally use rational arithmetic while
trying to simplify expressions given in argument of commands.
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:
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.
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.
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:
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):
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).
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):
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.
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:
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:
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:
+, -, *, /, ^
sqrt
abs
sin, cos, tan, sinh, cosh, tanh
asin, acos, atan, asinh, acosh, atanh
exp, expm1 (defined as expm1(x) = exp(x)-1)
log (natural logarithm), log2 (binary logarithm), log10 (decimal logarithm), log1p (defined as log1p(x) = log(1+x))
erf, erfc
single, double, doubleextended, doubledouble, tripledouble (see sections single, double, doubleextended, doubledouble and tripledouble)
SG, D, DE, DD, TD (see sections single, double, doubleextended, doubledouble and tripledouble)
floor, ceil, nearestint.
The constant pi is available through the keyword pi as a 0-ary function:
The reader may wish to see Sections library and function for ways of dynamically adding other base functions to Sollya.
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.
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.
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:
on, off (see sections on and off)
dyadic, powers, binary, decimal, hexadecimal (see sections dyadic, powers, binary, decimal and hexadecimal)
file, postscript, postscriptfile (see sections file, postscript and postscriptfile)
RU, RD, RN, RZ (see sections ru, rd, rn and rz)
absolute, relative (see sections absolute and relative)
floating, fixed (see sections floating and fixed)
single, double, doubleextended, doubledouble, tripledouble (see sections single, double, doubleextended, doubledouble and tripledouble)
SG, D, DE, DD, TD (see sections single, double, doubleextended, doubledouble and tripledouble)
perturb (see section perturb)
honorcoeffprec (see section honorcoeffprec)
default (see section default)
error (see section error)
void (see section void)
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:
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:
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:
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:
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:
Structures can also be defined literally using the syntax illustrated in the next example. They will also be printed in that syntax.
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.
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:
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.
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:
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.
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.
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:
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:
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:
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:
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:
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.
The list of commands of Sollya is available in two flavours:
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).
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])).
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].