\documentstyle[IEEEtran]{article}

\begin{document}

\pagestyle{myheadings}
\tolerance 10000

\markright{APIC'95, El Paso,
Extended Abstracts,
A Supplement to the international journal of {\rm Reliable
Computing}\ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ }


\def\Rw{\Rightarrow}
\def\rw{\rightarrow}

\title{Functional Programming and Interval Arithmetic}

\author{R. D. Lins, M. A. Campos, and M. de B. Correia}

\maketitle

\begin{abstract}
The functional programming paradigm makes it easier to prove
correctness of programs. However, if a program uses operations with
real numbers, then, even if this program is correct, the use standard
(not absolutely precise) computer operations with 
floating point numbers can make the result of this program incorrect. 

In this paper, we describe how to add 
interval arithmetic to functional programming. This addition enables
us to prove correctness of the programs that process real numbers. 
Our goal is to design 
programs that are reliable and efficient.
\end{abstract}

\auffil{The authors are with Dept.~de Inform\'atica, Universidade Federal de 
Pernambuco, Recife, Brazil.
Research reported herein has been sponsored by 
CNPq (Brazil) grant 530465/93-0.}

\section{Introduction}

Each day, the demand for reliable software increases.
Nowadays, software already controls nuclear plants, weapons, etc.
Human lives, and even the existence of the whole planet depend (to
some degree)
on the reliability of these programs.

One way to guarantee reliability is to test a program for all possible
cases. Usually, there are many possible inputs, so testing all of them
is always difficult, and most of the time practically impossible.
If we test a program on only some possible inputs, then the results of
this testing are not 100\% reliable. The only way to guarantee the
program's reliability is to {\it prove} the program to be correct.
The existing 
software design techniques, specification methods, programming style,
languages, and system environments are not very supportive of the
correctness proofs. To make them supportive, a long evolution is
needed.
Also, we need sophisticated tools to help us with proving program correctness.

In his 1978 Turing Award Lecture \cite{backus}, John Backus drew the attention 
of the computer science community to {\it functional programming} as a
possible solution to a series of 
problems of programming known as ``the software crisis''.
Following this idea, 
the 1980's saw large advances in formal methods and functional programming.
However, the low performance figures offered by all implementations of
functional
languages largely compromised their applicability.
Only recently, implementors of functional languages have learned how to
produce fast functional compilers \cite{gama,ogama}.
These compilers renewed the interest in functional programming.

Functional languages are, in essence, a nicer syntax to the $\lambda$-Calculus,
a theory of functions \cite{church,barendregt}.
This makes proving program correctness a much easier task than in 
{\it imperative
programming}, a more traditional 
programming paradigm in which programs reflect the features
of the machine architecture.

Application programs that have been formally proved correct can only be
reliable if they run on hardware that has been formally proved correct, under
correct basic software, such as operating systems, environments and tools.
This philosophy is inconsistent with the use of floating point arithmetic,
because floating point arithmetic is inherently imprecise.

One of the features of ``pure'' functional languages, such as 
Miranda\footnote{Miranda is a trademark of Research Software Ltd.} \cite{mira},
is {\it lazy} evaluation.
This means that any expression will be evaluated only if needed, and at
most once.
Lazy evaluation allows the use of infinite data structures, such as infinite
sets and lists, which are described by a formation law.
These structures can be seen as intensionally defined.

The functional programming community has been aware of the fact that floating
point arithmetic introduces errors to programs and thus,
destroys their reliability.
Lazy evaluation has been used to implement infinite precision arithmetic
\cite{boeh86,boeh88}.
Using this technique, real numbers are internally represented by a lazy
list, and for this reason they are called {\it lazy reals}.
In order to reduce the propagation of carries, Avizienis' numerical system is
used \cite{avizienis}, at a cost of losing uniqueness in representation.
Operations on these numbers are also lazy.
The whole evaluation process is driven by the printing routine, which
``unfolds'' the definition of the data structures generating a precision as
good as required by the application.
Unfortunately, this process involves far too much symbolic manipulation
and is unbearably slow.
Lazy reals also have an additional drawback: they cannot be described
by the existing (ordered and metric) 
approaches to formalizing continuous data types \cite{wilson}. 

We see interval arithmetic \cite{ale83} as an alternative to infinite 
precision arithmetic, an alternative that
can offer a much lower computational overhead.

In this paper, we briefly describe the main features 
of functional languages and advocate the idea 
that the combination of interval arithmetic 
and functional programming can make programs 
reliable and efficient.

\section{Functional Programming}

In this section we present a brief overview of the main features of lazy
functional languages.

Three main characteristics define a ``pure'' functional language, such as
Miranda \cite{mira}, are:
\begin{itemize}
\item {\it higher-order functions}: functions are not only passed as
parameters to other functions, but can also be the result of
the evaluation of a given function.
\item {\it referential transparency}: the value of any sub-expression is
static, there is no destructive assignment.
\item {\it lazy evaluation}: any expression is evaluated at most once,
and only when necessary.
\end{itemize}

Below we outline some aspects of the functional programming style.

\subsection{The evaluation mechanism}

Functional programs consist of definitions of functions and other objects.
The execution of
a program in a functional language consists of the
evaluation of an expression; this evaluation can be performed as 
a successive rewriting of an expression until it takes a printable 
({\it normal})
form (a normal form is the one that cannot be rewritten further.)
For example, if we say
%\begin{small}
\begin{verbatim}
     fac n = n * fac(n-1)  , n>0     (1)
           = 1             , otherwise
\end{verbatim}
%\end{small}
then
%\begin{small}
\begin{verbatim}
     fac 2
\end{verbatim}
%\end{small}
is rewritten thus
\begin{eqnarray*}
\verb+fac 2+ & \Rw & {\tt 2 * fac \ (2-1)} \hspace*{.5cm} ({\rm 2}) \\
& \Rw & {\tt 2 *  fac \ 1} \\
& \Rw & {\tt 2 * (1 * {fac} \ (1-1))} \\
& \Rw & {\tt 2 * (1 * {fac} \ 0)} \\
& \Rw & {\tt 2 * (1 * 1)} \\
& \Rw & {\tt 2 * 1 }\\
& \Rw & {\tt 2}
\end{eqnarray*}

The definition (\verb+1+) is used in the first line of (2) where we have to
substitute the actual value 2 for the variable {\it n}; this process of
parameter passing forms the major overhead in rewriting implementations
of functional languages.

\subsection{Pattern-matching}

Pattern-matching is another interesting simplification to the syntax
of expressions in functional languages.
Using pattern-matching, one can place guards on the left hand side of a
function definition.
For instance, 
using pattern-matching, the above function definition can be expressed more
neatly as
\begin{verbatim}
     fac 0 = 1
     fac n = n * fac(n-1)
\end{verbatim}
In the general case pattern-matching can become quite complex.
Miranda allows pattern-matching on general
algebraic data types.
In these cases, pattern-matching not only provides us with guards (as 
in the above example), but also with {\it selectors}
which can ``decompose'' objects of composite 
(algebraic) data types.

\subsection{Introducing new data types}

The primitive, or {\it basic} 
types in Miranda are: {\tt num, char}, and {\tt bool}.
The type {\tt num} comprises both integers and floating point numbers.
As elements of the type {\tt bool}, we have the truth values {\tt True} and
{\tt False}.
The type {\tt char} contains the characters of the ASCII character set.
Miranda also contains data type constructors such
as {\tt list} and {\tt tuple}.

A new algebraic type in Miranda can be is introduced by using the
symbol {\tt ::=}.
For instance, the type {\tt tree} can be introduced as follows:
\begin{verbatim}
  tree ::=  Leaf num | Node num tree tree
\end{verbatim}
The tree-constructor {\tt Leaf}  has a type  ${\tt num} \rw {\tt tree}$,
and {\tt Node} has a type  $${\tt ((num \rw tree)} \rw {\tt tree)} \rw
{\tt tree } $$
(the $\rw$ operator denotes curryfication and is left-associative).
In Miranda, the definition mechanism uses pattern matching on constructors.
For instance, we can define a function $\tt wt$ that computes the
weight of a give tree as
\begin{verbatim}
 wt (Leaf n) = n 
 wt (Node n t1 t2) = (wt t1)+(wt t2)+n
\end{verbatim}

The type system of Miranda subsumes Pascal enumerated types, records,
variant records, and some uses of pointers which are involved in the
construction of recursive dynamic data structures.

\subsection{ZF-expressions}

The general form of a ZF-expression in Miranda is
\[ \{ {\it exp; \ qualifiers} \} \]
with an arbitrary (non-zero) number of {\it qualifiers}.
Each qualifier is either a {\it generator} or a {\it filter}.
A {\it generator} is a list of values which will be attributed to a
specific variable in the expression {\it exp}.
A {\it filter} is an arbitrary boolean expression that further
restricts the range of a generator.

ZF-expressions are a convenient and elegant syntactic `sugaring' of a
class of expressions.
For example, the list of all the squares of the integer
numbers between 1 and 10 can be expressed in Miranda by the
following ZF-expression:
\begin{verbatim}
             { x*x; x <- (1..10)}
\end{verbatim}

\subsection{Local definitions}

The general form of a definition will be:
\[ \begin{array}{lcl}
f \ x_0 \dots x_n = & e_0 & {\tt where} \\
& & a^1 v^1_1 \dots v^1_p = d^1 \\
& & \vdots \\
& & a^m v^m_1 \dots v^m_q = d^m
\end{array} \]
The definitions of the functions $a^1, \ldots, a^m $ within the {\tt where}
block can be mutually recursive.
Their scope is restricted to the expression $e_0$ (and to the right-hand
sides of their definitions, since they are recursive).
Local definitions are used both to define auxiliary functions
and to hold values of intermediate computations which may be
referenced a number of times in the expression $e_0$.

The definitions of $a^1, \ldots , a^m $ may themselves contain local
definitions; a local definition is used even if a more
global definition of the same symbol exists. 

\section{Programming language support for scientific computation -
Prerequisites}

In this section (based on \cite{scicom,rump}),
 we present the features that a programming language should have
to be suitable for numerical computation with the type {\tt interval}.
It is necessary to know these features if we want to  
enrich a functional language with this data type.

The data types occuring in numerical computation include real and
complex numbers, vectors, and matrices.

Mathematicians use the same infix operators to denote the arithmetic
operations is all corresponding spaces. 
Also identical function names identify the standard functions for different 
data types. 
Matrix or vector algorithms are usually formulated for arbitrary dimension.

Furthermore, the accuracy of the basic operations shall be optimal for all 
the spaces of the numerical computations. 

Programming languages should 
enable the programmer to write and implement new arithmetic 
operations or even new expression evaluation in the language. 
For this purpose the following  concepts are recommended:
\begin{itemize}
\item  user-defined operators; at least, by overloading the standard
operators, and ideally,  
by allowing new operator identifiers and/or symbols;
\item operators and functions whose results are of composite (structured)
data types; 
\item overloadable  function identifiers;
\item dynamic arrays;
\item access to directed roundings for interval arithmetic;
\item  for  the accuracy requirement three arithmetic properties are mandatory:
\begin{itemize}
\item  floating-point  arithmetic must be optimally defined;
\item at least three  roundings must be accessible;
\item an optimal scalar  product  must be available.
\end{itemize}
\end{itemize}

The following additional features are intended to make programming
easier:
\begin{itemize}
\item A  module concept is very  helpful to facilitate the management of a 
lot  of different arithmetic libraries.
\item Generic, type-parameterized  subroutines reduce the size of source code  
and thus enhance the readability of the program by combining routines  which 
perform identical operations for different data types. 
The object  code size  may also decrease as a result.
\item A subtype concept allows the automatic conversion of parameters 
to match  the interface between the expressions of different types.
\item Alternative expression concepts (e.g., for accurate evaluation or
symbolic computation) may be supplied.
\item Simultaneous polymorphism increases  the information obtained:
\begin{itemize} 
\item 
a complex interval may be simultaneously treated as a  circle and 
as a rectangle;
\item an expression 
can be both kept in its symbolic form,
 and evaluated as floating-point number 
and interval.
\end{itemize} 
\end{itemize} 

\section{Functional Programming for Scientific Computation}

Analyzing the list of desirable features a language must have to
support numerical computations one can see that
many of the features above that will make programming easier either have
already been implemented in functional languages (such as modules,
polymorphism, 
etc.) or can be easily included in them.

Two major problems must be overcome in order to make functional languages
suitable for scientific computation:
\begin{enumerate}
\item The introduction of the type array should not break referential
transparency.
\item The inclusion of an explicit iteration operator.
\end{enumerate}
The loss of referential transparency means that the user is interfering
directly in the state of the execution of programs, which, in its
turn, means not only
losses to the potential parallelism, but also weakens the possibility of
formal reasoning about programs.
A neat solution has been recently proposed with {\em monads} \cite{monads}.

The second problem is a much deeper one.
Recursion is the natural way functional programmers express the repetition
of parts of code, while iteration plays the same r\^ole in expressing
numerical algorithms.
In our experience, the translation of a iterative numerical algorithm
into a recursive version is a {\it tour de force} and yields unnatural results.

In our implementation of $\Gamma$CMC with the primitive type interval
\cite{igama}, we are analyzing the possibility of including an explicit 
iteration operator, as
well as implementing the following features, inspired by the 
PASCAL-XSC compiler \cite{bohl}:
\begin{itemize}
\item The concept of a universal operator.
\item Functions and operators with results of arbitrary data types.
\item Overloading of procedures, functions and operators.
\item The concept of a module.
\item Dynamic arrays.
\item Access to subarrays.
\item The concept of a string.
\item Controlled rounding.
\item Optimal (exact) scalar product.
\item Standard type dot precision.
\item Additional arithmetic standard data 
types such as complex, interval, etc.
\item Highly accurate arithmetic for standard data types.
\item Highly accurate standard functions.
\item Exact evaluation of expressions.
\end{itemize}  

\section{Conclusions}
 
In this paper, we advocate the idea that the combination of 
interval arithmetic
and functional programming can make programs
reliable and efficient.
Programs obtained by these means have the quality of a theorem 
in the sense of pure mathematics. 

Many of the features that are desirable for the efficient scientific
programming are already present in the implementation of modern functional
programming languages.
However, in order to make numerical algorithms easier to program in
pure functional languages, some compromise is needed.
This compromise must not damage the reliabilities of 
the functional programming paradigm and of interval arithmetic.

\begin{thebibliography}{10}
\bibitem{ale83}
G. Alefeld and J. Herzberger,
{\bf Introduction to Interval Computations.}
Academic Press, N.Y., 1983. 

\bibitem{avizienis}
A. Avizienis,
``Signed-digit number representations for fast parallel arithmetic'',
{\it IRE Transactions on Electronic Computers}, 1961.

\bibitem{barendregt} H. P. Barendregt, {\bf The Lambda Calculus, 
its Syntax and
Semantics}, Studies in Logic and the Foundation of Mathematics,
2nd ed., North-Holland, 1984.

\bibitem{backus}
J. Backus.
``Can Programming be Liberated from the von Neumann Style?
A Functional Style and Its Algebra of Programs.''
{\it Communications ACM}, 1978, Vol. 21, No. 8, pp. 613--641.

\bibitem{boeh88}
H. Boehm and R. Cartwright,
{\bf Exact real arithmetic: Formulating real numbers as functions},
 Technical report Rice COMP TR88-66, Department of Computer Science,
Rice University, April 1988.

\bibitem{boeh86}
H. Boehm,  R. Cartwright, M. J.O'Donnell, and M. Riggle,
``Exact real arithmetic: A case study in higher order programming'',
 in {\it Proceedings of the Lisp and Functional Programming
Conference}, 1986, pp. 162--173.

\bibitem{bohl}
R. Hammer, M. Neaga, and D. Ratz,
``Pascal-XSC, New Concepts for Scientific Computation and Numerical
Data Processing'',
 In: R. S. Stepleman (ed.), {\bf Scientific Computing}, 
North-Holland, 1993, pp. 15--44.

\bibitem{church} 
A.Church,
``A set of postulates for the foundation of logic'',
{\em Annals of Math.}, Vol. 33, No. 2, pp. 346--366.

\bibitem{scicom}
J. W. von Gudenberg.
``Programming Language Support for Scientific Computation'',
 {\it Interval Computations}, 1992, No. 4(6), pp. 116--126.

\bibitem{gama}
R. D. Lins and B. O. Lira,
``$\Gamma$CMC: A Novel Way of Implementing Functional Languages'',
 {\em Journal of Programming Languages}, 1993, Vol. 1, pp. 19--39.

\bibitem{ogama}
R. D. Lins, G. G. Cruz Neto, and R. F. Lima,
``Implementing and Optimising $\Gamma$CMC'',
 {\it Proceedings of Euromicro'94}, IEEE Computer Society Press,
Sep. 1994, pp. 353--361.

\bibitem{igama}
R. D. Lins, M. A. Campos, M. B. Correia,
G. G. Cruz Neto, and R. M. F. Lima,
``The Implementation of the Type Interval in $\Gamma$CMC'',
 {\em in preparation}.

\bibitem{monads}
E. Moggi,
``Computational lambda calculus and monads,''
In: {\it Logic in Computer Science}, California, IEEE Press, June 1989.

\bibitem{wilson}
W. R. de Oliveira, and M. B. Smyth,
``Quasimetric $\Sigma$-Algebras'',
 in {\it Proceedings of the XIV Congress of the Brazilian Computing
Society}, Caxamb\'u, August 1994.

\bibitem{rump}
S. M. Rump,
 {\bf Seminar Notes}, Universidade Federal de Pernambuco, 
 Recife (Brazil), September 1994.

\bibitem{mira}
D.A.Turner,
 ``Functional Programming as executable Specifications'',
 {\em Phil.Transactions of the Royal Society of London}, 1984, Vol. 312,
pp. 363--388.

\end{thebibliography}
\end{document}