# Division by zero (newbie first question) **URL:** \ **Category:** Learning\ **Created:** [April 16, 2019, 10:00pm UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669 "2019-04-16T22:00:17Z")\ **Posts on this page:** 16\ **Page:** 1
**Author:** ![vistuleB](https://avatars.discourse-cdn.com/v4/letter/v/b38774/32.png) [@vistuleB](https://discuss.ocaml.org/u/vistuleB)\ **Post date:** [April 16, 2019, 10:00pm UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/1 "2019-04-16T22:00:17Z")
Hi. I just set my hands on Ocaml, expecting a mathematically rigorous language etc. I’m a bit mystified as to why the language designers would allow the following “horror” to occur: ``` # let a = 0.;; val a : float = 0. # let b = -0.;; val b : float = -0. # let f x = 1. /. x;; val f : float -> float = # a = b;; - : bool = true # f a = f b;; - : bool = false ``` So `a = b` does not imply `f a = f b`. Is this something that commonly occurs throughout the language? What is the design rationale to define floating-point division this way? I understand that some chips distinguish 0 from -0 and define division by zero this way, but this doesn’t quite seem a good enough reason to me to remove “substitutability” from the language. Thank you! ---
**Author:** ![bcc32](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/bcc32/32/203_2.png) [@bcc32](https://discuss.ocaml.org/u/bcc32)\ **Post date:** [April 16, 2019, 10:03pm UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/2 "2019-04-16T22:03:09Z")
If you print the results of `f a` and `f b`, you’ll see that you get: ```auto # f a;; - : float = inf # f b;; - : float = -inf ``` OCaml uses [IEEE 754](https://en.wikipedia.org/wiki/IEEE_754) floating-point arithmetic, which defines that those operations must have the results you described. As to the virtues of having or not having a signed zero, whether they should be “equal”, etc., I am not qualified to say. ---
**Author:** ![yawaramin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yawaramin/32/3384_2.png) [@yawaramin](https://discuss.ocaml.org/u/yawaramin)\ **Post date:** [April 17, 2019, 12:41am UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/3 "2019-04-17T00:41:37Z")
When you say ‘mathematically rigorous language’, what do you mean exactly? What defines a mathematically rigorous language, to you? ---
**Author:** ![Freyr666](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/freyr666/32/591_2.png) [@Freyr666](https://discuss.ocaml.org/u/Freyr666)\ **Post date:** [April 17, 2019, 7:14am UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/4 "2019-04-17T07:14:59Z")
It is mathematically rigorous, floats behave as floats, not as real numbers 😉 Flambda people even use SAT for proving the correctness of float optimizations. > **[Proofs (and Refutations) using Z3](https://blog.janestreet.com/proofs-and-refutations-using-z3/)** > > People often think of formal methods and theorem provers as forbiddingtools, cool in theory but with a steep learning curve that makes themhard to use in rea... ---
**Author:** ![vistuleB](https://avatars.discourse-cdn.com/v4/letter/v/b38774/32.png) [@vistuleB](https://discuss.ocaml.org/u/vistuleB)\ **Post date:** [April 17, 2019, 7:34am UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/5 "2019-04-17T07:34:06Z")
When I used the vague term “mathematically rigorous” (sorry about that) I guess what I meant is that I expected there to be some kind mapping (think Curry-Howard correspondence) from an Ocaml program to a subset of first-order logic… and that the correspondence would send “=” to “=”, e.g. (I’m no specialist in Curry-Howard, type theory or first order logic, so I can’t comment more than that. But it seems hard to imagine that a direct correspondence mapping “=” to “=” and mapping Ocaml functions to mathematical functions would exist, given the above behavior.) Anyway, it’s no my intention to start a food fight here, but I was genuinely surprised by this design decision to follow the IEEE754 arithmetic logic at the expense of breaking the ordinary logical meaning of “=” for floating point numbers. In particular, the fact that `a = b` does not imply `f a = f b` seems a huge drawback to me in terms of reasoning about programs. I guess I would be curious to know the following from advanced users: 1. in practice, does one assume that `a = b` implies `f a = f b` (and multi-argument generalizations thereof), or does one not trust `=` this way? (Again: in practice.) And if some OCaml guru / designer is in the room: 1. Is the decision to follow the IEEE754 arithmetic while simultaneously having `0. = -0.` evaluate to `true` currently seen as a design mistake? Or was it “all thought it” and the least of two evils? I am much looking forward to learning OCaml, and again, it’s not my intention to start a food fight. I am just curious to know the perspective of advanced users on this issue. Thank you! @Freyr666: our posts crossed, but I hope this clarifies my concerns. ---
**Author:** ![Freyr666](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/freyr666/32/591_2.png) [@Freyr666](https://discuss.ocaml.org/u/Freyr666)\ **Post date:** [April 17, 2019, 7:42am UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/6 "2019-04-17T07:42:20Z")
``` # Float.equal (-0.0) 0.0 - : true ``` Structural comparison sucks, QED. Hope one day we would have Modular Implicits, but till then don’t use polymorphic compare and equality, it’s broken beyond repair and not what you want in 99% of cases. Many `standard libraries` like Base/Core and Containers shadow it when you do `open Base`. Edit: Ups, sorry it seems structural comparison works properly here: ``` # (-0.0) = 0.0 - : true ``` And `-inf` is not equal to `inf`, so everything is mathematically rigorous, it seems 😉 ---
**Author:** ![Chris00](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/chris00/32/48_2.png) [@Chris00](https://discuss.ocaml.org/u/Chris00)\ **Post date:** [April 17, 2019, 8:12am UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/7 "2019-04-17T08:12:06Z")
> [@vistuleB](#): > > follow the IEEE754 arithmetic while simultaneously having `0. = -0.` evaluate to `true` For an example of the interest of (handling correctly) -0, you can see “Borda’s Mouthpiece” on p. 12 of “[How Java’s Floating-Point Hurts Everyone Everywhere](https://people.eecs.berkeley.edu/~wkahan/JAVAhurt.pdf)”. ---
**Author:** ![threepwood](https://avatars.discourse-cdn.com/v4/letter/t/8dc957/32.png) [@threepwood](https://discuss.ocaml.org/u/threepwood)\ **Post date:** [April 17, 2019, 11:55am UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/8 "2019-04-17T11:55:29Z")
Basically OCaml tries to respect what processors do and what systems programmers expect. This includes having its floats behave according to standard even though at first look to a mathematician the behaviour is wonky (but actually when you consider the constraints it makes sense). Another similar thing is how the `mod` operator denotes the modulo operation that `%` denotes in C and that processors do, which does not behave like mathematicians would expect in the presence of negative arguments (this one is just a design mistake on the part of early computer engineers imo, because the actual behaviour is less useful than the mathematically proper one). ---
**Author:** ![bcc32](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/bcc32/32/203_2.png) [@bcc32](https://discuss.ocaml.org/u/bcc32)\ **Post date:** [April 17, 2019, 2:54pm UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/9 "2019-04-17T14:54:00Z")
> [@vistuleB](#): > > the decision to follow the IEEE754 arithmetic while simultaneously having `0. = -0.` evaluate to `true` Erm, to clarify, I think IEEE754 says `0. = -0.` must evaluate to true. ---
**Author:** ![ohko](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ohko/32/1585_2.png) [@ohko](https://discuss.ocaml.org/u/ohko)\ **Post date:** [April 17, 2019, 3:21pm UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/10 "2019-04-17T15:21:21Z")
How does one end up with a `-0.` in the first place? Would it ever be the result of a computation? ---
**Author:** ![bcc32](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/bcc32/32/203_2.png) [@bcc32](https://discuss.ocaml.org/u/bcc32)\ **Post date:** [April 17, 2019, 3:25pm UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/11 "2019-04-17T15:25:48Z")
Yeah, if you do something like `-1e-200 /. 1e200`, you’ll get `-0.` It’s also possible in some other ways, but I think it’s usually a result of rounding a very small negative number to zero. (See also [wikipedia](https://en.wikipedia.org/wiki/Signed_zero)). ---
**Author:** ![Armael](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/armael/32/1223_2.png) [@Armael](https://discuss.ocaml.org/u/Armael)\ **Post date:** [April 17, 2019, 4:11pm UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/12 "2019-04-17T16:11:03Z")
> In particular, the fact that `a = b` does not imply `f a = f b` seems a huge drawback to me in terms of reasoning about programs. Also, note that this kind of equational reasoning does not hold in presence of side effects (which exist in OCaml). ```auto # let f = let counter = ref 0 in fun () -> incr counter; !counter;; val f : unit -> int = # f ();; - : int = 1 # f ();; - : int = 2 # f () (* 3 *) = f () (* 4 *);; - : bool = false ``` ---
**Author:** ![mseri](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/mseri/32/91_2.png) [@mseri](https://discuss.ocaml.org/u/mseri)\ **Post date:** [April 17, 2019, 9:08pm UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/13 "2019-04-17T21:08:47Z")
If you think about the definition in terms of limits, what is defined in the float standard is the behaviour that makes most sense imo: ```auto lim_{x -> 0-} x = 0 # here 0- means approaching zero "from the left" lim_{x -> 0+} x = 0 # here 0+ means approaching zero "from the right" lim_{x -> 0-} x = lim_{x -> 0+} x = lim_{x -> 0} x = 0 ``` However ```auto lim_{x -> 0-} 1/x = -inf lim_{x -> 0+} 1/x = inf ``` and in fact ```auto lim_{x -> 0} 1/x does not exist ``` I think here the float standard is more coherent and correct than assuming `1/x = inf`. Having `a=b` imply `f a = f b` makes sense only if `f` is actually well defined at `a` (or `b`), but division by zero is not defined at `0`. ---
**Author:** ![yallop](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yallop/32/517_2.png) [@yallop](https://discuss.ocaml.org/u/yallop)\ **Post date:** [April 18, 2019, 8:04am UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/14 "2019-04-18T08:04:24Z")
> [@vistuleB](#): > > in practice, does one assume that `a = b` implies `f a = f b` (and multi-argument generalizations thereof), or does one not trust `=` this way? (Again: in practice.) It’s sometimes possible to reason informally in that way, when you know something about `f`, `a`, and `b`. But the property doesn’t hold in general. Here’s another example where it doesn’t hold: ```auto # let a, b = ref (), ref ();; val a : unit ref = {contents = ()} val b : unit ref = {contents = ()} # let f x = x == a;; val f : unit ref -> bool = # a = b;; - : bool = true # f a = f b;; - : bool = false ``` ---
**Author:** ![TheAspiringHacker](https://avatars.discourse-cdn.com/v4/letter/t/a9a28c/32.png) [@TheAspiringHacker](https://discuss.ocaml.org/u/TheAspiringHacker)\ **Post date:** [April 26, 2019, 3:10am UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/15 "2019-04-26T03:10:57Z")
> [@vistuleB](#): > > When I used the vague term “mathematically rigorous” (sorry about that) I guess what I meant is that I expected there to be some kind mapping (think Curry-Howard correspondence) from an Ocaml program to a subset of first-order logic… and that the correspondence would send “=” to “=”, e.g. (I’m no specialist in Curry-Howard, type theory or first order logic, so I can’t comment more than that. But it seems hard to imagine that a direct correspondence mapping “=” to “=” and mapping Ocaml functions to mathematical functions would exist, given the above behavior.) Because OCaml has nontermination, it is an inconsistent logic. In fact, with nontermination, you can prove anything. If you want to experiment with the Curry-Howard correspondence, I would recommend something like [Coq](https://coq.inria.fr/) (written in OCaml!) or [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php). Remember that in the Curry-Howard correspondence, propositions are _types_. The `(=)` operator is not a type constructor, and it is not what propositional equality maps to. [Martin-Lof Type Theory](https://en.wikipedia.org/wiki/Intuitionistic_type_theory) defines an “equality” type denoted `Id A x y` that represents propositional equality between `x` and `y`, terms of type `A`. In OCaml, something similar to it could be implemented as: ```auto type ('x, 'y) id = | Refl : ('x, 'x) id ``` but because OCaml is not dependently typed, you can only compare types for equality, not terms. Fun fact: Homotopy Type Theory, an ongoing subject of research, gives new meaning to propositional equality! Both Coq and Agda have HoTT libraries. ---
**Author:** ![LdBeth](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ldbeth/32/2680_2.png) [@LdBeth](https://discuss.ocaml.org/u/LdBeth)\ **Post date:** [February 22, 2021, 2:59pm UTC](https://discuss.ocaml.org/t/division-by-zero-newbie-first-question/3669/16 "2021-02-22T14:59:04Z")
Maybe I’m too late to the party, but someday I just happened to across an OCaml library implements constructive real numbers that can make someone expecting a rigorous programming language happy. [Jean-Christophe Filliâtre : Creal (lri.fr)](https://www.lri.fr/~filliatr/creal.en.html) There’re other useful or not so useful OCaml small scale libraries under the same homepage, some of them are mentioned elsewhere in this forum.