Is HD [] at all possible to define? For some fixed list type yes but in general for [] : 'a list ?
- Gergely Az Android Outlook letöltése On Fri, Feb 15, 2019 at 12:00 AM +0100, <michael.norr...@data61.csiro.au> wrote: The author of LENGTH_TL probably didn’t have access to the updated definition of TL. Once upon a time, the philosophy was to keep more things unspecified so that one could not know which list TL [] denoted. I assume, not having looked into the relevant history, that LENGTH_TL dates back to that earlier period. In that vein, natural number division does not define what x DIV 0 might happen to be at all. Pleasantly, the feature of starting out with things unspecified is that it is sound to later specify exactly what the border cases might be. TAKE, DROP and ZIP have also picked up defined values for what were unspecified cases relatively recently. (These functions all map into ranges where halfway reasonable defaults seem to exist. It’s harder to imagine what HD [] should be. ) Michael From: Thomas Sewell <sew...@chalmers.se> Date: Friday, 15 February 2019 at 04:15 To: "Chun Tian (binghe)" <binghe.l...@gmail.com>, hol-info <hol-info@lists.sourceforge.net> Subject: Re: [Hol-info] 0 / 0 = 0 ??? 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
