diff options
Diffstat (limited to 'ic-reals-6.3/doc/manual')
| -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 |
14 files changed, 1751 insertions, 0 deletions
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 |