cs0701141/all.tex
1: \documentclass[times, 10pt,twocolumn]{article} 
2: \usepackage{latex8}
3: \usepackage{graphicx}
4: \usepackage{latexsym}
5: 
6: \title{The Fundamental Theorems of Interval Analysis
7: }
8: 
9: \author{M.H. van Emden and B. Moa \\
10:            Department of Computer Science\\
11:            University of Victoria, Canada
12:           }
13: 
14: \begin{document}
15: \vspace{-15mm}
16: \maketitle
17: \pagestyle{empty}
18: \vspace{-5mm}
19: \begin{abstract}
20: Expressions are not functions.
21: Confusing the two concepts or failing to define
22: the function that is computed by an expression
23: weakens the rigour of interval arithmetic.
24: We give such a definition and continue
25: with the required re-statements
26: and proofs of the fundamental theorems of interval arithmetic
27: and interval analysis.
28: \end{abstract}
29: 
30: \vspace{-5mm}
31: \input{defs}
32: 
33: \input{01.intro}
34: \input{02.mathPrelim}
35: \input{03.intvSet}
36: \input{04.composition}
37: \input{05.contIntrvExt}
38: 
39: \vspace{-2mm}
40: \section{Conclusions}
41: \vspace{-2mm}
42: 
43: %It is fundamental to interval methods to evaluate an expression
44: %in terms of interval arithmetic and to compare the result with
45: %the real-valued function that is computed by the expression.
46: %It is therefore important to be clear about the relation between
47: %very different entities:
48: %expressions, which are syntactic objects, and
49: %the functions in $\R^n \rightarrow \R$ that they compute.
50: %We have clarified this relationship.
51: 
52: The fact that the result
53: of an expression evaluation in intervals gives a result
54: that contains the range of values of the function
55: computed by the expression
56: cannot be a mathematical theorem
57: without a mathematical definition
58: of what it means for a function to be computed by an expression.
59: In this paper we give such a definition
60: and prove the theorem on the basis of it.
61: 
62: Another fundamental assumption
63: in the use of intervals is that,
64: as we make the intervals
65: in an interval evaluation of an expression narrower,
66: the interval result gets closer
67: to the range of values of the function
68: computed by the expression.
69: We use our definition to prove a theorem to this effect.
70: 
71: Our starting point in all this is that intervals are sets
72: and that, therefore,
73: interval extensions of functions are set extensions of functions.
74: The latter concept is an old one in set theory
75: and is more widely applicable.
76: Our definition and two main theorems are stated in terms of sets,
77: so apply to intervals as special cases.
78: 
79: This is of course only of interest to those who believe in sets
80: as foundation of mathematics. A radically different approach to the
81: fundamental theorems of interval analysis is found in Paul Taylor's
82: work (see for example \cite{TaylorP:intawi}).
83: Here the starting point is topology, axiomatically founded rather
84: than set-theoretically.
85: 
86: If it seems that our proposed foundations
87: for interval methods are overly complex
88: in comparison with the way they are given in the literature,
89: we are comforted by Einstein's dictum:
90: \emph{Make things as simple as possible, but not simpler.}
91: 
92: \vspace{-2mm}
93: \section{Acknowledgements}
94: \vspace{-5mm}
95: This research was supported by the University of Victoria and by
96: the Natural Science and Engineering Research Council of Canada.
97: We owe a great debt of gratitude to our anonymous reviewer whose
98: extremely detailed and helpful report has helped us to improve
99: this paper.
100: \vspace{-2mm}
101: %\bibliographystyle{latex8}
102: %\bibliography{article,book,collection,proceedings,techreport,thesis,unpublished}
103: 
104: \begin{thebibliography}{10}\setlength{\itemsep}{-1ex}\small
105: 
106: \bibitem{brbk39}
107: N.~Bourbaki.
108: \newblock {\em Th\'eorie des Ensembles (Fascicule de R\'esultats)}.
109: \newblock Hermann et Cie, 1939.
110: 
111: \bibitem{chjo91}
112: S.~H. Cheng and C.~B. Jones.
113: \newblock On the usability of logics which handle partial functions.
114: \newblock In {\em Proc. of the 3rd. Refinement Workshop}, pages 51--69, 1991.
115: 
116: \bibitem{hlm60}
117: P.~R. Halmos.
118: \newblock {\em Naive Set Theory}.
119: \newblock D. Van Nostrand, 1960.
120: 
121: \bibitem{hnsn92}
122: E.~Hansen.
123: \newblock {\em Global Optimization Using Interval Analysis}.
124: \newblock Marcel Dekker, 1992.
125: 
126: \bibitem{hckvnmdn01}
127: T.~Hickey, Q.~Ju, and M.~van Emden.
128: \newblock Interval arithmetic: from principles to implementation.
129: \newblock {\em Journal of the ACM}, 48(5):1038 -- 1068.
130: \newblock 2001.
131: 
132: \bibitem{jln01}
133: L.~Jaulin, M.~Kieffer, O.~Didrit, and E.~Walter.
134: \newblock {\em Applied Interval Analysis}.
135: \newblock Springer-Verlag, 2001.
136: 
137: \bibitem{kll55}
138: J.~L. Kelley.
139: \newblock {\em Topology}.
140: \newblock D. Van Nostrand, 1955.
141: 
142: \bibitem{moore66}
143: R.~E. Moore.
144: \newblock {\em Interval Analysis}.
145: \newblock Prentice-Hall, 1966.
146: 
147: \bibitem{nmr90}
148: A.~Neumaier.
149: \newblock {\em Interval Methods for Systems of Equations}.
150: \newblock Cambridge University Press, 1990.
151: 
152: \bibitem{prns93}
153: D.~L. Parnas.
154: \newblock Predicate logic for software engineering.
155: \newblock {\em IEEE Trans. Softw. Eng.}, 19(9):856--862, 1993.
156: 
157: \bibitem{rtrkn84}
158: H.~Ratschek and J.~Rokne.
159: \newblock {\em Computer Methods for the Range of Functions}.
160: \newblock Ellis Horwood/John Wiley, 1984.
161: 
162: \bibitem{rtrkn88}
163: H.~Ratschek and J.~Rokne.
164: \newblock {\em New Computer Methods for Global Optimization}.
165: \newblock Ellis Horwood/John Wiley, 1988.
166: 
167: \bibitem{TaylorP:intawi}
168: P.~Taylor.
169: \newblock Interval analysis without intervals (extended abstract).
170: \newblock In G.~Hanrot and P.~Zimmermann, editors, {\em Real Numbers and
171:   Computers 7}, pages 41--45, 2006.
172: \newblock Nancy.
173: 
174: \end{thebibliography}
175: 
176: \end{document} 
177: