Hend Dawood

InCLosure (Interval enCLosure) is a Language and Environment for Reliable Scientific Computing. Interval computations are radically different from traditional numerical approximation methods and reliable computing under uncertainty is a key focus for modern research in mathematics, computer science, physics, and engineering. InCLosure is a system for carrying out reliable and self-validated computations in arbitrary precision. From its name, InCLosure (abbreviated as "InCL") focuses on "computing guaranteed interval enclosures", that is, "enclosing the exact real result in an interval".
InCLosure is powerful enough to carry out computations ranging from simple real and interval arithmetic, through symbolic and numeric differentiation to an arbitrary order, real automatic differentiation, and interval automatic differentiation, up to and including interval enclosures of integrals and Taylor model computations. No matter how complicated the problem under consideration is, InCLosure provides arbitrary precisions and reliable interval results that can be as narrow as possible by the computational power of the hosting machine.
InCLosure supports arbitrary precision in both real and interval computations. In real arithmetic, the precision is arbitrary in the sense that it is governed only by the computational power of the machine (default is 20 significant digits). The user can change the default precision according to the requirements of the application under consideration. Since interval arithmetic is defined in terms of real arithmetic, interval computations inherit the arbitrary precision of real arithmetic with an added property that the interval subdivision method is provided with an arbitrary number of subdivisions which is also governed only by the computational power of the machine. The user can get tighter and tighter guaranteed interval enclosures by setting the desired number of subdivisions to cope with the problem at hand.
All the computations defined in terms of real and interval arithmetic (e.g., real and interval automatic differentiation, Taylor model computations, and so forth) inherit the same arbitrary precision.
InCLosure is designed to support both interactive and batch modes. In the InCLosure interactive interface, the user can input an InCL command and see its result before moving on to the next command. InCLosure can also be used in batch mode in which case sequences of InCL commands can be given to InCLosure via InCL input files with the results saved in simple and intuitively formatted output files.
InCLosure is coded entirely in Lisp, arguably the fastest and most powerful language for scientific computations. InCLosure provides a friendly and easy-to-use user interface, a simple and intuitive language, a detailed documentation, and clear and fast results. Anyone can compute with InCLosure.

Differentiation arithmetic is a principal and accurate technique for the computational evaluation of derivatives of first and higher order. This article aims at recasting real differentiation arithmetic in a formalized theory of dyadic real differentiation numbers that provides a foundation for first and higher order automatic derivatives. After we set the stage by putting on a systematic basis certain fundamental notions of the algebra of differentiation numbers, we begin by setting up an axiomatic theory of real differentiation arithmetic, as a many-sorted extension of the theory of a continuously ordered field, and then establish the proofs for its consistency and categoricity. Next, we carefully construct the algebraic system of real differentiation arithmetic, deduce its fundamental properties, and prove that it constitutes a commutative unital ring. Furthermore, we describe briefly the extensionality of the system to an interval differentiation arithmetic and to an algebraically closed commutative ring of complex differentiation arithmetic. Finally, a word is said on machine realization of real differentiation arithmetic and its correctness, with an addendum on how to compute automatic derivatives of first and higher order.

Keywords: Automatic differentiation; Categorical differentiation arithmetic; Consistent differentiation arithmetic; Commutative unital ring; Interval differentiation arithmetic; Algebraically closed commutative rings.

Progress in scientific knowledge discloses an increasingly paramount use of quantifiable properties in the description of states and processes of the real-world physical systems. Through our encounters with the physical world, it reveals itself to us as systems of uncertain quantifiable properties. One approach proved to be most fundamental and reliable in coping with quantifiable uncertainties is interval mathematics. A main drawback of interval mathematics, though, is the persisting problem known as the "interval dependency problem". This, naturally, confronts us with the question: Formally, what is interval dependency? Is it a meta-concept or an object-ingredient of interval and fuzzy computations? In other words, what is the fundamental defining properties that characterize the notion of interval dependency as a formal mathematical object? Since the early works on interval mathematics by John Charles Burkill and Rosalind Cecily Young in the dawning of the twentieth century, this question has never been touched upon and remained a question still today unanswered. Although the notion of interval dependency is widely used in the interval and fuzzy literature, it is only illustrated by example, without explicit formalization, and no attempt has been made to put on a systematic basis its meaning, that is, to indicate formally the criteria by which it is to be characterized. Here, we attempt to answer this long-standing question. This article, therefore, is devoted to presenting a complete systematic formalization of the notion of interval dependency, by means of the notions of Skolemization and quantification dependence. A novelty of this formalization is the expression of interval dependency as a logical predicate (or relation) and thereby gaining the advantage of deducing its fundamental properties in a merely logical manner. Moreover, on the strength of the generality of the logical apparatus we adopt, the results of this article are not only about classical intervals, but they are meant to apply also to any possible theory of interval arithmetic. That being so, our concern is to shed new light on some fundamental problems of interval mathematics and to take one small step towards paving the way for developing alternate dependency-aware interval theories and computational methods.

Keywords: Interval mathematics; Interval dependency; Functional dependence; Skolemization; Guaranteed bounds; Interval enclosures; Interval functions; Quantifiable uncertainty; Scientific knowledge; Reliability; Fuzzy mathematics; InCLosure.