The Sollya tool is Copyright © 2006-2010 by
Laboratoire de l'Informatique du Parallélisme - UMR CNRS - ENS Lyon - UCB Lyon 1 - INRIA 5668, Lyon, France, and by
LORIA (CNRS, INPL, INRIA, UHP, U-Nancy 2) Nancy, 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.
The Sollya distribution can be compiled and installed using the usual
./configure
, make
, make install
procedure. Besides 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)
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:
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.
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-4 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 4. 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.
Note 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 make 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. Note 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 note 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 var
keyword. See section var for details
on its usage and semantic.
The following code examples illustrate the usage 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 continuing with ASCII letters or numerical digits.
true
and false
. Boolean expressions can be constructed using the boolean connectors &&
(and), ||
(or), !
(not), and comparisons.
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. Note 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:
Note that 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:
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 note 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 in 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
. Note 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.
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:
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:
@
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.
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)
@
. 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:
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.