-
Notifications
You must be signed in to change notification settings - Fork 0
/
interval2.mli
232 lines (163 loc) · 7.24 KB
/
interval2.mli
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
(* ========================================================================== *)
(* A simple OCaml interval library *)
(* https://github.com/monadius/ocaml_simple_interval *)
(* *)
(* Author: Alexey Solovyev *)
(* https://github.com/monadius *)
(* *)
(* This file is distributed under the terms of the MIT license *)
(* ========================================================================== *)
(** A simple OCaml interval library.
This interval library needs the OCaml [Num] module.
It is assumed that all floating-point operations are IEEE 754
compatible and the rounding mode is to nearest.
It is also assumed that OCaml functions [exp], [log], [atan] compute results with
less than 1 ulp error.
Intervals computed with this library are optimal floating-point
intervals for basic arithmetic operations.
{!Interval1} provides faster interval functions which are only
slightly less optimal.
*)
(** The interval type *)
type interval = {
low : float;
high : float;
}
(** The empty interval *)
val empty_interval : interval
(** The entire interval representing (-infinity, infinity) *)
val entire_interval : interval
(** [[0., 0.]] *)
val zero_interval : interval
(** [[1., 1.]] *)
val one_interval : interval
(** {6 Interval operations} *)
(** Creates an interval from given endpoints *)
val make_interval : float -> float -> interval
(** Tests if an interval is empty *)
val is_empty : interval -> bool
(** Tests if an interval is the entire interval *)
val is_entire : interval -> bool
(** Tests if an interval is valid. A valid interval is either empty
or [[a, b]] with [a <= b], [a < infinity], [-infinity < b]. *)
val is_valid : interval -> bool
(** Computes a midpoint of an interval. This function returns finite
values for all valid non-empty intervals. *)
val mid_i : interval -> float
(** Interval negation {b (optimal)} *)
val neg_i : interval -> interval
(** Interval absolute value {b (optimal)} *)
val abs_i : interval -> interval
(** Interval maximum {b (optimal)} *)
val max_ii : interval -> interval -> interval
(** Interval minimum {b (optimal)} *)
val min_ii : interval -> interval -> interval
(** Interval addition {b (optimal)} *)
val add_ii : interval -> interval -> interval
(** Addition of an interval and a number {b (optimal)} *)
val add_id : interval -> float -> interval
(** Addition of a number and an interval {b (optimal)} *)
val add_di : float -> interval -> interval
(** Interval subtraction {b (optimal)} *)
val sub_ii : interval -> interval -> interval
(** Subtraction of an interval and a number {b (optimal)} *)
val sub_id : interval -> float -> interval
(** Subtraction of a number and an interval {b (optimal)} *)
val sub_di : float -> interval -> interval
(** Interval multiplication {b (optimal)} *)
val mul_ii : interval -> interval -> interval
(** Multiplication of an interval and a number {b (optimal)} *)
val mul_id : interval -> float -> interval
(** Multiplication of a number and an interval {b (optimal)} *)
val mul_di : float -> interval -> interval
(** Interval division {b (optimal)} *)
val div_ii : interval -> interval -> interval
(** Division of an interval by a number {b (optimal)} *)
val div_id : interval -> float -> interval
(** Division of a number by an interval {b (optimal)} *)
val div_di : float -> interval -> interval
(** Interval reciprocal {b (optimal)} *)
val inv_i : interval -> interval
(** Interval square root {b (optimal)} *)
val sqrt_i : interval -> interval
(** Interval square {b (optimal)} *)
val sqr_i : interval -> interval
(** Interval integer power. This function returns an optimal interval
but this behavior may change in the future. *)
val pown_i : interval -> int -> interval
(** Interval exponential function. It is assumed that the standard
function [exp:float->float] has less than 1 ulp error. *)
val exp_i : interval -> interval
(** Interval natural logarithm. It is assumed that the standard
function [log:float->float] has less than 1 ulp error. *)
val log_i : interval -> interval
(** Interval arctangent. It is assumed that the standard
function [atan:float->float] has less than 1 ulp error. *)
val atan_i : interval -> interval
(** Interval sine (not implemented yet) *)
val sin_i : interval -> interval
(** Interval cosine (not implemented yet) *)
val cos_i : interval -> interval
(** {6 Floating-point operations with directed rounding} *)
(** Computes a successor of a floating-point number {b (optimal)} *)
val fsucc : float -> float
(** Computes a predecessor of a floating-point number {b (optimal)} *)
val fpred : float -> float
(** Returns a lower bound of the sum of two floating-point numbers {b
(optimal)} *)
val fadd_low : float -> float -> float
(** Returns an upper bound of the sum of two floating-point numbers {b
(optimal)} *)
val fadd_high : float -> float -> float
(** Returns a lower bound of the difference of two floating-point
numbers {b (optimal)} *)
val fsub_low : float -> float -> float
(** Returns an upper bound of the difference of two floating-point
numbers {b (optimal)} *)
val fsub_high : float -> float -> float
(** Returns a lower bound of the product of two floating-point numbers
{b (optimal)} *)
val fmul_low : float -> float -> float
(** Returns an upper bound of the product of two floating-point
numbers {b (optimal)} *)
val fmul_high : float -> float -> float
(** Returns a lower bound of the ratio of two floating-point numbers
{b (optimal)} *)
val fdiv_low : float -> float -> float
(** Returns an upper bound of the ratio of two floating-point numbers
{b (optimal)} *)
val fdiv_high : float -> float -> float
(** Returns a lower bound of [x^2] {b (optimal)} *)
val fsqr_low : float -> float
(** Returns an upper bound of [x^2] {b (optimal)} *)
val fsqr_high : float -> float
(** Returns a lower bound of [sqrt x] {b (optimal)} *)
val fsqrt_low : float -> float
(** Returns an upper bound of [sqrt x] {b (optimal)} *)
val fsqrt_high : float -> float
(** Returns a lower bound of [exp x] *)
val fexp_low : float -> float
(** Returns an upper bound of [exp x] *)
val fexp_high : float -> float
(** Returns a lower bound of [log x] *)
val flog_low : float -> float
(** Returns an upper bound of [log x] *)
val flog_high : float -> float
(** Returns a lower bound of [atan x] *)
val fatan_low : float -> float
(** Returns an upper bound of [atan x] *)
val fatan_high : float -> float
(*
(** Return a lower bound of [cos x] *)
val fcos_low : float -> float
(** Returns an upper bound of [cos x] *)
val fcos_high : float -> float
(** Returns a lower bound of [sin x] *)
val fsin_low : float -> float
(** Returns an upper bound of [sin x] *)
val fsin_high : float -> float
*)
(** Returns a lower bound of [x^n] *)
val fpown_low : float -> int -> float
(** Returns an upper bound of [x^n] *)
val fpown_high : float -> int -> float