Email Gateway (Aug 17 2022 at 14:47): Email Gateway (Aug 17 2022 at 14:47):From: Francisco Jose Chaves Alonso <francisco.jose.chaves.alonso@ens-lyon.fr>
Hello
I want to implement the interval arithmetic for use in the proof of expressions
like:
x \<in> [0,1] ==> x * (1 x) \<in> [0,1]
The interval [a,b] is the set of real numbers { x | a <= x <= b}.
Based on the work of Daumas et al. on PVS,
http://research.nianet.org/~munoz/Papers/arith-17.pdf,
the idea is to show that x(1 x) is in the interval X(1 X) where X is the
interval [0,1], and then show that X*(1 X) \<subseteq> [0,1]. The operations
on intervals are defined such that
X@Y = { x@y | x \<in> X /\ y \<in> Y }, @ \<in> {+,-,*,/}
To model the intervals I have at least the following possibilities:
datatype interval = Interval real * real
record interval =
lb:: real
ub:: real
types interval:: real * real
which could be a good choice for Isabelle? Other possibilities or suggestions?
Thanks
Francisco
-- Francisco José Cháves (ENS-LIP)
mailto: Francisco.Jose.Chaves.Alonso@ens-lyon.fr
http://perso.ens-lyon.fr/francisco.jose.chaves.alonso
ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE
Phone: (+33) 4 72 72 84 36
Email Gateway (Aug 17 2022 at 14:47):From: Amine Chaieb <chaieb@informatik.tu-muenchen.de>
Hi,
In the paper, there is no need for infinite bounds, so i guess all the
alternatives are ok. If you want to include infinite bounds, you
definitely need more, e.g. types interval = (real option) * (real option).
It also depends on what you want to prove for the intervals. If you want
to prove e.g. that the intervals form a semi-lattice, then maybe the types
approach is more suitable.
I have no experience with records, may be an other one could comment on
it.
Hope it helps.
Amine.
Email Gateway (Aug 17 2022 at 14:47):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Francisco Jose Chaves Alonso wrote:
Francisco,
I did some work on intervals of real numbers some years ago.
The work was based on some existing literature, and involved sets of
intervals (more complicated than single intervals!) which could be
either open or closed at either endpoint.
It was written up in
Jeremy E. Dawson & Rajeev Goré, Machine-checking the Timed Interval
Calculus, 15th Australian Joint Conference on Artificial Intelligence
(AI'02), LNCS 2557, 95-106,
see http://users.rsise.anu.edu.au/~jeremy/pubs/tic/
Software files in Isabelle are at
http://users.rsise.anu.edu.au/~jeremy/isabelle/tic/
Jeremy
Email Gateway (Aug 17 2022 at 14:49):From: Steve Stevenson <steve@cs.clemson.edu>
Your best bet is to contact the folks doing interval arithmetic
research: reliable_computing@interval.louisiana.edu and
interval@listserv.utep.edu.
To the point, there has been recent discussions on the mis-
representation of intervals by Mathematica. The problems become very
complex, really quickly, if you're doing symbolic mathematics on
intervals.
Last updated: May 03 2024 at 04:19 UTC