This is one of the most common questions about HOL.
HOL is a logic of total functions. There are some expressions, like division by
zero and the head of an empty list, which we often intuitively think of as
special exceptional values. But HOL's type system doesn't have special
exceptional values, so ``HD []`` and ``0 \ 0`` have to be values of the correct
type.
We could choose to define HD and the division operator so that it was not
possible to prove what these unusual values are. But that doesn't mean quite
the same thing as an exception. For instance, however HD and division were
defined, we can still prove equalities about them:
``HD [] + (0 / 0) - HD [] - (0 / 0) = 0``.
Since we have to have normal values, it's often convenient to pick sensible
defaults, since they make some theorems true without side conditions. For
instance, we pick that "0 - 1 = 0" in numerals, and "TL [] = []", which happens
to make "LENGTH (TL xs) = (LENGTH xs - 1)" unconditionally true. Curiously, in
HOL4, the author of the LENGTH_TL theorem didn't seem to realise that.
If this bothers you a lot, you can consider the HOL ``x \ y`` expression to map
to the expression "if x = 0 then 0 else (x \ y)" in whatever your intuitive
logic is.
Cheers,
Thomas.
Cheers,
Thomas.
________________________________
From: Chun Tian (binghe) <binghe.l...@gmail.com>
Sent: Thursday, February 14, 2019 5:40:36 PM
To: HOL
Subject: [Hol-info] 0 / 0 = 0 ???
Hi,
in HOL's realTheory, division is defined by multiplication:
[real_div] Definition
⊢ ∀x y. x / y = x * y⁻¹
and zero multiplies any other real number equals to zero, which is
definitely true:
[REAL_MUL_LZERO] Theorem
⊢ ∀x. 0 * x = 0
However, above two theorems together gives ``0 / 0 = 0``, as shown below:
> REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
val it = ⊢ 0 / 0 = 0: thm
How do I understand this result? Is there anything "wrong"?
(The same problems happens also in extrealTheory, since the definition
of `*` finally reduces to `*` of real numbers)
Regards,
Chun Tian
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
