diff options
Diffstat (limited to 'ic-reals-6.3/doc')
| -rw-r--r-- | ic-reals-6.3/doc/implementation-notes/README | 2 | ||||
| -rw-r--r-- | ic-reals-6.3/doc/implementation-notes/decimal_precision.tex | 704 | ||||
| -rw-r--r-- | ic-reals-6.3/doc/manual/collect-eps-converted-to.pdf | bin | 0 -> 2628 bytes | |||
| -rw-r--r-- | ic-reals-6.3/doc/manual/collect.eps | 68 | ||||
| -rw-r--r-- | ic-reals-6.3/doc/manual/continue-eps-converted-to.pdf | bin | 0 -> 2614 bytes | |||
| -rw-r--r-- | ic-reals-6.3/doc/manual/continue.eps | 68 | ||||
| -rw-r--r-- | ic-reals-6.3/doc/manual/go-eps-converted-to.pdf | bin | 0 -> 2599 bytes | |||
| -rw-r--r-- | ic-reals-6.3/doc/manual/go.eps | 68 | ||||
| -rw-r--r-- | ic-reals-6.3/doc/manual/manual.aux | 30 | ||||
| -rw-r--r-- | ic-reals-6.3/doc/manual/manual.log | 324 | ||||
| -rw-r--r-- | ic-reals-6.3/doc/manual/manual.pdf | bin | 0 -> 191783 bytes | |||
| -rw-r--r-- | ic-reals-6.3/doc/manual/manual.tex | 1057 | ||||
| -rw-r--r-- | ic-reals-6.3/doc/manual/step-eps-converted-to.pdf | bin | 0 -> 2603 bytes | |||
| -rw-r--r-- | ic-reals-6.3/doc/manual/step.eps | 68 | ||||
| -rw-r--r-- | ic-reals-6.3/doc/manual/stop-eps-converted-to.pdf | bin | 0 -> 2598 bytes | |||
| -rw-r--r-- | ic-reals-6.3/doc/manual/stop.eps | 68 |
16 files changed, 2457 insertions, 0 deletions
diff --git a/ic-reals-6.3/doc/implementation-notes/README b/ic-reals-6.3/doc/implementation-notes/README new file mode 100644 index 0000000..b70ba06 --- /dev/null +++ b/ic-reals-6.3/doc/implementation-notes/README @@ -0,0 +1,2 @@ +This directory will eventually contain documents describing the +implementation. Regretfully, most are incomplete at present. diff --git a/ic-reals-6.3/doc/implementation-notes/decimal_precision.tex b/ic-reals-6.3/doc/implementation-notes/decimal_precision.tex new file mode 100644 index 0000000..7d8d14d --- /dev/null +++ b/ic-reals-6.3/doc/implementation-notes/decimal_precision.tex @@ -0,0 +1,704 @@ +\documentclass[11pt,a4paper]{article} + +\usepackage{amsfonts} +\usepackage{amsmath} + +\newtheorem{tm}{Theorem} +\newtheorem{df}[tm]{Def{i}nition} +\newtheorem{lemma}[tm]{Lemma} +\newtheorem{prop}[tm]{Proposition} +\newtheorem{cor}[tm]{Corollary} + +%\newenvironment{proof}{\textbf{Proof:} \footnotesize}{} +\newenvironment{proof} + { \begin{description} \item[Proof:] \footnotesize } + { \end{description} } + + +\begin{document} + +\title{Obtaining a Required Absolute Precision from an Exact Floating Point + Number} +\author{Marko Krznari\'{c}} +\date{\today} %\date{21 March 2000} +\maketitle + + +\section{Introduction} +A real number may be represented as a shrinking sequence of nested, + closed intervals with rational end--points whose length tends to + zero. We will work in the one--point compactification $\mathbb{R}^* + = \mathbb{R} \cup \{ \infty \}$ of the real line, which is usually + represented by the unit circle and the stereographic projection. In + the LFT approach to Exact Real Arithmetic the sequence of intervals + is generated by a sequence of one--dimensional linear fractional + transformations (LFTs) applied to a base interval, \cite{vui90, + niekor95, edapot97, pot98, hec99}. + +These intervals (LFTs applied to the base interval) are better and + better approximations to the real number. Knowing the length of the + interval we may tell how good the approximations are. Except of + one proposition in \cite{pot98} (Proposition 40, page 129), there + are no other references which tell us how to calculate the length + of the intervals. Here, we show how to determine the length of the + intervals and especially, how to obtain a required decimal + precision of a real number. + + +\section{Representation of Real Numbers} +Let us denote the set of matrices with integer coefficients by: + \[ \mathbb{M} = + \left\{ \left( \begin{array}{cc} a&c\\b&d \end{array} + \right)\ |\ a,b,c,d \in \mathbb{Z} \right\}. \] + A matrix induces an 1--dimensional LFT (a function from + $\mathbb{R}^*$ to $\mathbb{R}^*$) which is given by: + \[ \Theta \left( \begin{array}{cc} a&c\\b&d \end{array} + \right)(x) = \displaystyle { \frac{ax+c}{bx+d} }. \] + We can identify an LFT $\Theta(M)$ with the matrix $M$ and this + identification is unique up to scaling by a non--zero + integer. The composition of two 1--dimensional LFTs correspond + to matrix multiplication. A non--singular matrix $M$ maps an + interval to an interval: the interval $[p,q]$ is mapped to + $[Mp, Mq]$ for $\det M > 0$ and $[Mq,Mp]$ for $\det M < 0$. + In $\mathbb{R}^*$, the interval $[p,q]$ is the set of all of + the points which belong to the arc starting from $p$ and going + anti--clockwise to $q$ on the unit circle. For example, $[1,-1] = + \{ x\ |\ |x| \ge 1 \}$. + +One can easily verify that for any two intervals I and J with rational + end--points, there exists an LFT $M$ such that $M(I) = J$. This implies + that all rational intervals can be encoded as an LFT applied to a + fixed interval, which is called the \textsc{base interval}. Although + the choice of the base interval is essentially not relevant (whatever + holds for one, will hold, with minor adjustments, for any other + base interval), we should choose it in a way to make computations + as efficient as possible. There are two base intervals which have + been used, namely $[-1,1]$ and $[0,\infty]$. Check \cite{eda97, + edapot97, pot98, hec99} for more details. + +For a base interval $[a,b]$, we say that a matrix $M$ is \textsc{refining} + if $M[a,b] \subseteq [a,b]$. The set of all refining matrices is + denoted by $\mathbb{M}^+$. We also define the \textsc{information} of + an LFT $M$ by $\textbf{Info}_{[a,b]}(M) = {\bf Info}(M)=M[a,b]$. + +As we mentioned earlier, a real number can be represented as a + shrinking sequence of nested, closed intervals with rational + end--points whose length tends to zero. Or, using the facts given + above, as a sequence of 1--dimensional LFTs: + \[ \begin{array}{rccl} + & \{ x \} &=& \displaystyle{ \bigcap_n [p_n,q_n], + \qquad p_n,q_n \in \mathbb{Q}, } \vspace{1em} \\ + & [p_n,q_n] &=& \displaystyle{ M_0 M_1 \ldots M_n [a,b], + \qquad \forall n, } \vspace{1em} \\ + \Rightarrow & \{ x \} &=& \displaystyle{ \bigcap_n M_0 M_1 + \ldots M_n [a,b], } + \end{array} \] + where $[a,b]$ is the base interval, $M_0 \in \mathbb{M}$, and + $M_n \in \mathbb{M}^+,\ n>0$. This representation is called + \textsc{normal product}. The first matrix, $M_0$, determines an + interval which contains the real number $x$, while all other matrices + refine that interval more and more. By analogy with the usual + representation of the real numbers, the first matrix of the normal + product, $M_0 \in \mathbb{M}$, is called a \textsc{sign} matrix, + while the matrices $M_n \in \mathbb{M}^+$ are called \textsc{digit} + matrices. + + Edalat and Potts in~\cite{eda97,edapot97} proposed a standard form, + called \textsc{exact floating point}, EFP, where both, sign and digit + matrices, belong to predetermined finite sets of matrices. The + information in the sign matrices should overlap and cover + $\mathbb{R}^*$. The four sign matrices proposed by Edalat and Potts + correspond to rotations of the unit circle by $0^\circ$ (i.e identity), + $90^\circ, \ 180^\circ$ and $270^\circ$, and form a cyclic group. + Digit matrices should overlap, cover the base interval $[a,b]$, and + contract distances in $[a,b]$. + + +\section{The Base Interval $[0,\infty]$} +The main reason to choose $[0,\infty]$ as a base interval is that it is + very easy to calculate the information of a matrix $M=\begin{pmatrix} + a&c\\b&d \end{pmatrix}$: ${\bf Info}M=[\frac{c}{d},\frac{a}{b}]$ if + $\det M > 0$ or ${\bf Info}M=[\frac{a}{b},\frac{c}{d}]$ if $\det M < 0$. + In the base interval $[0,\infty]$, the four sign matrices are named + as follows: + \[ \begin{array}{rccclcrcl} + S_+ &=& \begin{pmatrix} 1&0 \\ 0&1 \end{pmatrix} &=& + S_\infty^{4k} = \textrm{Id}, &\qquad& + \textbf{Info}(S_+) &=& [0,\infty], \vspace{0.5em} \\ + S_{\infty} &=& \begin{pmatrix} 1&1 \\ -1&1 \end{pmatrix} &=& + S_\infty^{4k+1}, &\qquad& + \textbf{Info}(S_\infty) &=& [1,-1], \vspace{0.5em} \\ + S_- &=& \begin{pmatrix} 0&-1 \\ 1&0 \end{pmatrix} &=& + S_\infty^{4k+2}, &\qquad& + \textbf{Info}(S_-) &=& [\infty,0], \vspace{0.5em} \\ + S_0 &=& \begin{pmatrix} 1&-1 \\ 1&1 \end{pmatrix} &=& + S_\infty^{4k+3}, &\qquad& + \textbf{Info}(S_0) &=& [-1,1]. + \end{array} \] + It is easy to check that, for example, $S_0 S_\infty = + S_\infty S_0 = S_+ = \textrm{Id}$. + + For an integer $b \ge 2$ we define digit matrices in base $b$ by: + \[ D_k = \begin{pmatrix} b+k+1 & b+k-1 \\ b-k-1 & b-k+1 \end{pmatrix} + = S_\infty \begin{pmatrix} 1&k\\0&b \end{pmatrix} S_0, \] + where $k$ is an integer with $ |k| < b$. Products of digit matrices + can be obtained as follows: + \[ D_{d_1} D_{d_2} \ldots D_{d_n} = \begin{pmatrix} + b^n+c+1 & b^n+c-1 \\ b^n-c-1 & b^n-c+1 \end{pmatrix} =: + \mathfrak{D}_c^n, \] + where + \[ c = c(d_1,d_2,\ldots,d_n) = \sum_{i=1}^n d_i b^{n-i}. \] + Furthermore, $\mathfrak{D}_c^n D_d = \mathfrak{D}_{bc+d}^{n+1}$. The + number $c$ provides a compressed representation for this product + of digit matrices. However, the original sequence of digits usually + cannot be recovered from $\mathfrak{D}_c^n$. + +The most used base $b$ in both, theory and practise, is the base $b=2$. + In that case, we get the following three digit matrices: + \[ \begin{array}{rccclcrcl} + D_{-1} &=& \begin{pmatrix} 1&0 \\ 1&2 \end{pmatrix} &=& + S_\infty \begin{pmatrix} 1&-1 \\0&2 \end{pmatrix} S_0, &\qquad& + \textbf{Info}(D_{-1}) &=& [0,1], \vspace{0.5em} \\ + D_0 &=& \begin{pmatrix} 3&1 \\ 1&3 \end{pmatrix} &=& + S_\infty \begin{pmatrix} 1&0\\0&2 \end{pmatrix} S_0, &\qquad& + \textbf{Info}(D_0) &=& [\frac{1}{3},3], \vspace{0.5em} \\ + D_1 &=& \begin{pmatrix} 2&1 \\ 0&1 \end{pmatrix} &=& + S_\infty \begin{pmatrix} 1&1\\0&2 \end{pmatrix} S_0, &\qquad& + \textbf{Info}(D_1) &=& [1,\infty]. + \end{array} \] + Any sequence of $n$ digits in base $2$, $D_{d_1},\ D_{d_2},\ \ldots,\ + D_{d_n}$ can be compressed into the number $c(d_1,d_2,\ldots,d_n)$, + which can be represented in only $n+1$ bits of memory. + + +\subsection{$S_0 D_{d_1} D_{d_2} \ldots$} +The information of the sign matrix $S_0$ is the interval $[-1,1]$, + i.e. $\textbf{Info}(S_0) = [-1,1]$. Any digit in base $b$ will + contract distances on the real line by a factor $\frac{1}{b}$. + We have the following: + \begin{prop} \label{prop:Szero and width of information with base b} + \[ {\sf width} ( {\bf Info} ( S_0 D_{d_1} D_{d_2} + \ldots D_{d_n} ) ) = \frac{2}{b^n}, \] + where $D_{d_i},\ i=1 \ldots n$, are digits in the base $b$. + \end{prop} + \begin{proof} As $D_i = S_\infty \begin{pmatrix} 1&d\\0&b \end{pmatrix} + S_0$ and $S_\infty S_0 = \textrm{Id}$ we have: + \[ \begin{array}{rcl} + S_0 D_{d_1} D_{d_2} \ldots D_{d_n} &=& S_0 S_\infty + \begin{pmatrix} 1&d_1\\0&b \end{pmatrix} S_0 S_\infty + \begin{pmatrix} 1&d_2\\0&b \end{pmatrix} S_0 \ldots S_\infty + \begin{pmatrix} 1&d_n\\0&b \end{pmatrix} S_0 \\ + &=& \begin{pmatrix} 1&d_1\\0&b \end{pmatrix} + \begin{pmatrix} 1&d_2\\0&b \end{pmatrix} \ldots + \begin{pmatrix} 1&d_n\\0&b \end{pmatrix} S_0 \\ + &=& \begin{pmatrix} 1&c\\0&b^n \end{pmatrix} S_0, + \end{array} \] + where $c = \sum_{i=1}^n d_i b^{n-i}$. + Then, + \[ \begin{array}{rcl} + \textsf{width} (\textbf{Info}(S_0 D_{d_1} D_{d_2}\ldots D_{d_n})) + &=& \textsf{width} \left( \begin{pmatrix} 1&c\\0&b^n + \end{pmatrix} S_0 [0,\infty] \right) \\ + &=& \textsf{width} \left( + \begin{pmatrix} 1&c\\0&b^n \end{pmatrix} [-1,1] \right) \\ + &=& \displaystyle{ \textsf{width} \left( + \left[ \frac{-1+c}{b^n}, \frac{1+c}{b^n} \right] \right) } \\ + &=& \displaystyle{ \frac{2}{b^n} }. + \end{array} \] + \end{proof} + Knowing that, it is easy to calculate a sufficient number of digits + which will achieve any required accuracy. + + +\subsection{$S_+ D_{d_1} D_{d_2} \ldots$} \label{subsection spos} +Real numbers which can be represented by the product $S_+ D_{d_1} + D_{d_2} \ldots = D_{d_1} D_{d_2} \ldots$ are points of the + interval $[0,\infty]$. An infinite product of digits $D_{b-1}$ in + base $b$ represents $\infty$. Any other infinite product + can be written as a finite product of $D_{b-1}$ (exponent), followed + by an infinite product of digits starting with $D_k$ where $-(b-1) + \le k \le (b-2)$ (mantissa). Any such product represents a + non--negative real number $x \in [0,\infty)$. + +If the product represents $\infty$, as it happens with $\frac{1}{0}$, the + computation of the interval lengths will not finish in finite + time (unless we put a time limit). In all other cases, using + Proposition~\ref{prop:Spos and width of information with base b}, we + will be able to determine how many digit matrices will be sufficient + to satisfy the required accuracy. Proposition~\ref{prop:Spos and + width of information with base b} is a generalisation of Potts's + Proposition~\ref{prop:width of information with base 2}, + \cite{pot98}, which we present later. + \begin{prop} \label{prop:Spos and width of information with base b} + Let $D_{b-1}^e D_{d_1} D_{d_2} \ldots D_{d_n}$ be a finite product + of digits in base $b$ with $d_1 \ne (b-1)$. + Then: + \[ b^{e-n} < {\sf width} ( {\bf Info} ( D_{b-1}^e D_{d_1} + D_{d_2} \ldots D_{d_n} ) ) < 4 b^{e-n+2}. \] + \end{prop} + \begin{proof} + The product $D_{b-1}^e D_{d_1} D_{d_2} \ldots D_{d_n} = D_{b-1}^e + \mathfrak{D}_c^n$ can be compressed into $\mathfrak{D}_{c'}^{n'}$ where + \[ \begin{array}{rcl} + n' &=& e+n, \\ + c' &=& \left[ (b-1)b^{e+n-1} + \ldots + (b-1)b^n \right] + \left[ + d_1 b^{n-1} + \ldots + d_{n-1} b + d_n \right] \\ + &=& \displaystyle{ b^n (b-1) \frac{b^e-1}{b-1} + c } \\ + &=& b^{e+n} - b^n + c + \end{array} \] + Information of $D_{b-1}^e \mathfrak{D}_c^n$ is given by: + \[ \begin{array}{rcl} + {\bf Info} (D_{b-1}^e \mathfrak{D}_c^n) &=& \begin{pmatrix} + b^{n'}+c'+1 & b^{n'}+c'-1 \\ b^{n'}-c'-1 & b^{n'}-c'+1 + \end{pmatrix} [0,\infty] \\ + &=& \begin{pmatrix} 2b^{e+n}-(b^n-c-1) & 2b^{e+n}-(b^n-c+1) + \\ b^n-c-1 & b^n-c+1 \end{pmatrix} [0,\infty] \\ + &=& \left[ \displaystyle{ \frac{2b^{e+n}}{b^n-c+1} - 1, + \frac{2b^{e+n}}{b^n-c-1} - 1 } \right]. + \end{array} \] + Therefore, + \[ \begin{array}{rcl} + {\sf width} ( {\bf Info} ( D_{b-1}^e \mathfrak{D}_c^n ) ) &=& + \displaystyle{ \frac{2b^{e+n}}{b^n-c-1} - + \frac{2b^{e+n}}{b^n-c+1} } \\ + &=& \displaystyle{ \frac{4b^{e+n}}{(b^n-c)^2-1}. } + \end{array} \] + This holds for any sequence of digits. If, for example, all of the + $n$ digits compressed into $\mathfrak{D}_c^n$ are digits $D_{b-1}$, + then, + \[ \begin{array}{rcl} + \displaystyle{ \frac{4b^{e+n}}{(b^n-c)^2-1} } &=& + \displaystyle{ \frac{4b^{e+n}}{(b^n-(b^n-1))^2-1} } \\ + &=& \displaystyle{ \frac{4b^{e+n}}{0} } \\ + &=& \infty, + \end{array} \] + which corresponds to the length of the interval: + \[ \begin{array}{rcl} + {\bf Info} ( D_{b-1}^e \mathfrak{D}_{b^n-1}^n ) &=& + \displaystyle{ \left[ \frac{2b^{e+n}}{b^n-c+1} - 1, + \frac{2b^{e+n}}{b^n-c-1} -1 \right] } \\ + &=& [b^{e+n}-1, \infty]. + \end{array} \] + If $d_1 \ne b-1$, i.e. $-(b-1) \le d_1 < (b-1)$, we have: + \[ \begin{array}{rcl} + c &\ge& -(b-1) b^{n-1} - (b-1) b^{n-2} - \ldots - (b-1) b^0 \\ + &=& -b^n + 1 \vspace{1em} \\ + c &\le& (b-2) b^{n-1} + (b-1) b^{n-2} + (b-1) b^{n-3} + + \ldots + (b-1) b^0 \\ + &=& (b-2) b^{n-1} + (b^{n-1}-1) \\ + &=& (b-1) b^{n-1} - 1. + \end{array} \] + Therefore, + \[ \begin{array}{rcl} + {\sf width} ( {\bf Info} ( D_{b-1}^e \mathfrak{D}_c^n ) ) &=& + \displaystyle{ \frac{4b^{e+n}}{(b^n-c)^2-1} } \\ + &\le& \displaystyle{ \frac{4b^{e+n}}{(b^n-(b-1)b^{n-1}+1)^2 - 1} } \\ + &=& \displaystyle{ \frac{4b^{e+n}}{b^{2(n-1)}+2b^{n-1}} } \\ + &=& \displaystyle{ \frac{4b^{e+1}}{b^{n-1}+2} } \\ + &<& 4b^{e-n+2} \vspace{1em} \\ + {\sf width} ( {\bf Info} ( D_{b-1}^e \mathfrak{D}_c^n ) ) &\ge& + \displaystyle{ \frac{4b^{e+n}}{(b^n+b^n-1)^2-1} } \\ + &=& \displaystyle{ \frac{4b^{e+n}}{4b^{2n}-4b^n} } \\ + &=& \displaystyle{ \frac{b^e}{b^n-1} } \\ + &>& b^{e-n}. + \end{array} \] + \end{proof} + +Therefore, as soon as we get a digit in base $b$ which is not $D_{b-1}$, + i.e. when we determine a natural number $e$, we may use the formula + above to calculate the total number of digit matrices which will + guarantee the absolute tolerance we wish to achieve. + + +\subsection{$S_- D_{d_1} D_{d_2} \ldots$} \label{subsection sneg} +This case is basically the same as in the previous section. In the base + $b$, the sequence $S_- D_{-(b-1)} D_{-(b-1)} D_{-(b-1)} \ldots$ will + represent $\infty$. Hence, any attempt to obtain an absolute + precision will be futile. For any other sequence we can use a + variation of Proposition~\ref{prop:Spos and width of information with + base b}, in which $D_{-(b-1)}$ takes the position of $D_{b-1}$. + + +\subsection{$S_\infty D_{d_1} D_{d_2} \ldots$} +As we have seen earlier in Sections \ref{subsection spos} and + \ref{subsection sneg} the information of an EFP may contain $\infty$. + Of course, that will prevent us obtaining any absolute precision. That + is also the case when the sign digit of an EFP is $S_\infty$. We have + the following: + \begin{prop} \label{prop:the information containing infty} + The information of an EFP $S_\infty \mathfrak{D}_c^n$ will contain + $\infty$ if and only if $|c| \le 1$, i.e. $c=-1,0,1$. + \end{prop} + \begin{proof} + We have: + \[ \begin{array}{rcl} + {\bf Info} (S_\infty \mathfrak{D}_c^n) &=& \begin{pmatrix} 1&1\\-1&1 + \end{pmatrix} \begin{pmatrix} b^n+c+1 & b^n+c-1\\ b^n-c-1 & b^n-c+1 + \end{pmatrix} [0,\infty] \\ + &=& \begin{pmatrix} b^n & b^n \\ -1-c & 1-c \end{pmatrix} [0,\infty] \\ + &=& \displaystyle{ \left[ \frac{b^n}{1-c}, \frac{b^n}{-1-c} \right] }. + \end{array} \] + If $c \ge 2$ then $-1-c < 1-c <0$ which implies + \[ -\infty < \frac{b^n}{1-c} < \frac{b^n}{-1-c} < 0. \] + Similarly, if $c \le -2$ the interval ${\bf Info} (S_\infty + \mathfrak{D}_c^n )$ does not contain $\infty$. On the other hand, each + of the three intervals below: + \[ \begin{array}{rcl} + {\bf Info} (S_\infty \mathfrak{D}_{-1}^n) &=& \displaystyle{ \left[ + \frac{b^n}{2}, \infty \right] }, \\ + {\bf Info} (S_\infty \mathfrak{D}_0^n) &=& [b^n,-b^n], \\ + {\bf Info} (S_\infty \mathfrak{D}_1^n) &=& \displaystyle{ \left[ + \infty, -\frac{b^n}{2} \right] }, + \end{array} \] + contain $\infty$. This completes the proof. + \end{proof} + Note that $c(d_1,d_2,\ldots,d_n)=0$ iff $d_1=d_2=\ldots=d_n=0$. + Furthermore, $c(d_1,d_2,\ldots,d_n)$ is $1$, respectively $-1$, iff the + product of digit matrices $D_{d_1} D_{d_2} \ldots D_{d_n}$ is of the form + $D_0^e D_1 D_{-(b-1)}^{n-e-1}$, respectively $D_0^e D_{-1} D_{b-1}^{n-e-1}$, + for some $e \in \mathbb{N},\ e < n$. + \begin{prop} \label{prop:dneg db-1 = dzer dneg} + The following holds: + \[ \begin{array}{c} + D_{-1} D_{b-1} = D_0 D_{-1} \\ + D_1 D_{-(b-1)} = D_0 D_1 + \end{array} \] + \end{prop} + \begin{proof} + As $-1 \cdot b + (b-1) = -1$ we have that $D_{-1} D_{b-1} = + \mathfrak{D}_{-1}^2$. Similarly, $D_0 D_{-1} = \mathfrak{D}_{-1}^2$. + \end{proof} + +When the information of $S_\infty D_{d_1} D_{d_2} \ldots$ becomes bounded + ($|c|>1$) we can calculate the number of digits which will guarantee + any required absolute precision. We can do that with the help of the + following two propositions: + \begin{prop} \label{prop:Sinf and width of information with base b 1} + Let $S_\infty D_0^e D_{-1} D_{b-1}^f D_{d_1} D_{d_2} \ldots D_{d_n}$ + be a finite product of matrices in base $b$ with $d_1 \ne (b-1)$ + (that is, the information of such a product is a bounded interval). Then: + \[ \frac{1}{2} b^{e+f-n+1} < {\sf width} ( {\bf Info} ( S_\infty + D_0^e D_{-1} D_{b-1}^f \mathfrak{D}_c^n ) ) < 2b^{e+f-n+3}, \] + where $\mathfrak{D}_c^n = D_{d_1} D_{d_2} \ldots D_{d_n}$. + \end{prop} + \begin{proof} + Because of Proposition \ref{prop:dneg db-1 = dzer dneg} we have + $D_{-1} D_{b-1}^f = D_0^f D_{-1}$ and hence we can assume $f=0$ + and at the end, replace $e$ by $e+f$. We have: + \[ \begin{array}{rcl} + {\bf Info} (S_\infty D_0^e D_{-1} \mathfrak{D}_c^n) &=& + \begin{pmatrix} b^{e+n+1} & b^{e+n+1} \\ b^n-c-1 & b^n-c+1 + \end{pmatrix} [0,\infty] \\ + &=& \displaystyle{ \left[ \frac{b^{e+n+1}}{b^n-c+1}, + \frac{b^{e+n+1}}{b^n-c-1} \right]. } + \end{array} \] + Therefore, + \[ \begin{array}{rcl} + {\sf width} ( {\bf Info} ( S_\infty D_0^e D_{-1} + \mathfrak{D}_c^n ) ) &=& \displaystyle{ \frac{b^{e+n+1}}{b^n-c-1} + - \frac{b^{e+n+1}}{b^n-c+1} } \\ + &=& \displaystyle{ \frac{2b^{e+n+1}}{(b^n-c)^2-1}. } + \end{array} \] + As in the proof of the Proposition \ref{prop:Spos and width of + information with base b} we show that $-(b^n-1) \le c \le + (b-1)b^{n-1}-1$, which implies: + \[ \begin{array}{rcl} + {\sf width} ( {\bf Info} ( S_\infty D_0^e D_{-1} + \mathfrak{D}_c^n ) ) &=& \displaystyle{ + \frac{2b^{e+n+1}}{(b^n-c)^2-1} } \\ + &\le& \displaystyle{ \frac{2b^{e+n+1}}{(b^n-(b-1)b^{n-1}+1)^2 - 1} } \\ + &=& \displaystyle{ \frac{2b^{e+n+1}}{b^{2(n-1)}+2b^{n-1}} } \\ + &=& \displaystyle{ \frac{2b^{e+2}}{b^{n-1}+2} } \\ + &<& 2b^{e-n+3} \vspace{1em} \\ + {\sf width} ( {\bf Info} ( S_\infty D_0^e D_{-1} + \mathfrak{D}_c^n ) ) &\ge& \displaystyle{ + \frac{2b^{e+n+1}}{(b^n+b^n-1)^2-1} } \\ + &=& \displaystyle{ \frac{2b^{e+n+1}}{4b^{2n}-4b^n} } \\ + &=& \displaystyle{ \frac{b^{e+1}}{2(b^n-1)} } \\ + &>& \displaystyle{ \frac{1}{2} b^{e-n+1}. } + \end{array} \] + \end{proof} + \begin{prop} \label{prop:Sinf and width of information with base b 2} + Let $S_\infty D_0^e D_1 D_{-(b-1)}^f D_{d_1} D_{d_2} \ldots D_{d_n}$ + be a finite product of matrices in base $b$ with $d_1 \ne + -(b-1)$ (that is, the information of such a product is a + bounded interval). Then: + \[ \frac{1}{2} b^{e+f-n+1} < {\sf width} ( {\bf Info} ( S_\infty + D_0^e D_1 D_{-(b-1)}^f \mathfrak{D}_c^n ) ) < 2b^{e+f-n+3}, \] + where $\mathfrak{D}_c^n = D_{d_1} D_{d_2} \ldots D_{d_n}$. + \end{prop} + + +\subsection{Absolute Decimal Precision in Base $b=2$} +Usually we want to obtain the decimal precision of a given number. + In addition, base $b=2$ is the most used base in both theory + and practise. Therefore, the issue of obtaining the absolute decimal + precision in base $b=2$ is of a great importance \cite{errhec00}. + +Of course, we can use the propositions proved above, but we will use, + for performance reasons, better bounds, which we can obtain + because we take more digits in base $b=2$ into account. + + +\subsubsection{$S_0 D_{d_1} D_{d_2} \ldots$} +This case is quite easy. If we choose + \begin{equation} + n=\lceil 1 + 3.322 k \rceil, + \end{equation} + where $k$ is the required number of correct decimal digits, we have: + \[ \begin{array}{lrl} + & n & = \lceil 1 + 3.322 k \rceil, \\ + \Rightarrow & n & > 1 + k \log_2 10, \\ + \Rightarrow & -k \log_2 10 & > 1 - n, \\ + \Rightarrow & 10^{-k} & > 2^{1-n} \\ + && = {\sf width} ( {\bf Info} (S_0 D_{d_1} D_{d_2} \ldots D_{d_n} ) ). + \end{array} \] + + +\subsubsection{$S_+ D_{d_1} D_{d_2} \ldots,\ S_- D_{d_1} D_{d_2} \ldots$} +The following proposition is given in \cite{pot98}, page 129. ??????? + Check if it is correct or not ????????? + \begin{prop} \label{prop:width of information with base 2} + For any $e \in \mathbb{N},\ \alpha \in \{-1,0\},\ \beta \in + \{-1,0,1\}$ and $\gamma \in \mathbb{Z}$, if + \[ n = e - 1 - \gamma + (1+\alpha)(1+\beta) \] + then + \[ 2^{\gamma-1} < {\sf width} ( {\bf Info} (D_1^e D_\alpha + D_\beta \mathfrak{D}_c^n )) < 2^{\gamma+1} \] + for all $c \in \mathbb{Z}(2^n)$. + \end{prop} + +Suppose that we have a real number whose EFP represenation is given by + $S_+ D_{d_1} D_{d_2} \ldots$. Provided that $e$, the number of leading + digit matrices $D_1$ is finite (i.e. the number is not $\infty$), we + will calculate correctly the number up to $k$ decimal digits by + emitting not more than $e+2+n$ digit matrices, where + \begin{equation} + n = \lceil e + 3.322 k + 2 \rceil. + \end{equation} + We use $3.322$ as an upper bound for $\log_2 10$. The reasoning is + as follows: + \[ \begin{array}{lrl} + & n & = \lceil e + 3.322 k + 2 \rceil, \\ + \Rightarrow & n & > e + k \log_2 10 + 2, \\ + \Rightarrow & -k \log_2 10 & > e - n + 2, \\ + \Rightarrow & 10^{-k} & > 2^{e-n+2} \\ + && \ge 2^{e-n+(1+\alpha)(1+\beta)} \\ + && = 2^{\gamma + 1}, + \end{array} \] + where $\gamma = e-n-1+(1+\alpha)(1+\beta)$. By Proposition + \ref{prop:width of information with base 2}: + \[ {\sf width} ( {\bf Info} (D_1^e D_\alpha D_\beta + \mathfrak{D}_c^n )) < 2^{\gamma+1} < 10^{-k} \] + for all $c \in \mathbb{Z}(2^n)$. + +The same conclusion can be used in the case $S_- D_{d_1} D_{d_2} \ldots$. + The only difference is that $e$ is the number of leading digit matrices + $D_{-1}$. + + +\subsubsection{$S_\infty D_{d_1} D_{d_2} \ldots$} +If the sign digit is $S_0$, we do not have problems to yield any required + absolute precision. The information of $S_0$ is bounded interval and + every digit matrix will half the previous interval. In the case when + the sign digit is $S_+$ any conclusion is postponed until we get one + {\sc good} digit. By {\em good} digit in this case we mean a digit which + is not $D_1$ (recall that $S_+ D_1 D_1 \ldots$ represents $\infty$). + Then we will get a bounded interval (one which does not contain + $\infty$) and every subsequent digit will refine that interval. + Basically, we require that $e$, the number of leading digits $D_1$, is + finite. Similarly, if the sign is $S_-$ a {\em good} digit is a digit + which is not $D_{-1}$. + +Using Proposition \ref{prop:the information containing infty} is easy to + check that in the case when the leading matrix is $S_\infty$, we need two + {\em good} digits. The first {\em good} digit is $D_{-1}$, respectively + $D_1$, while the second one is either $D_{-1}$ or $D_0$, respectively + $D_0$ or $D_1$. The reason is that all of the sequences: + \[ \begin{array}{ll} + S_\infty D_0 D_0 \ldots &(\Leftrightarrow c=0) \\ + S_\infty D_0^e D_{-1} D_1 D_1 \ldots &(\Leftrightarrow c=-1) \\ + S_\infty D_0^e D_1 D_{-1} D_{-1} \ldots &(\Leftrightarrow c=1) + \end{array} \] + represent $\infty$. + +Once the information of $S_\infty D_{d_1} D_{d_2} \ldots$ is either + positive or negative (we got the first {\em good} digit) we can make + use of the proposition below. + \begin{prop} For $e,f \in \mathbb{N}$ we have: + \[ \begin{array}{c} + {\sf width} ( {\bf Info} ( S_\infty D_0^e D_{-1} D_1^f + \mathfrak{D}_c^n ) ) = {\sf width} ( {\bf Info} ( S_+ D_1^{e+f} + \mathfrak{D}_c^n ) ), \\ + {\sf width} ( {\bf Info} ( S_\infty D_0^e D_1 D_{-1}^f + \mathfrak{D}_c^n ) ) = {\sf width} ( {\bf Info} ( S_- D_{-1}^{e+f} + \mathfrak{D}_c^n ) ). + \end{array} \] + \end{prop} + \begin{proof} + Let us first prove the first equality. From proofs of + Proposition~\ref{prop:Spos and width of information with base b} and + Proposition~\ref{prop:Sinf and width of information with base b 1} we get: + \[ \begin{array}{rcl} + {\bf Info} (S_+ D_1^{e+f} \mathfrak{D}_c^n) &=& [A-1,B-1], \\ + {\bf Info} (S_\infty D_0^{e+f} D_{-1} \mathfrak{D}_c^n ) + &=& [A,B] + \end{array} \] + where + \[ A=\frac{2^{n+e+f+1}}{2^n-c+1} \qquad B=\frac{2^{n+e+f+1}}{2^n-c-1}. \] + This implies the first equality. Similarly, we prove the second one. + \end{proof} + The proposition above enables us to use Proposition \ref{prop:width of + information with base 2} in order to determine the number of necessary + digits which will produce required absolute decimal precision. + Provided that $e$ and $f$ are finite numbers, i.e. we got two {\em good} + digits, in order to achieve absolute decimal precision of $10^{-k},\ k + \in \mathbb{N}$ we need not more than $e+f+2+n$ digit matrices, where + \[ n = \lceil e+f+ 3.322k + 2 \rceil. \] + + +\section{The Base Interval $[-1,1]$} +Comparing with $[0,\infty]$, the base interval $[-1,1]$ has an obvious + disadvantage in amount of effort required to calculate the information + of a matrix $M=\begin{pmatrix} a&c\\b&d \end{pmatrix}$: ${\bf Info}M= + [\frac{c-a}{d-b},\frac{c+a}{d+b}]$ if $\det M > 0$ or ${\bf Info}M= + [\frac{c+a}{d+b}, \frac{c-a}{d-b}]$ if $\det M < 0$. Furthermore, + testing the refining property is more complex with $[-1,1]$ as the + base interval ($|M(-1)| = |\frac{c-a}{d-b}| \le 1$ and $|M(1)| = + |\frac{c+a}{d+b}| \le 1$), comparing it with $[0,\infty]$ as the base + interval ($a,b,c$ and $d$ are of the same sign). + +Despite drawbacks above, it seems that $[-1,1]$ as the base interval + pays off at later stages, since digit matrices, which are given below, + the representation of the functions by tensors, emission and absorbtion, + \cite{edapot97, pot98}, are simpler due to more zeros which appear in + such representations. Pros and cons are discussed in more details in + \cite{hec99}. + +The four possible sign matrices are given as follows: + \[ \begin{array}{rclcrcl} + S^0 &=& \begin{pmatrix} 1&0 \\ 0&1 \end{pmatrix} = \textrm{Id}, &\qquad& + \textbf{Info}(S^0) &=& [-1,1], \vspace{0.5em} \\ + S^1 &=& \begin{pmatrix} 1&1 \\ -1&1 \end{pmatrix}, &\qquad& + \textbf{Info}(S^1) &=& [0,\infty], \vspace{0.5em} \\ + S^2 &=& \begin{pmatrix} 0&-1 \\ 1&0 \end{pmatrix}, &\qquad& + \textbf{Info}(S^2) &=& [1,-1], \vspace{0.5em} \\ + S^3 &=& \begin{pmatrix} 1&-1 \\ 1&1 \end{pmatrix}, &\qquad& + \textbf{Info}(S^3) &=& [\infty,0]. + \end{array} \] + The indices may be observed as exponents as $S^i S^j = S^{(i+j) \mod 4}$. + Digit matrices in base $b$ are given by: + \[ A_k = \begin{pmatrix} 1&k\\ 0&b \end{pmatrix}, \] + for integer $k$ such that $|k| < b$. $A_k$ maps $[-1,1]$ into + the interval$[\frac{k-1}{b},\frac{k+1}{b}]$, whose length is $2/b$. + A product $A_{d_1} A_{d_2} \ldots A_{d_n}$ corresponds to a real number + $r = \sum_{i=1}^n d_i b^{-i} \in [-1,1]$. + +When $b=2$ we get three matrices ($k=-1,0,1$): + \[ \begin{array}{rclcl} + A_{-1} &=& \begin{pmatrix} 1&-1 \\0&2 \end{pmatrix}, &\qquad& + \textbf{Info}(A_{-1}) = [-1,0], \vspace{0.5em} \\ + A_0 &=& \begin{pmatrix} 1&0\\0&2 \end{pmatrix}, &\qquad& + \textbf{Info}(A_0) = [-\frac{1}{2},-\frac{1}{2}], \vspace{0.5em} \\ + A_1 &=& \begin{pmatrix} 1&1\\0&2 \end{pmatrix}, &\qquad& + \textbf{Info}(A_1) = [0,1]. + \end{array} \] + Then, the product of digits $A_{d_1} A_{d_2} \ldots A_{d_n}$ corresponds + to well--known signed binary representation of a number from $[-1,1]$. + +It is easy to check that there exists isomorphism between representations + with base intervals $[0,\infty$ and $[-1,1]$. Every EFP with base + interval $[-1,1]$ can be easily translated into EFP with base $[0,\infty]$: + \[ \begin{array}{rcl} + S^i A_{d_1} \ldots A_{d_n} &=& S^i A_{d_1} \ldots A_{d_n} \\ + &=& S^i (S^3 S^1) A_{d_1} (S^3 S^1) \ldots (S^3 S^1) A_{d_n} (S^3 S^1) \\ + &=& (S^i S^3) (S^1 A_{d_1} S^3) (S^1 \ldots S^3) (S^1 A_{d_n} S^3) S^1 \\ + &=& S^{i+3} D_{d_1} \ldots D_{d_n} S^1. + \end{array} \] + We used the facts that $S^3 S^1 = S^0 = {\textrm Id}$, $D_{d_i} = + S^1 A_{d_i} S^3$. As $S^1 [-1,1] = [0,\infty]$ we have that + \[ \begin{array}{rcl} + {\bf Info}_{[-1,1]} (S^i A_{d_1} \ldots A_{d_n}) &=& + (S^i A_{d_1} \ldots A_{d_n}) [-1,1] \\ + &=& S^{i+3} D_{d_1} \ldots D_{d_n} S^1 [-1,1] \\ + &=& {\bf Info}_{[0,\infty]} (S^{i+3} D_{d_1} \ldots D_{d_n}). + \end{array} \] + +Therefore, trying to obtain any absolute accuracy from EFP which is given + by $S^i A_{d_1} A_{d_2} \ldots$ with the base interval $[-1,1]$ is + equivalent to problem of obtaining the same absolute accuracy from + $S^{i+3} D_{d_1} D_{d_2} \ldots$ with $[0,\infty]$ as the base interval. + We have: + \[ \begin{array}{ccc} + S^0 A_{d_1} A_{d_2} \ldots A_{d_n} [-1,1] &\Longleftrightarrow& + S_0 D_{d_1} D_{d_2} \ldots D_{d_n} [0,\infty], \vspace{0.5em} \\ + S^1 A_{d_1} A_{d_2} \ldots A_{d_n} [-1,1] &\Longleftrightarrow& + S_+ D_{d_1} D_{d_2} \ldots D_{d_n} [0,\infty], \vspace{0.5em} \\ + S^2 A_{d_1} A_{d_2} \ldots A_{d_n} [-1,1] &\Longleftrightarrow& + S_\infty D_{d_1} D_{d_2} \ldots D_{d_n} [0,\infty], \vspace{0.5em} \\ + S^3 A_{d_1} A_{d_2} \ldots A_{d_n} [-1,1] &\Longleftrightarrow& + S_- D_{d_1} D_{d_2} \ldots D_{d_n} [0,\infty]. + \end{array} \] + + +\subsection{Alternative Approaches with Base Interval $[-1,1]$} +We will mention another two approaches, namely {\sc mantissa--exponent + approach} and {\sc integer part--fractional part approach}. In the + former, any real number $x \in \mathbb{R}$ can be represented in base + $b$ as $x=b^e u$, where $e$ is a non--negative integer and $u = + \sum d_i b^{-i} \in [-1,1]$. This corresponds to the product of matrices + $\begin{pmatrix} b^e&0 \\ 0&1 \end{pmatrix} A_{d_1} A_{d_2} \ldots$. + Obtaining any required absolute precision in this approach is + straightforward. As each of digit matrices in base $b$, $A_{d_i}$, + contracts distances by $1/b$, the product: + \[ \begin{pmatrix} b^e&0 \\ 0&1 \end{pmatrix} A_{d_1} A_{d_2} \ldots + A_{d_{e+k}} \] + will induce an interval whose length is $2b^{-k}$, for any $k \in + \mathbb{N}$. + +In the integer part--fractional part approach, a real number $x \in + \mathbb{R}$ is represented as $x=e+u$, where $e$ is an integer and + $u = \sum d_i b^{-i} \in [-1,1]$. Obtaining an absolute precision for $x$ + is even simpler. Calculating $u$ within the same absolute precision will + solve the problem. The product of $k$ digit matrices, $A_{d_1} A_{d_2} + \ldots A_{d_k}$ will induce an interval of the length $2b^{-k}$. Hence, + $x=e+u$ will be calculated with error not greater than $2b^{-k}$. + + +\section*{Acknowledgements} +I would like to thank Reinhold Heckmann for all his help. + + +\begin{thebibliography}{99} + \bibitem{eda97} Edalat, A.: + Domains for Computation in Mathemetics, Physics and Exact + Real Arithmetic. + Bulletin of Symbolic Logic, Vol.~3 (1997). + + \bibitem{edapot97} Edalat, A., Potts, P.~J.: + A New Representation for Exact Real Numbers. + Electronic Notes in Theoretical Computer Science, Vol.~6 (1997). + + \bibitem{errhec00} Errington, L., Heckmann, R.: + Using the C--LFT Library (2000). + + \bibitem{hec99} Heckmann, R.: + How Many Argument Digits are Needed to Produce $n$ + Result Digits? Electronic Notes in Theoretical Computer Science, + Vol.~24 (2000). + + \bibitem{niekor95} Nielsen, A., Kornerup P.: + MSB--First Digit Serial Arithmetic. + Journal of Univ. Comp. Science, 1(7):523--543 (1995). + + \bibitem{pot98} Potts, P.~J.: + Exact Real Arithmetic Using M\"obius Transformations. + PhD Thesis, University of London, Imperial College (1998). + + \bibitem{vui90} Vuillemin, J.~E.: + Exact Real Computer Arithmetic with Continued Fractions. + IEEE Transactions on Computers, 39(8):1087--1105 (1990). +\end{thebibliography} + + +\end{document}
\ No newline at end of file diff --git a/ic-reals-6.3/doc/manual/collect-eps-converted-to.pdf b/ic-reals-6.3/doc/manual/collect-eps-converted-to.pdf Binary files differnew file mode 100644 index 0000000..93ebb2e --- /dev/null +++ b/ic-reals-6.3/doc/manual/collect-eps-converted-to.pdf diff --git a/ic-reals-6.3/doc/manual/collect.eps b/ic-reals-6.3/doc/manual/collect.eps new file mode 100644 index 0000000..bc82e8e --- /dev/null +++ b/ic-reals-6.3/doc/manual/collect.eps @@ -0,0 +1,68 @@ +%!PS-Adobe-2.0 EPSF-2.0 +%%Title: /home/le/Work/reals/blue/5-c-reals/icons/collect.ps +%%Creator: XV Version 3.10a Rev: 12/29/94 (PNG patch 1.2) - by John Bradley +%%BoundingBox: 289 418 301 430 +%%Pages: 1 +%%DocumentFonts: +%%EndComments +%%EndProlog + +%%Page: 1 1 + +% remember original state +/origstate save def + +% build a temporary dictionary +20 dict begin + +% define string to hold a scanline's worth of data +/pix 3 string def + +% define space for color conversions +/grays 18 string def % space for gray scale line +/npixls 0 def +/rgbindx 0 def + +% lower left corner +289 418 translate + +% size of image (on paper, in 1/72inch coords) +11.59200 11.59200 scale + +% dimensions of data +18 18 1 + +% mapping matrix +[18 0 0 -18 0 18] + +{currentfile pix readhexstring pop} +image +ffffff +ffffff +c3f0ff +81e07f +18c63f +3ccf3f +3fcfff +3fcfff +3fcfff +30cfff +30cfff +3ccfff +3ccf3f +18c63f +81e07f +c3f0ff +ffffff +ffffff + + +showpage + +% stop using temporary dictionary +end + +% restore original state +origstate restore + +%%Trailer diff --git a/ic-reals-6.3/doc/manual/continue-eps-converted-to.pdf b/ic-reals-6.3/doc/manual/continue-eps-converted-to.pdf Binary files differnew file mode 100644 index 0000000..7b413ff --- /dev/null +++ b/ic-reals-6.3/doc/manual/continue-eps-converted-to.pdf diff --git a/ic-reals-6.3/doc/manual/continue.eps b/ic-reals-6.3/doc/manual/continue.eps new file mode 100644 index 0000000..da762ab --- /dev/null +++ b/ic-reals-6.3/doc/manual/continue.eps @@ -0,0 +1,68 @@ +%!PS-Adobe-2.0 EPSF-2.0 +%%Title: /home/le/Work/reals/blue/5-c-reals/icons/continue.ps +%%Creator: XV Version 3.10a Rev: 12/29/94 (PNG patch 1.2) - by John Bradley +%%BoundingBox: 289 418 301 430 +%%Pages: 1 +%%DocumentFonts: +%%EndComments +%%EndProlog + +%%Page: 1 1 + +% remember original state +/origstate save def + +% build a temporary dictionary +20 dict begin + +% define string to hold a scanline's worth of data +/pix 3 string def + +% define space for color conversions +/grays 18 string def % space for gray scale line +/npixls 0 def +/rgbindx 0 def + +% lower left corner +289 418 translate + +% size of image (on paper, in 1/72inch coords) +11.59200 11.59200 scale + +% dimensions of data +18 18 1 + +% mapping matrix +[18 0 0 -18 0 18] + +{currentfile pix readhexstring pop} +image +ffffff +ffffff +c000ff +c000ff +ffffff +ffffff +c000ff +e001ff +e001ff +f003ff +f807ff +f807ff +fc0fff +fe1fff +fe1fff +ff3fff +ffffff +ffffff + + +showpage + +% stop using temporary dictionary +end + +% restore original state +origstate restore + +%%Trailer diff --git a/ic-reals-6.3/doc/manual/go-eps-converted-to.pdf b/ic-reals-6.3/doc/manual/go-eps-converted-to.pdf Binary files differnew file mode 100644 index 0000000..ea22606 --- /dev/null +++ b/ic-reals-6.3/doc/manual/go-eps-converted-to.pdf diff --git a/ic-reals-6.3/doc/manual/go.eps b/ic-reals-6.3/doc/manual/go.eps new file mode 100644 index 0000000..454833b --- /dev/null +++ b/ic-reals-6.3/doc/manual/go.eps @@ -0,0 +1,68 @@ +%!PS-Adobe-2.0 EPSF-2.0 +%%Title: /home/le/Work/reals/blue/5-c-reals/icons/go.ps +%%Creator: XV Version 3.10a Rev: 12/29/94 (PNG patch 1.2) - by John Bradley +%%BoundingBox: 289 418 301 430 +%%Pages: 1 +%%DocumentFonts: +%%EndComments +%%EndProlog + +%%Page: 1 1 + +% remember original state +/origstate save def + +% build a temporary dictionary +20 dict begin + +% define string to hold a scanline's worth of data +/pix 3 string def + +% define space for color conversions +/grays 18 string def % space for gray scale line +/npixls 0 def +/rgbindx 0 def + +% lower left corner +289 418 translate + +% size of image (on paper, in 1/72inch coords) +11.59200 11.59200 scale + +% dimensions of data +18 18 1 + +% mapping matrix +[18 0 0 -18 0 18] + +{currentfile pix readhexstring pop} +image +ffffff +ffffff +cfffff +c3ffff +c0ffff +c03fff +c00fff +c003ff +c000ff +c000ff +c003ff +c00fff +c03fff +c0ffff +c3ffff +cfffff +ffffff +ffffff + + +showpage + +% stop using temporary dictionary +end + +% restore original state +origstate restore + +%%Trailer diff --git a/ic-reals-6.3/doc/manual/manual.aux b/ic-reals-6.3/doc/manual/manual.aux new file mode 100644 index 0000000..3514aca --- /dev/null +++ b/ic-reals-6.3/doc/manual/manual.aux @@ -0,0 +1,30 @@ +\relax +\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {2}Copyright}{2}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {3}Installation}{2}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {4}Using the library}{3}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {5}Types}{3}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {6}Arithmetic}{4}{}\protected@file@percent } +\@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Primitive arithmetic functions}}{4}{}\protected@file@percent } +\newlabel{arith-table}{{1}{4}} +\@writefile{toc}{\contentsline {section}{\numberline {7}Special functions}{5}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {8}Forcing, printing and conversion}{6}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {9}Predicates, Boolean operations and conditionals}{8}{}\protected@file@percent } +\@writefile{lot}{\contentsline {table}{\numberline {2}{\ignorespaces Predicates on reals}}{8}{}\protected@file@percent } +\newlabel{pred}{{2}{8}} +\@writefile{lot}{\contentsline {table}{\numberline {3}{\ignorespaces Boolean operators}}{9}{}\protected@file@percent } +\newlabel{Bool-Ops}{{3}{9}} +\@writefile{lot}{\contentsline {table}{\numberline {4}{\ignorespaces Action of the predicate \texttt {gtEq{\_}R{\_}0}}}{9}{}\protected@file@percent } +\newlabel{Truth-values}{{4}{9}} +\@writefile{lot}{\contentsline {table}{\numberline {5}{\ignorespaces Action of the Boolean operators}}{10}{}\protected@file@percent } +\newlabel{op-action}{{5}{10}} +\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Example of conditional with delays.}}{12}{}\protected@file@percent } +\newlabel{fig:conditionals}{{1}{12}} +\@writefile{toc}{\contentsline {section}{\numberline {10}Extracting digits following forcing}{13}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {11}Environment variables}{13}{}\protected@file@percent } +\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Taking digits one-by-one.}}{14}{}\protected@file@percent } +\newlabel{fig:digits-info}{{2}{14}} +\@writefile{toc}{\contentsline {section}{\numberline {12}The daVinci interface}{15}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {13}Compilation flags}{16}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {14}Problems}{16}{}\protected@file@percent } +\gdef \@abspage@last{16} diff --git a/ic-reals-6.3/doc/manual/manual.log b/ic-reals-6.3/doc/manual/manual.log new file mode 100644 index 0000000..40fe007 --- /dev/null +++ b/ic-reals-6.3/doc/manual/manual.log @@ -0,0 +1,324 @@ +This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Parabola GNU/Linux-libre) (preloaded format=pdflatex 2023.10.5) 11 NOV 2023 09:14 +entering extended mode + \write18 enabled. + file:line:error style messages enabled. + %&-line parsing enabled. +**manual.tex +(./manual.tex +LaTeX2e <2022-11-01> patch level 1 +L3 programming layer <2023-02-22> +(/usr/share/texmf-dist/tex/latex/base/article.cls +Document Class: article 2022/07/02 v1.4n Standard LaTeX document class +(/usr/share/texmf-dist/tex/latex/base/size12.clo +File: size12.clo 2022/07/02 v1.4n Standard LaTeX file (size option) +) +\c@part=\count185 +\c@section=\count186 +\c@subsection=\count187 +\c@subsubsection=\count188 +\c@paragraph=\count189 +\c@subparagraph=\count190 +\c@figure=\count191 +\c@table=\count192 +\abovecaptionskip=\skip48 +\belowcaptionskip=\skip49 +\bibindent=\dimen140 +) +(/usr/share/texmf-dist/tex/latex/amsmath/amsmath.sty +Package: amsmath 2022/04/08 v2.17n AMS math features +\@mathmargin=\skip50 + +For additional information on amsmath, use the `?' option. +(/usr/share/texmf-dist/tex/latex/amsmath/amstext.sty +Package: amstext 2021/08/26 v2.01 AMS text + +(/usr/share/texmf-dist/tex/latex/amsmath/amsgen.sty +File: amsgen.sty 1999/11/30 v2.0 generic functions +\@emptytoks=\toks16 +\ex@=\dimen141 +)) +(/usr/share/texmf-dist/tex/latex/amsmath/amsbsy.sty +Package: amsbsy 1999/11/29 v1.2d Bold Symbols +\pmbraise@=\dimen142 +) +(/usr/share/texmf-dist/tex/latex/amsmath/amsopn.sty +Package: amsopn 2022/04/08 v2.04 operator names +) +\inf@bad=\count193 +LaTeX Info: Redefining \frac on input line 234. +\uproot@=\count194 +\leftroot@=\count195 +LaTeX Info: Redefining \overline on input line 399. +LaTeX Info: Redefining \colon on input line 410. +\classnum@=\count196 +\DOTSCASE@=\count197 +LaTeX Info: Redefining \ldots on input line 496. +LaTeX Info: Redefining \dots on input line 499. +LaTeX Info: Redefining \cdots on input line 620. +\Mathstrutbox@=\box51 +\strutbox@=\box52 +LaTeX Info: Redefining \big on input line 722. +LaTeX Info: Redefining \Big on input line 723. +LaTeX Info: Redefining \bigg on input line 724. +LaTeX Info: Redefining \Bigg on input line 725. +\big@size=\dimen143 +LaTeX Font Info: Redeclaring font encoding OML on input line 743. +LaTeX Font Info: Redeclaring font encoding OMS on input line 744. +\macc@depth=\count198 +LaTeX Info: Redefining \bmod on input line 905. +LaTeX Info: Redefining \pmod on input line 910. +LaTeX Info: Redefining \smash on input line 940. +LaTeX Info: Redefining \relbar on input line 970. +LaTeX Info: Redefining \Relbar on input line 971. +\c@MaxMatrixCols=\count199 +\dotsspace@=\muskip16 +\c@parentequation=\count266 +\dspbrk@lvl=\count267 +\tag@help=\toks17 +\row@=\count268 +\column@=\count269 +\maxfields@=\count270 +\andhelp@=\toks18 +\eqnshift@=\dimen144 +\alignsep@=\dimen145 +\tagshift@=\dimen146 +\tagwidth@=\dimen147 +\totwidth@=\dimen148 +\lineht@=\dimen149 +\@envbody=\toks19 +\multlinegap=\skip51 +\multlinetaggap=\skip52 +\mathdisplay@stack=\toks20 +LaTeX Info: Redefining \[ on input line 2953. +LaTeX Info: Redefining \] on input line 2954. +) +(/usr/share/texmf-dist/tex/latex/amsfonts/amsfonts.sty +Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support +\symAMSa=\mathgroup4 +\symAMSb=\mathgroup5 +LaTeX Font Info: Redeclaring math symbol \hbar on input line 98. +LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' +(Font) U/euf/m/n --> U/euf/b/n on input line 106. +) +(/usr/share/texmf-dist/tex/latex/graphics/graphicx.sty +Package: graphicx 2021/09/16 v1.2d Enhanced LaTeX Graphics (DPC,SPQR) + +(/usr/share/texmf-dist/tex/latex/graphics/keyval.sty +Package: keyval 2022/05/29 v1.15 key=value parser (DPC) +\KV@toks@=\toks21 +) +(/usr/share/texmf-dist/tex/latex/graphics/graphics.sty +Package: graphics 2022/03/10 v1.4e Standard LaTeX Graphics (DPC,SPQR) + +(/usr/share/texmf-dist/tex/latex/graphics/trig.sty +Package: trig 2021/08/11 v1.11 sin cos tan (DPC) +) +(/usr/share/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration +) +Package graphics Info: Driver file: pdftex.def on input line 107. + +(/usr/share/texmf-dist/tex/latex/graphics-def/pdftex.def +File: pdftex.def 2022/09/22 v1.2b Graphics/color driver for pdftex +)) +\Gin@req@height=\dimen150 +\Gin@req@width=\dimen151 +) +(/usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def +File: l3backend-pdftex.def 2023-01-16 L3 backend support: PDF output (pdfTeX) +\l__color_backend_stack_int=\count271 +\l__pdf_internal_box=\box53 +) (./manual.aux) +\openout1 = `manual.aux'. + +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 20. +LaTeX Font Info: ... okay on input line 20. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 20. +LaTeX Font Info: ... okay on input line 20. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 20. +LaTeX Font Info: ... okay on input line 20. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 20. +LaTeX Font Info: ... okay on input line 20. +LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 20. +LaTeX Font Info: ... okay on input line 20. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 20. +LaTeX Font Info: ... okay on input line 20. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 20. +LaTeX Font Info: ... okay on input line 20. +(/usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii +[Loading MPS to PDF converter (version 2006.09.02).] +\scratchcounter=\count272 +\scratchdimen=\dimen152 +\scratchbox=\box54 +\nofMPsegments=\count273 +\nofMParguments=\count274 +\everyMPshowfont=\toks22 +\MPscratchCnt=\count275 +\MPscratchDim=\dimen153 +\MPnumerator=\count276 +\makeMPintoPDFobject=\count277 +\everyMPtoPDFconversion=\toks23 +) (/usr/share/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty +Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf +Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4 +85. + +(/usr/share/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg +File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Liv +e +)) +LaTeX Font Info: Trying to load font information for U+msa on input line 21. + + +(/usr/share/texmf-dist/tex/latex/amsfonts/umsa.fd +File: umsa.fd 2013/01/14 v3.01 AMS symbols A +) +LaTeX Font Info: Trying to load font information for U+msb on input line 21. + + +(/usr/share/texmf-dist/tex/latex/amsfonts/umsb.fd +File: umsb.fd 2013/01/14 v3.01 AMS symbols B +) [1 + +{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2{/usr/share/texmf-dist/f +onts/enc/dvips/cm-super/cm-super-ts1.enc}] [3] [4] +Overfull \hbox (9.20828pt too wide) in paragraph at lines 336--338 +\OT1/cmr/m/n/12 The next two func-tions yield the even more com-pli-cated ex-pr +es-sion $[]$: + [] + +[5] +Overfull \hbox (11.72748pt too wide) in paragraph at lines 483--491 +[]\OT1/cmr/m/n/12 There are two ways to spec-ify the amount of forc-ing: the fi +rst, \OT1/cmtt/m/n/12 force[]R[]Digs\OT1/cmr/m/n/12 , + [] + +[6] [7] [8] +Overfull \hbox (0.7466pt too wide) in paragraph at lines 676--682 +[]\OT1/cmr/m/n/12 Roughly spo-ken, the func-tion eval-u-ates the guards $\OML/c +mm/m/it/12 b[]$\OT1/cmr/m/n/12 , ..., $\OML/cmm/m/it/12 b[]$\OT1/cmr/m/n/12 , t +hen chooses + [] + +[9] [10] [11] [12] +Overfull \hbox (1.67105pt too wide) in paragraph at lines 893--895 +[]\OT1/cmr/m/n/12 From a com-pressed digit rep-re-sen-ta-tion as it is pro-vide +d by \OT1/cmtt/m/n/12 retrieveInfo\OT1/cmr/m/n/12 , + [] + +LaTeX Font Info: Font shape `OT1/cmtt/bx/n' in size <12> not available +(Font) Font shape `OT1/cmtt/m/n' tried instead on input line 941. + +Overfull \hbox (9.85213pt too wide) in paragraph at lines 942--951 +\OT1/cmr/m/n/12 than 1, try set-ting the en-vi-ron-ment vari-able \OT1/cmtt/m/n +/12 ICR[]DEFAULT[]FORCE[]COUNT=1 + [] + +[13] [14] +Package epstopdf Info: Source file: <stop.eps> +(epstopdf) date: 2000-07-24 21:06:57 +(epstopdf) size: 990 bytes +(epstopdf) Output file: <stop-eps-converted-to.pdf> +(epstopdf) date: 2023-11-11 09:14:32 +(epstopdf) size: 2598 bytes +(epstopdf) Command: <repstopdf --outfile=stop-eps-converted-to.pdf +stop.eps> +(epstopdf) \includegraphics on input line 998. +Package epstopdf Info: Output file is already uptodate. +<stop-eps-converted-to.pdf, id=60, 12.045pt x 12.045pt> +File: stop-eps-converted-to.pdf Graphic file (type pdf) +<use stop-eps-converted-to.pdf> +Package pdftex.def Info: stop-eps-converted-to.pdf used on input line 998. +(pdftex.def) Requested size: 12.04495pt x 12.04495pt. +Package epstopdf Info: Source file: <go.eps> +(epstopdf) date: 2000-07-24 21:06:57 +(epstopdf) size: 988 bytes +(epstopdf) Output file: <go-eps-converted-to.pdf> +(epstopdf) date: 2023-11-11 09:14:33 +(epstopdf) size: 2599 bytes +(epstopdf) Command: <repstopdf --outfile=go-eps-converted-to.pdf go +.eps> +(epstopdf) \includegraphics on input line 999. +Package epstopdf Info: Output file is already uptodate. +<go-eps-converted-to.pdf, id=61, 12.045pt x 12.045pt> +File: go-eps-converted-to.pdf Graphic file (type pdf) +<use go-eps-converted-to.pdf> +Package pdftex.def Info: go-eps-converted-to.pdf used on input line 999. +(pdftex.def) Requested size: 12.04495pt x 12.04495pt. +Package epstopdf Info: Source file: <step.eps> +(epstopdf) date: 2000-07-24 21:06:57 +(epstopdf) size: 990 bytes +(epstopdf) Output file: <step-eps-converted-to.pdf> +(epstopdf) date: 2023-11-11 09:14:33 +(epstopdf) size: 2603 bytes +(epstopdf) Command: <repstopdf --outfile=step-eps-converted-to.pdf +step.eps> +(epstopdf) \includegraphics on input line 1001. +Package epstopdf Info: Output file is already uptodate. +<step-eps-converted-to.pdf, id=62, 12.045pt x 12.045pt> +File: step-eps-converted-to.pdf Graphic file (type pdf) +<use step-eps-converted-to.pdf> +Package pdftex.def Info: step-eps-converted-to.pdf used on input line 1001. +(pdftex.def) Requested size: 12.04495pt x 12.04495pt. +Package epstopdf Info: Source file: <continue.eps> +(epstopdf) date: 2000-07-24 21:06:57 +(epstopdf) size: 994 bytes +(epstopdf) Output file: <continue-eps-converted-to.pdf> +(epstopdf) date: 2023-11-11 09:14:34 +(epstopdf) size: 2614 bytes +(epstopdf) Command: <repstopdf --outfile=continue-eps-converted-to. +pdf continue.eps> +(epstopdf) \includegraphics on input line 1003. +Package epstopdf Info: Output file is already uptodate. +<continue-eps-converted-to.pdf, id=63, 12.045pt x 12.045pt> +File: continue-eps-converted-to.pdf Graphic file (type pdf) +<use continue-eps-converted-to.pdf> +Package pdftex.def Info: continue-eps-converted-to.pdf used on input line 1003 +. +(pdftex.def) Requested size: 12.04495pt x 12.04495pt. +Package epstopdf Info: Source file: <collect.eps> +(epstopdf) date: 2000-07-24 21:06:57 +(epstopdf) size: 993 bytes +(epstopdf) Output file: <collect-eps-converted-to.pdf> +(epstopdf) date: 2023-11-11 09:14:34 +(epstopdf) size: 2628 bytes +(epstopdf) Command: <repstopdf --outfile=collect-eps-converted-to.p +df collect.eps> +(epstopdf) \includegraphics on input line 1005. +Package epstopdf Info: Output file is already uptodate. +<collect-eps-converted-to.pdf, id=64, 12.045pt x 12.045pt> +File: collect-eps-converted-to.pdf Graphic file (type pdf) +<use collect-eps-converted-to.pdf> +Package pdftex.def Info: collect-eps-converted-to.pdf used on input line 1005. + +(pdftex.def) Requested size: 12.04495pt x 12.04495pt. + [15 <./stop-eps-converted-to.pdf> <./go-eps-converted-to.pdf> <./step-eps-conv +erted-to.pdf> <./continue-eps-converted-to.pdf> <./collect-eps-converted-to.pdf +>] [16] (./manual.aux) ) +Here is how much of TeX's memory you used: + 2206 strings out of 476025 + 33817 string characters out of 5796518 + 1866388 words of memory out of 5000000 + 22652 multiletter control sequences out of 15000+600000 + 522992 words of font info for 73 fonts, out of 8000000 for 9000 + 1141 hyphenation exceptions out of 8191 + 57i,15n,62p,223b,363s stack positions out of 5000i,500n,10000p,200000b,80000s +</usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/c +mbx12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmbxti10.pfb></ +usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/share/texm +f-dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb></usr/share/texmf-dist/fonts/t +ype1/public/amsfonts/cm/cmmi8.pfb></usr/share/texmf-dist/fonts/type1/public/ams +fonts/cm/cmr12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17. +pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/ +texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texmf-dist/fon +ts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texmf-dist/fonts/type1/public +/amsfonts/cm/cmti12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/c +mtt12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb +></usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb> +Output written on manual.pdf (16 pages, 191783 bytes). +PDF statistics: + 137 PDF objects out of 1000 (max. 8388607) + 85 compressed objects within 1 object stream + 0 named destinations out of 1000 (max. 500000) + 26 words of extra memory for PDF output out of 10000 (max. 10000000) + diff --git a/ic-reals-6.3/doc/manual/manual.pdf b/ic-reals-6.3/doc/manual/manual.pdf Binary files differnew file mode 100644 index 0000000..79c12b7 --- /dev/null +++ b/ic-reals-6.3/doc/manual/manual.pdf diff --git a/ic-reals-6.3/doc/manual/manual.tex b/ic-reals-6.3/doc/manual/manual.tex new file mode 100644 index 0000000..db3a1c5 --- /dev/null +++ b/ic-reals-6.3/doc/manual/manual.tex @@ -0,0 +1,1057 @@ +\documentclass[a4paper,12pt]{article} +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage{graphicx} +\parskip=10pt% +\newcommand{\vdist}{\vrule width0pt height2.5ex depth1.0ex\relax} +\title{Using the IC Reals Library} +\author{Lindsay Errington and Reinhold Heckmann} +\newenvironment{funlist}{\begin{list}% + {}% + {\topsep=0pt% + \leftmargin=0cm% + \rightmargin=0cm% + \listparindent=0cm% + \parskip=10pt% + \partopsep=0pt% + \itemsep=0pt% + \parsep=0pt}}% + {\end{list}} +\begin{document} +\maketitle +\newcommand{\Type}[1]{\texttt{#1}} +\newcommand{\Name}[1]{\texttt{#1}} +\newcommand{\Var}[1]{\textit{#1}} +\newcommand{\File}[1]{\textsf{#1}} + +\section{Introduction} +The Imperial College Exact Real Arithmetic Library +is a collection of C types and functions +which implement exact real arithmetic. The functions +allow one to construct objects representing real numbers +and then to demand information, for example some number +of decimal digits, from those objects. The user need not specify a precision +in advance. All the digits retrieved are correct and further digits +can be demanded. + +The library includes arithmetic operations as +well as a suite of analytic functions on reals. +In addition to a real type, the library also includes a lazy boolean +type and a collection of predicates on reals, boolean operations +and a conditional construct. + +The representation of reals is based on \emph{linear fractional +transformations} (LFTs). The underlying theory was developed by +Abbas Edalat, Martin Escardo, Reinhold Heckmann, Peter Potts, Philipp +S\"{u}nderhauf and Lindsay Errington (lazy booleans). + +The library was written by Lindsay Errington with contributions from Marko +Krznaric and Reinhold Heckmann. + +% \cite{}. + +This document describes the types and functions provided by the +library. It is not an introduction to +exact real arithmetic nor does it describe the details of +the LFT approach. + +\section{Copyright} + +All software in this distribution comes under the following copyright notice: + +Copyright \copyright\ 1998-2000 by Imperial College of Science, Technology +and Medicine + +Permission to use, copy, modify, and distribute this software and its +documentation for any non-commercial purpose and without fee is hereby +granted, provided that this copyright notice appears in all copies. +The library cannot be used directly or indirectly for any commercial +application without a licence from Imperial College. + +Neither Imperial College nor Lindsay Errington make representations about +the suitability of this software for any purpose. It is provided ``as is'' +without express or implied warranty. + +\section{Installation} + +To install the library it is necessary to +edit the Makefile and change \texttt{REALDIR} to point to the +root of the Real Library source tree. + +Also, the library requires the GNU Multiple Precision Arithmetic Library +(GMP) (Version 3.1). The Makefile defines a variable +\texttt{GMPDIR} which is assumed to be the root directory of the +GMP installation. + +Assuming the Makefile has been edited such that \texttt{REALDIR} +and \texttt{GMPDIR} point to the respective directories, +then the command +\begin{quote} +\texttt{make} +\end{quote} +will create the real library. To remove the library +and all binaries, type: +\begin{quote} +\texttt{make clean} +\end{quote} + +\section{Using the library} + +All applications which call functions in the library must include +the file \texttt{real.h}. This file defines all the types +and prototypes for all functions exported from the library. +In particular +the file defines the types \Type{Real} and \Type{Bool} corresponding +to lazy reals and lazy booleans. The file \texttt{real.h} includes +\texttt{gmp.h}. + +The user must call the function +\begin{quote} +\texttt{initReals();} +\end{quote} +before invoking any other functions in the library. +This function should be called only once. + +\section{Types} + +The main purpose of the library is to provide +a type \Type{Real} of real numbers. +Since it requires +the GNU Multiple Precision Arithmetic Library (GMP) as well, +it also provides GMP's big integer type \Type{mpz{\_}t} as a byproduct. +Most of the functions defined by the library come in +a number of instances for different types. +These instances are named using suffixes +abbreviating type names; e.g.\ the suffix \Name{R} +indicates the type \Type{Real}. +The full list is given by the following table. + +\begin{tabular}{|l|l|l|} +\hline +\vdist Abbreviation & Prototype & Denotation \\ +\hline +\hline +\vdist \Name{R} + & \Type{Real} \Var{x} + & $\mbox{\Var{x}} : \mathbb{R}$ \\ +\hline +\vdist \Name{Int} + & \Type{int} \Var{x} + & $x : \mathbb{Z}$, $x$ machine integer \\ +\hline +\vdist \Name{Z} + & \Type{mpz{\_}t} \Var{x} + & $x : \mathbb{Z}$, $x$ GMP integer \\ +\hline +\vdist \Name{QInt} + & \Type{int} \Var{a}, \Type{int} \Var{b} + & $\frac{a}{b} : \mathbb{Q}$, $a$, $b$ machine integers \\ +\hline +\vdist \Name{QZ} + & \Type{mpz{\_}t} \Var{a}, \Type{mpz{\_}t} \Var{b} + & $\frac{a}{b} : \mathbb{Q}$, $a$, $b$ GMP integers \\ +\hline +\end{tabular} + +Usually, the specialised functions are more efficient +than the general ones. +The possibility of using machine integers +is particularly useful +since these integers are readily available +and need not be set up specially. +\vspace{-2ex} + +\section{Arithmetic} +\vspace{-2ex} +The basic functions for addition, subtraction, +multiplication and division occur in a general form +operating on two reals, and in various specialised forms +involving integers. +The available functions are listed in Table~\ref{arith-table}. + +\begin{table}[htp] +\begin{center} +\begin{tabular}{|l|c|} +\hline +\begin{tabular}{l} +\vdist\Type{Real} \Name{neg{\_}R}(% + \Type{Real} \Var{x}) +\end{tabular} +& $-x$ \\ +\begin{tabular}{l} +\vdist\Type{Real} \Name{abs{\_}R}(% + \Type{Real} \Var{x}) +\end{tabular} +& $|x|$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Real} \Name{add{\_}R{\_}R}(% + \Type{Real} \Var{x}, + \Type{Real} \Var{y}) \\ +\vdist\Type{Real} \Name{add{\_}R{\_}Int}(% + \Type{Real} \Var{x}, + \Type{int} \Var{y}) \\ +\vdist\Type{Real} \Name{add{\_}R{\_}Z}(% + \Type{Real} \Var{x}, + \Type{mpz{\_}t} \Var{y}) +\end{tabular} +& $x + y$ \\ +\hline +\begin{tabular}{l} + \vdist\Type{Real} \Name{add{\_}R{\_}QInt}(% + \Type{Real} \Var{x}, + \Type{int} \Var{a}, + \Type{int} \Var{b}) \\ + \vdist\Type{Real} \Name{add{\_}R{\_}QZ}(% + \Type{Real} \Var{x}, + \Type{mpz{\_}t} \Var{a}, + \Type{mpz{\_}t} \Var{b}) \\ +\end{tabular} +& $x + \frac{a}{b}$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Real} \Name{sub{\_}R{\_}R}(% + \Type{Real} \Var{x}, + \Type{Real} \Var{y}) \\ +\vdist\Type{Real} \Name{sub{\_}R{\_}Int}(% + \Type{Real} \Var{x}, + \Type{int} \Var{y}) \\ +\vdist\Type{Real} \Name{sub{\_}Int{\_}R}(% + \Type{int} \Var{x}, + \Type{Real} \Var{y}) +\end{tabular} +& $x - y$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Real} \Name{sub{\_}R{\_}QInt}(% + \Type{Real} \Var{x}, + \Type{int} \Var{a}, + \Type{int} \Var{b}) +\end{tabular} +& $x - \frac{a}{b}$ \\ +\begin{tabular}{l} +\vdist\Type{Real} \Name{sub{\_}QInt{\_}R}(% + \Type{int} \Var{a}, + \Type{int} \Var{b}, + \Type{Real} \Var{x}) +\end{tabular} +& $\frac{a}{b} - x$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Real} \Name{mul{\_}R{\_}R}(% + \Type{Real} \Var{x}, + \Type{Real} \Var{y}) \\ +\vdist\Type{Real} \Name{mul{\_}R{\_}Int}(% + \Type{Real} \Var{x}, + \Type{int} \Var{y}) \\ +\vdist\Type{Real} \Name{mul{\_}R{\_}Z}(% + \Type{Real} \Var{x}, + \Type{mpz{\_}t} \Var{y}) \\ +\end{tabular} +& $x \times y$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Real} \Name{mul{\_}R{\_}QInt}(% + \Type{Real} \Var{x}, + \Type{int} \Var{a}, + \Type{int} \Var{b}) \\ +\vdist\Type{Real} \Name{mul{\_}R{\_}QZ}(% + \Type{Real} \Var{x}, + \Type{mpz{\_}t} \Var{a}, + \Type{mpz{\_}t} \Var{b}) \\ +\end{tabular} +& $x \times \frac{a}{b}$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Real} \Name{div{\_}R{\_}R}(% + \Type{Real} \Var{x}, + \Type{Real} \Var{y}) \\ +\vdist\Type{Real} \Name{div{\_}R{\_}Int}(% + \Type{Real} \Var{x}, + \Type{int} \Var{y}) \\ +\vdist\Type{Real} \Name{div{\_}Int{\_}R}(% + \Type{int} \Var{x}, + \Type{Real} \Var{y}) +\end{tabular} +& $\frac{x}{y}$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Real} \Name{div{\_}R{\_}QInt}(% + \Type{Real} \Var{x}, + \Type{int} \Var{a}, + \Type{int} \Var{b}) +\end{tabular} +& $x / \frac{a}{b} = \frac{b x}{a}$ \\[0.5ex] +\begin{tabular}{l} +\vdist\Type{Real} \Name{div{\_}QInt{\_}R}(% + \Type{int} \Var{a}, + \Type{int} \Var{b}, + \Type{Real} \Var{x}) +\end{tabular} +& $\frac{a}{b} / x = \frac{a}{bx}$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Real} \Name{pow{\_}R{\_}R}(% + \Type{Real} \Var{x}, + \Type{Real} \Var{y}) +\end{tabular} +& $x^y$ \\ +\hline +\end{tabular} +\end{center} +\caption{Primitive arithmetic functions}\label{arith-table} +\end{table} + +The following two functions define the rational number $\frac{a}{b}$, +considered as a real: +\begin{funlist} +\item \Type{Real} \Name{real{\_}QInt}(% + \Type{int} \Var{a}, + \Type{int} \Var{b}) +\item \Type{Real} \Name{real{\_}QZ}(% + \Type{mpz{\_}t} \Var{a}, + \Type{mpz{\_}t} \Var{b}) +\end{funlist} + +Real numbers are implemented using \emph{linear fractional +transformations} (LFTs). Users can construct +LFT functions explicitly. +The following two functions compute the expression +$\frac{ax+b}{cx+d}$: +\begin{funlist} +\item \Type{Real} \Name{lft{\_}R{\_}Int}(% + \Type{Real} \Var{x}, + \Type{int} \Var{a}, + \Type{int} \Var{b}, + \Type{int} \Var{c}, + \Type{int} \Var{d}) +\item \Type{Real} \Name{lft{\_}R{\_}Z}(% + \Type{Real} \Var{x}, + \Type{mpz{\_}t} \Var{a}, + \Type{mpz{\_}t} \Var{b}, + \Type{mpz{\_}t} \Var{c}, + \Type{mpz{\_}t} \Var{d}) +\end{funlist} + +\noindent The next two functions yield the even more complicated expression +$\frac{axy + bx + cy + d}{exy + fx + gy + h}$: +\begin{funlist} +\item \Type{Real} \Name{lft{\_}R{\_}R{\_}Int}(% + \Type{Real} \Var{x}, + \Type{Real} \Var{y}, + \Type{int} \Var{a}, + \Type{int} \Var{b}, +\ldots, + % \Type{int} \Var{c}, + % \Type{int} \Var{d}, + % \Type{int} \Var{e}, + % \Type{int} \Var{f}, + % \Type{int} \Var{g}, + \Type{int} \Var{h}) +\item \Type{Real} \Name{lft{\_}R{\_}R{\_}Z}(% + \Type{Real} \Var{x}, + \Type{Real} \Var{y}, + \Type{mpz{\_}t} \Var{a}, + \Type{mpz{\_}t} \Var{b}, +\ldots, + % \Type{mpz{\_}t} \Var{c}, + % \Type{mpz{\_}t} \Var{d}, + % \Type{mpz{\_}t} \Var{e}, + % \Type{mpz{\_}t} \Var{f}, + % \Type{mpz{\_}t} \Var{g}, + \Type{mpz{\_}t} \Var{h}) +\end{funlist} + +\noindent \textbf{Examples:} +\vspace{-1.0ex} +\begin{itemize} +\item To compute $y = x+1$ ($x$ real), use\quad + \verb| y = add_R_Int (x, 1);|\\[0.5ex] + This is both simpler and more efficient than to use\\[0.5ex] + \verb| one = real_QInt (1, 1); y = add_R_R (x, one);| +\item To compute $y = \frac{x+1}{x-1}$, use\\[0.5ex] + \verb| y = lft_R_Int (x, 1, 1, 1, -1);|\\[0.5ex] + This is both simpler and more efficient than to use\\[0.5ex] + \verb| y = div_R_R (add_R_Int (x, 1), sub_R_Int (x, 1));| +\item To compute $z = \frac{2x+y}{xy-1}$, use\\[0.5ex] + \verb| z = lft_R_R_Int (x, y, 0, 2, 1, 0,|\\ + \verb| 1, 0, 0, -1);|\\[0.5ex] + This is both shorter and more efficient than to use\\[0.5ex] + \verb| num = add_R_R (mul_R_Int (x, 2), y);|\\ + \verb| den = sub_R_Int (mul_R_R (x, y), 1);|\\ + \verb| z = div_R_R (num, den);|\\[0.5ex] + (We admit that both versions are not quite readable.) +\end{itemize} + +\section{Special functions} + +There are the usual standard functions, +each existing in three versions, +one for a real argument, one for a rational argument made from machine integers, +and one for a rational argument made from GMP integers. +Often, the rational version will be more efficient +(sometimes, it is just mapped to the real version, + but it is offered anyway for uniformity and convenience). +The general pattern is illustrated at the square root function: + +\begin{funlist} +\item \makebox[6.2cm][l]{\Type{Real} \Name{sqrt{\_}R}(% + \Type{Real} \Var{x})} + to compute $\sqrt{x}$; +\item \makebox[6.2cm][l]{\Type{Real} \Name{sqrt{\_}QInt}(% + \Type{int} \Var{a}, + \Type{int} \Var{b})} + to compute $\sqrt{\frac{a}{b}}$; +\item \makebox[6.2cm][l]{\Type{Real} \Name{sqrt{\_}QZ}(% + \Type{mpz{\_}t} \Var{a}, + \Type{mpz{\_}t} \Var{b})} + to compute $\sqrt{\frac{a}{b}}$. +\end{funlist} +\vspace{-1ex} + +\begin{tabbing} +In the following list of functions, +we enumerate only the `R' versions.\\[0.5ex] +Basic:\quad \Name{sqrt{\_}R} for $\sqrt{x}$,\quad + \Name{exp{\_}R} for $e^x$,\quad + \Name{log{\_}R} for natural logarithm;\\[0.5ex] +Inverse trigonometric: +M \= \Name{asinh{\_}R}, + \= \Name{acosh{\_}R}, + \= \Name{atanh{\_}R}, + \= \Name{asech{\_}R}, + \= \Name{acosech{\_}R}, + \= \Name{acotanh{\_}R} \kill +Trigonometric: + \> \Name{sin{\_}R}, + \> \Name{cos{\_}R}, + \> \Name{tan{\_}R}, + \> \Name{sec{\_}R}, + \> \Name{cosec{\_}R}, + \> \Name{cotan{\_}R} + \\[0.5ex] +Inverse trigonometric: + \> \Name{asin{\_}R}, + \> \Name{acos{\_}R}, + \> \Name{atan{\_}R}, + \> \Name{asec{\_}R}, + \> \Name{acosec{\_}R}, + \> \Name{acotan{\_}R} + \\[0.5ex] +Hyperbolic: + \> \Name{sinh{\_}R}, + \> \Name{cosh{\_}R}, + \> \Name{tanh{\_}R}, + \> \Name{sech{\_}R}, + \> \Name{cosech{\_}R}, + \> \Name{cotanh{\_}R} + \\[0.5ex] +Inverse hyperbolic: + \> \Name{asinh{\_}R}, + \> \Name{acosh{\_}R}, + \> \Name{atanh{\_}R}, + \> \Name{asech{\_}R}, + \> \Name{acosech{\_}R}, + \> \Name{acotanh{\_}R} + \\[0.5ex] +\end{tabbing} +\vspace{-1ex} + +\noindent In addition, there are the two predefined constants +\Type{Real} \Name{Pi} and \Type{Real} \Name{E}. + +\section{Forcing, printing and conversion} + +When working with the library, +it is best to think of real numbers as infinite digit streams +(but these digit expansions do not correspond directly + to any familiar binary or decimal system). +Each finite prefix corresponds to a rational interval +(much as the finite prefix 3.14 of 3.14159\ldots\ +corresponds to the interval [3.14, 3.15]). +Thus, if more and more digits of the stream are computed, +the result is a nested sequence of intervals +$[a_1, b_1] \supseteq [a_2, b_2] \supseteq \cdots$ +which provide increasingly better approximations to the real number. + +If a real number is set up and assigned to a variable, +an object is created which records the way the number was constructed, +but no digits are actually calculated. +It is only when the number is ``forced'' +that a finite prefix of the digit stream is computed. + +There are two ways to specify the amount of forcing: +the first, \Name{force{\_}R{\_}Digs}, +is by indicating the number of digits to be computed. +Unfortunately, there is no simple rule telling +the size of the resulting interval. +This is the reason why there is a second force function, \Name{force{\_}R{\_}Dec}, +which forces a real number until an interval is obtained +which guarantees a certain decimal precision. + +\begin{funlist} +\item \Type{void} \Name{force{\_}R{\_}Digs}(% +\Type{Real} \Var{x}, \Type{int} \Var{n})\\ +This computes at least the first $n$ digits +of the digit stream describing the value of the argument \Var{x}. +\vspace{1ex} +% +\item \Type{void} \Name{force{\_}R{\_}Dec}(% +\Type{Real} \Var{x}, \Type{int} \Var{n})\\ +This computes an approximating interval for $x$ +whose size is at most $10^{-n}$. +\vspace{1ex} +% +\item \Type{void} \Name{print{\_}R}(\Type{Real} \Var{x})\\ +This takes whatever information about the value of \Var{x} +is currently available and prints it as an interval (no forcing). +\vspace{1ex} +% +\item \Type{void} \Name{print{\_}R{\_}Digs}(\Type{Real} \Var{x}, \Type{int} \Var{n})\\ +This first calls \Name{force{\_}R{\_}Digs}(\Var{x}, \Var{n}) +and prints the interval which results from this forcing. +\vspace{1ex} +% +\item \Type{void} \Name{print{\_}R{\_}Dec}(\Type{Real} \Var{x}, \Type{int} \Var{n})\\ +This first calls \Name{force{\_}R{\_}Dec}(\Var{x}, \Var{n}) +and prints the resulting interval. +\vspace{1ex} +% +\item \Type{double} \Name{realToDouble}(\Type{Real} \Var{x})\\ +This takes whatever information about the value of \Var{x} is currently available, +and converts one of the end-points of this interval +to a double precision floating point value. +\vspace{1ex} +% +\item \Type{void} \Name{force{\_}B}(% +\Type{Bool} \Var{b}, \Type{int} \Var{n})\\ +This can be called to force the evaluation of a boolean. When $b$ +is viewed as a stream, the argument $n$ indicates the maximum depth in the +stream to examine to determine the value of the boolean. +\vspace{1ex} +\item \Type{Boolean} \Name{boolValue}(\Type{Bool} \Var{b}) \\ +This is a macro which returns the value of a boolean. This may be +one of three constants: +\Name{LAZY{\_}TRUE}, +\Name{LAZY{\_}FALSE} or +\Name{LAZY{\_}UNKNOWN} +\vspace{1ex} +\item \Type{Real} \Name{realError}(\Type{char}\verb|*| \Var{string})\\ +This function ``computes'' and returns a kind of placeholder +for a real number which is fine as long as it is not forced. +But if this placeholder is forced to produce some digits, +then it causes the program to be aborted. +The argument string provided in the call of \Name{realError} +is printed as an error message. +\item \Type{Real} \Name{realDelay}(\Type{Delay{\_}Fun} \Var{f}, +\Type{Delay{\_}Arg} \Var{x})\\ +This function yields a \emph{closure} for the function +\Var{f} applied to \Var{x}. In other words, it denotes the real +\Var{f}(\Var{x}) but the function call is not made until +the closure is forced. An example of its use is given +in the next section. +\end{funlist} + +\section{Predicates, Boolean operations and conditionals} + +The library introduces a new type \Type{Bool} for Boolean values +which serves as the result type of predicates. +Therefore, it must also introduce its own versions +of Boolean operations and its own conditional, +which is a function reminiscent of Dijkstra's guarded commands. +We shall shortly see why this was done, +but first we introduce the corresponding functions. + +Table~\ref{pred} shows the available predicates: + +\begin{table}[htp] +\begin{center} +\begin{tabular}{|l|l|} +\hline +\begin{tabular}{l} +\vdist\Type{Bool} \Name{lt{\_}R{\_}0}(\Type{Real} \Var{x}) +\end{tabular} +& $x < 0$ \\ +\begin{tabular}{l} +\vdist\Type{Bool} \Name{lt{\_}R{\_}QInt}(\Type{Real} \Var{x}, + \Type{int} \Var{a}, \Type{int} \Var{b}) +\end{tabular} +& $x < \frac{a}{b}$ \\ +\begin{tabular}{l} +\vdist\Type{Bool} \Name{lt{\_}R{\_}R}(\Type{Real} \Var{x}, \Type{Real} \Var{y}) +\end{tabular} +& $x < y$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Bool} \Name{ltEq{\_}R{\_}0}(\Type{Real} \Var{x}) +\end{tabular} +& $x \leq 0$ \\ +\begin{tabular}{l} +\vdist\Type{Bool} \Name{ltEq{\_}R{\_}QInt}(\Type{Real} \Var{x}, + \Type{int} \Var{a}, \Type{int} \Var{b}) +\end{tabular} +& $x \leq \frac{a}{b}$ \\ +\begin{tabular}{l} +\vdist\Type{Bool} \Name{ltEq{\_}R{\_}R}(\Type{Real} \Var{x}, \Type{Real} \Var{y}) +\end{tabular} +& $x \leq y$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Bool} \Name{gt{\_}R{\_}0}(\Type{Real} \Var{x}) +\end{tabular} +& $x > 0$ \\ +\begin{tabular}{l} +\vdist\Type{Bool} \Name{gt{\_}R{\_}QInt}(\Type{Real} \Var{x}, + \Type{int} \Var{a}, \Type{int} \Var{b}) +\end{tabular} +& $x > \frac{a}{b}$ \\ +\begin{tabular}{l} +\vdist\Type{Bool} \Name{gt{\_}R{\_}R}(\Type{Real} \Var{x}, \Type{Real} \Var{y}) +\end{tabular} +& $x > y$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Bool} \Name{gtEq{\_}R{\_}0}(\Type{Real} \Var{x}) +\end{tabular} +& $x \geq 0$ \\ +\begin{tabular}{l} +\vdist\Type{Bool} \Name{gtEq{\_}R{\_}QInt}(\Type{Real} \Var{x}, + \Type{int} \Var{a}, \Type{int} \Var{b}) +\end{tabular} +& $x \geq \frac{a}{b}$ \\ +\begin{tabular}{l} +\vdist\Type{Bool} \Name{gtEq{\_}R{\_}R}(\Type{Real} \Var{x}, \Type{Real} \Var{y}) +\end{tabular} +& $x \geq y$ \\ +\hline +\end{tabular} +\end{center} +\caption{Predicates on reals}\label{pred} +\end{table} + +Boolean values may be combined with the operators presented in Table~\ref{Bool-Ops}: +\newpage + +\begin{table}[htp] +\begin{center} +\begin{tabular}{|l|l|} +\hline +\begin{tabular}{l} +\vdist\Type{Bool} \Name{and{\_}B{\_}B}(\Type{Bool} \Var{x}, Bool \Var{y}) +\end{tabular} +& $x \wedge y$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Bool} \Name{or{\_}B{\_}B}(\Type{Bool} \Var{x}, Bool \Var{y}) +\end{tabular} +& $x \vee y$ \\ +\hline +\begin{tabular}{l} +\vdist\Type{Bool} \Name{not{\_}B}(\Type{Bool} \Var{x}) +\end{tabular} +& $\neg x$ \\ +\hline +\end{tabular} +\end{center} +\caption{Boolean operators}\label{Bool-Ops} +\end{table} + +Finally, the conditional is a function with a variable number of arguments: + +\begin{funlist} +\item \Type{Real} \Name{realIf}(% +\Type{int} \Var{n}, +\Type{Bool} $b_1$, +\Type{Real} $x_1$, +\ldots, +\Type{Bool} $b_n$, +\Type{Real} $x_n$) +\end{funlist} + +This function takes an integer as its first argument, +followed by a variable number of guard/value pairs. +The integer argument should tell the number of these pairs. +The variable argument list is implemented with stdarg(3). + +Roughly spoken, the function evaluates the guards $b_1$, \ldots, $b_n$, +then chooses non-deterministically one of the guards which happened to be true, +and returns the corresponding value. +Before we can provide a more detailed description, +we must say more about the type \Type{Bool} +and the behaviour of the predicates. + +Recall that an element of \Type{Real} is implemented as a digit stream, +whose initial prefixes provide a shrinking sequence of intervals +approximating a real number. +Correspondingly, the elements of type \Type{Bool} are implemented +as sequences of ``truth intervals''. +These sequences usually start out with the interval +\Name{Unknown} = [\Name{False}, \Name{True}], +which may at some later stage be refined to either \Name{False} or \Name{True}.\\[0.5ex] +\textbf{Example:} +Table~\ref{Truth-values} shows how nested sequences of intervals +are mapped to sequences of truth values by the predicate \Name{gtEq{\_}R{\_}0}. + +\begin{table}[htp] +\begin{center} +\begin{tabular}{|c|c||c|c|} +\hline +\vdist$[-3,2]$ & \Name{Unknown} & $[-2,3]$ & \Name{Unknown} \\ +\vdist$[-2,1]$ & \Name{Unknown} & $[-1,2]$ & \Name{Unknown} \\ +\vdist$[-1.5,0.5]$ & \Name{Unknown} & $[-0.5, 1.5]$ & \Name{Unknown} \\ +\vdist$[-1,0]$ & \Name{Unknown} & $[0, 1]$ & \Name{True} \\ +\vdist$[-0.8,-0.2]$ & \Name{False} & $[0.2, 0.8]$ & \Name{True} \\ +\vdist$[-0.7,-0.3]$ & \Name{False} & $[0.3, 0.7]$ & \Name{True} \\ +\vdist$\vdots$ & $\vdots$ & $\vdots$ & $\vdots$ \\ +\hline +\end{tabular} +\end{center} +\caption{Action of the predicate \Name{gtEq{\_}R{\_}0}}\label{Truth-values} +\end{table} + +Thus, the sequence of truth values computed by \Name{gtEq{\_}R{\_}0}(\Var{x}) +will eventually reach \Name{True} if $x > 0$, +and will eventually reach \Name{False} if $x < 0$. +If the exact value of $x$ happens to be 0, +it is possible that the sequence of truth values +remains \Name{Unknown} for ever---% +this happens if all the intervals $[a,b]$ approximating $x$ +have the property $a < 0 < b$. +Yet it is also possible that the sequence switches to \Name{True}---% +this happens if there is an approximating interval $[a,b]$ with $a = 0$. +Which of these two possibilities occur depends on the way +how $x$ was set up, and on implementation details. +But it should be remembered that \Name{gtEq{\_}R{\_}0} +may remain undecided for ever when applied to $0$. + +The Boolean operations produce their output stream by acting +on their input stream(s) element by element, +i.e.\ to produce the $n$th element of the output stream, +the $n$th input element(s) of the input stream(s) are combined +according to Table~\ref{op-action}, +where the truth values have been abbreviated by U, F, and T, +and the operations by logical symbols. + +\begin{table}[htp] +\begin{center} +\begin{tabular}{c|ccc} +$x$ & T & F & U \\ +\hline +$\neg x$ & F & T & U +\end{tabular}\hspace{2em} +\begin{tabular}{c|ccc} +$\land$ & T & F & U \\ +\hline + T & T & F & U \\ + F & F & F & F \\ + U & U & F & U +\end{tabular}\hspace{2em} +\begin{tabular}{c|ccc} +$\lor$ & T & F & U \\ +\hline + T & T & T & T \\ + F & T & F & U \\ + U & T & U & U +\end{tabular} +\end{center} +\caption{Action of the Boolean operators}\label{op-action} +\end{table} + +Now, we can return to the conditional +\begin{funlist} +\item \Type{Real} \Name{realIf}(% +\Type{int} $n$, +\Type{Bool} $b_1$, +\Type{Real} $x_1$, +\ldots, +\Type{Bool} $b_n$, +\Type{Real} $x_n$) +\end{funlist} +This function behaves as follows: +It constructs a cyclic list of guard/value pairs. +Starting with the first pair, \Name{realIf} forces the guard +to compute an element of the resulting Boolean stream. +If the value of this element is \Name{True}, +the real number associated with this guard is returned. +If the value is \Name{False}, the pair is removed from the list. +If the value remains \Name{Unknown}, then \Name{realIf} tries the next pair. +In this way, the function cycles through the list forcing each guard in turn +until a guard becomes \Name{True}. +If the list becomes empty (all the guards are \Name{False}), +then \Name{realIf} issues an error message. +If some guards are remaining \Name{Unknown} for ever, +\Name{realIf} will not terminate. +Some examples will clarify the situation. + +\verb|realIf (2, lt_R_QInt (x, 1, 1), 0, gt_R_0(x), 1)|\\[0.3ex] +means $x < 1 \to 0 \;[\!]\; x > 0 \to 1$. +For $x = \frac12$, the result is unpredictable; +it depends on the actual sequence of intervals +which approximate $\frac12$. +On the other hand, there is no risk of non-termination or error +since at least one guard will eventually yield \Name{True} +for any $x$. + +\verb|realIf (2, ltEq_R_0(x), neg_R(x), gtEq_R_0(x), x)|\\[0.3ex] +means $x \leq 0 \to -x \;[\!]\; x \geq 0 \to x$. +As an implementation of $|x|$, this works well for all $x \neq 0$, +while there is a considerable risk of non-termination for $x = 0$. +(Fortunately, there is the predefined function \Name{abs{\_}R}). + +Suppose you have an implementation \Name{sqrt1} for square root +which works only for arguments in the interval $(\frac14,4)$, +but not for arguments near 0 or very big arguments. +With this knowledge, you can set up the following function: +\[ \begin{array}{ r l @{\;\;\to\;\;} l l } + \sqrt{x} \;=\; (\! & x > \frac14 \land x < 4 & \Name{sqrt1}(x) & \;[\!] \\[0.5ex] + & x \geq 0 \land x < \frac12 & \frac12 \sqrt{4x} & \;[\!] \\[0.5ex] + & x > 2 & 2 \sqrt{x/4} & \;[\!] \\[0.5ex] + & x < 0 & ??? & \;) + \end{array} +\] +Notice how the guards overlap: +if the second guard were $x \geq 0 \land x \leq \frac14$, +then there would be a considerable risk of non-termination +for $x = \frac14$. +By the overlap, this non-termination is prevented---% +without introducing non-determinism +since the values following these guards +are semantically equal in the overlap region. +Similarly, the first and third guard overlap +to prevent non-termination for $x = 4$. +Yet notice that the function does not terminate for $x = 0$ \ldots\\[0.5ex] +As a C program, the above function appears in figure \ref{fig:conditionals}. +Note the use of delays to prevent endless eager recursion. + +\begin{figure}[htp] +\begin{verbatim} + Real sqrt (Real x) { + return realIf (4, + and_B_B (gt_R_QInt (x, 1, 4), lt_R_QInt (x, 4, 1)), + sqrt1 (x), + and_B_B (gtEq_R_0, lt_R_QInt (x, 1, 2)), + div_R_Int ( + realDelay( + (Delay_Fun) sqrt, + (Delay_Arg) mul_R_Int (x, 4)), + 2), + gt_R_QInt (x, 2, 1), + mul_R_Int ( + realDelay( + (Delay_Fun) sqrt, + (Delay_Arg) div_R_Int (x, 4)), + 2), + lt_R_0 (x), + realError ("Square root of negative number") + ); + } +\end{verbatim} +\caption{Example of conditional with delays.}\label{fig:conditionals} +\end{figure} + +As the last example, +suppose you want to iterate a function \Name{f} +until the difference between two consecutive values in the iteration +is smaller than some threshold \Var{eps}. +This can be done by the following recursive function: +\begin{verbatim} + Real iter (Real x) { + Real y = f(x); + Real d = abs_R (sub_R_R (x, y)); /* d = |x - y| */ + return realIf (2, + lt_R_R (d, eps), + y, + gt_R_R (d, eps2), + realDelay((Delay_Fun) iter, (Delay_Arg) y)); + } +\end{verbatim} +where \Var{eps2} is $\Var{eps}/2$. +By using \Var{eps2}, the two guards overlap non-trivially, +and non-termination at \Var{d} = \Var{eps} is prevented +(of course, the iteration still fails to terminate + if \Var{d} never gets small). + +\section{Extracting digits following forcing} + +The functions in this section provide access to the internal representation +of real numbers. +They are not very useful for ordinary users of the library. + +\begin{funlist} +\item \Type{void} \Name{retrieveInfo}(% +\Type{Real} \Var{x}, \Type{Sign} $\ast$\Var{sign}, \Type{int} $\ast$\Var{count}, + \Type{mpz{\_}t} digits) +\end{funlist} +This function retrieves the information that is currently available on \Var{x}. +The sign of \Var{x} is stored in \Var{sign}, +the number of digits calculated so far is stored in \Var{count}, +and a compressed representation of all these digits is deposited in \Var{digits}. +The variable \Var{digits} must be initialised +with the GMP function \Name{mpz{\_}init} prior to calling \Name{retrieveInfo}. +The real argument \Var{x} is unchanged by the call. + +From a compressed digit representation as it is provided by \Name{retrieveInfo}, +the individual digits can be extracted by means of +\begin{funlist} +\item \Type{Digit} \Name{takeDigit}(\Type{int} $\ast$\Var{count}, + \Type{mpz{\_}t} \Var{digits}) +\end{funlist} +This function should only be called if \Var{digits} +contains at least one digit. +It returns the most significant digit contained in \Var{digits}, +removes this digit from \Var{digits}, +and decreases the counter \Var{count} by 1. +Thus, successive calls yield successive digits. + +\noindent An example of the use of these two functions is given in Figure +\ref{fig:digits-info}. + +\begin{figure}[htp] +\begin{verbatim} + Real x; + mpz_t digits; + Sign sign; + Digit digit; + int count; + ... + x = tan_R(y); + force_R_Digs(x, 20); + mpz_init(digits); + retrieveInfo(x, &sign, &count, digits); + printf("%s ", signToString(sign)); + while (count > 0) { + digit = takeDigit(&count, digits); + printf("%s ", digitToString(digit)); + } + printf("\n"); +\end{verbatim} +\caption{Taking digits one-by-one.} +\label{fig:digits-info} +\end{figure} + +Note the two functions \Name{signToString} and \Name{digitToString} +which convert signs and digits to strings for output. + +\section{Environment variables} + +The library uses three environment variables to control its runtime behaviour. +These variables are as follows: + +\begin{description} +\item[\texttt{ICR{\_}STACK{\_}SIZE}=$n$] +\quad This sets the runtime stack to +$n \times k$ words. The default is $n = 20$ for $20k$ words. +It is unlikely that the stack size needs to be adjusted. +If you get a ``stack overflow'' at runtime, it is more likely that the +algorithm for some function is not sufficiently converging for a given +argument. Assuming the default has been set to something other than 1, +try setting the +environment variable \texttt{ICR{\_}DEFAULT{\_}FORCE{\_}COUNT=1} and executing +your program again. +\item[\texttt{ICR{\_}DEFAULT{\_}FORCE{\_}COUNT}=$n$] +\quad Sometimes it +is necessary to force +an arbitrary number of digits from an LFT. This can happen, for example, +when a predicate is forced which in turn must force some number of digits +from its real argument. In theory, one would always want to force as +few digits as possible (i.e.\ 1 digit) +to avoid unnecessary computation. In practice, it +is more efficient to demand more than one digit. The value +of \texttt{ICR{\_}DEFAULT{\_}FORCE{\_}COUNT} +is the number of digits forced in such +circumstances. It is also the number of digits forced from an argument +to a linear fractional transformation when $\epsilon-\delta$ analysis +for the transformation yields a value $\leq 0$. The default is $n = 1$. +The maximum reasonable value is $n = 4$. +\item[\texttt{ICR{\_}FORCE{\_}DEC{\_}UPPER{\_}BOUND}=$n$] +\quad +When extracting information from reals, the library works with +``digits''. Each digit gives a fixed amount of information. Usually, however, +a user wishes to extract enough information to ensure some decimal precision. +The functions \Name{force{\_}R{\_}Dec} and \Name{print{\_}R{\_}Dec} +are provided to +retrieve information from a real to a specified decimal precision. +Unfortunately, there is not always a direct correspondence between a number of +digits and a decimal precision. As a number approaches infinity, more +digits are needed to bound it above. This variable sets a bound +on the number of digits to retrieve from a real to bound it above before +giving up. +The default is $n = 10000$. +\end{description} + +\section{The daVinci interface} + +For debugging and instruction, the library is instrumented to +work with the graph visualisation tool daVinci. +But be warned that much of this visualisation +is only comprehensible to insiders. +When a program has been compiled with daVinci enabled, +a separate daVinci window will be created +when \Name{init\-Reals} is called. +Thereafter, any calls to \Name{force{\_}R{\_}Digs} or \Name{force{\_}R{\_}Dec} +will lead to control being transferred to the daVinci window. + +Once started the daVinci window provides a collection of buttons +to control the execution of a real program. The buttons are as follows: + +\begin{description} +\item[\includegraphics{stop.eps}] Stops execution. +\item[\includegraphics{go.eps}] Enabled when there is work on the +stack. This button starts execution. +\item[\includegraphics{step.eps}] Enabled when there is work on the stack. This +single steps execution. +\item[\includegraphics{continue.eps}] When enabled, it means the stack +is empty. This button returns control to the C program. +\item[\includegraphics{collect.eps}] This button is not implemented. +Ultimately it will be used to invoke the garbage collector. +\end{description} + +In addition, when the program is stopped, the user can click the right +button over any object in the heap. This gives a popup menu +of which only the first entry is implemented. It can be used +to print (in the main program window) the contents of the selected +heap object. This is typically a linear fractional transformation +(nearly all functions in the library are implemented + as compositions of linear fractional transformations). + +\section{Compilation flags} + +There are a number of compilation flags in the Makefile. With the exception +of those listed below, it is unwise to change these flags. + +\begin{description} +\item[\texttt{-DDAVINCI}]\quad When set, the library will connect to the daVinci +graph visualisation tool. In this mode, all objects in the heap and +all information flow is displayed in a separate daVinci window. +Computation is controlled from the daVinci window. The user can run, stop +and single-step the activities of the program, +which mainly consist of emission and absorption of LFTs, +and examine the contents of objects in the heap. +\item[\texttt{-DDEFAULT{\_}FORCE{\_}COUNT}=$n$] +\quad This sets the default force count to use when it is not given by +the environment variable +\texttt{ICR{\_}DEFAULT{\_}FORCE{\_}COUNT}. +\item[\texttt{-DTRACE}=\textit{val}]\quad This enables tracing of force methods. +When set to $0$, tracing is disabled. When set to $1$, tracing is enabled. +Finally, when set to \texttt{traceOn}, tracing can be enabled +and disabled at runtime under software control via the function +\Name{debugTrace}(\Type{int} \Var{b}) where \Var{b} is $1$ to enable +tracing and $0$ to stop tracing. +\item[\texttt{-DSTACK{\_}SIZE=$n$}] +\quad This sets stack size to use when it is not given by +the environment variable +\texttt{ICR{\_}STACK{\_}SIZE}. +\item[\texttt{-DFORCE{\_}DEC{\_}UPPER{\_}BOUND=$n$}] +\quad This is the default value used when the environment variable +\texttt{ICR{\_}FORCE{\_}DEC{\_}UPPER{\_}BOUND} is absent. +\end{description} + +\section{Problems} + +The library is still under development. Future versions of the library +will have specialized versions of the analytic functions +for rational arguments. A document describing the implementation +is also planned. The most serious omission from the present +version of the library is a garbage collector. + +\end{document} diff --git a/ic-reals-6.3/doc/manual/step-eps-converted-to.pdf b/ic-reals-6.3/doc/manual/step-eps-converted-to.pdf Binary files differnew file mode 100644 index 0000000..df2ccb4 --- /dev/null +++ b/ic-reals-6.3/doc/manual/step-eps-converted-to.pdf diff --git a/ic-reals-6.3/doc/manual/step.eps b/ic-reals-6.3/doc/manual/step.eps new file mode 100644 index 0000000..2f9f0ff --- /dev/null +++ b/ic-reals-6.3/doc/manual/step.eps @@ -0,0 +1,68 @@ +%!PS-Adobe-2.0 EPSF-2.0 +%%Title: /home/le/Work/reals/blue/5-c-reals/icons/step.ps +%%Creator: XV Version 3.10a Rev: 12/29/94 (PNG patch 1.2) - by John Bradley +%%BoundingBox: 289 418 301 430 +%%Pages: 1 +%%DocumentFonts: +%%EndComments +%%EndProlog + +%%Page: 1 1 + +% remember original state +/origstate save def + +% build a temporary dictionary +20 dict begin + +% define string to hold a scanline's worth of data +/pix 3 string def + +% define space for color conversions +/grays 18 string def % space for gray scale line +/npixls 0 def +/rgbindx 0 def + +% lower left corner +289 418 translate + +% size of image (on paper, in 1/72inch coords) +11.59200 11.59200 scale + +% dimensions of data +18 18 1 + +% mapping matrix +[18 0 0 -18 0 18] + +{currentfile pix readhexstring pop} +image +ffffff +ffffff +ff3fff +fe3fff +fc3fff +fc3fff +ff3fff +ff3fff +ff3fff +ff3fff +ff3fff +ff3fff +ff3fff +ff3fff +fc0fff +fc0fff +ffffff +ffffff + + +showpage + +% stop using temporary dictionary +end + +% restore original state +origstate restore + +%%Trailer diff --git a/ic-reals-6.3/doc/manual/stop-eps-converted-to.pdf b/ic-reals-6.3/doc/manual/stop-eps-converted-to.pdf Binary files differnew file mode 100644 index 0000000..93b7331 --- /dev/null +++ b/ic-reals-6.3/doc/manual/stop-eps-converted-to.pdf diff --git a/ic-reals-6.3/doc/manual/stop.eps b/ic-reals-6.3/doc/manual/stop.eps new file mode 100644 index 0000000..7419b6c --- /dev/null +++ b/ic-reals-6.3/doc/manual/stop.eps @@ -0,0 +1,68 @@ +%!PS-Adobe-2.0 EPSF-2.0 +%%Title: /home/le/Work/reals/blue/5-c-reals/icons/stop.ps +%%Creator: XV Version 3.10a Rev: 12/29/94 (PNG patch 1.2) - by John Bradley +%%BoundingBox: 289 418 301 430 +%%Pages: 1 +%%DocumentFonts: +%%EndComments +%%EndProlog + +%%Page: 1 1 + +% remember original state +/origstate save def + +% build a temporary dictionary +20 dict begin + +% define string to hold a scanline's worth of data +/pix 3 string def + +% define space for color conversions +/grays 18 string def % space for gray scale line +/npixls 0 def +/rgbindx 0 def + +% lower left corner +289 418 translate + +% size of image (on paper, in 1/72inch coords) +11.59200 11.59200 scale + +% dimensions of data +18 18 1 + +% mapping matrix +[18 0 0 -18 0 18] + +{currentfile pix readhexstring pop} +image +ffffff +ffffff +c000ff +c000ff +c000ff +c000ff +c000ff +c000ff +c000ff +c000ff +c000ff +c000ff +c000ff +c000ff +c000ff +c000ff +ffffff +ffffff + + +showpage + +% stop using temporary dictionary +end + +% restore original state +origstate restore + +%%Trailer |