> So I think the key is to make sure that “undefined” thing really undefined, such that whenever it appears, the proof cannot proceed any more
I think this is exactly what is impossible to do in HOL: it is a logic of total functions. On Wed, 20 Feb 2019 at 15:26, Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > Well, as the purpose of optionTheory is to augment any type with one more > value, for (at least) extreals, it would be equivalent to have that > “undefined” thing defined as part of the datatype definition: > > val extreal_def = Datatype > `extreal = NegInf | PosInf | Normal real | Undefined`; > > However, once “Undefined” is actually defined, it’s then a disaster to > affect almost all arithmetic laws. For a number which is either PosInf nor > NegInf, now we can’t say it must be a (Normal x) any more, and many > theorems will be broken. To fix it, we have to treat this “Undefined” as > something like those NaNs in IEEE 754 standard and define their orders and > arithmetic laws, then all these work are unnecessary for formalization of > pure math theorems. > > So I think the key is to make sure that “undefined” thing really > undefined, such that whenever it appears, the proof cannot proceed any > more, except for syntactic rewriting, which is inevitable in HOL. Keeping > ``0 / 0 = 0`` as before, could be another option, but I have concerns to > convince mathematicians to accept this fact since I aim at precisely > reproduce those pure math proofs under the “same” formal system with math > books (except for the subtle differences between ZFC and HOL not affecting > the math theories that I’m working with.) > > —Chun > > Il giorno 20 feb 2019, alle ore 13:16, Ramana Kumar < > ramana.ku...@cl.cam.ac.uk> ha scritto: > > I'd say one of the stronger ways to get "undefined" is to add an element > to your type representing undefinedness, e.g., make it (/) : real option -> > real option -> real option, where NONE represents "undefined". But then you > will have a lot of bookkeeping to deal with... > I don't suggest this seriously in the case of division -- I would rather > suggest accepting the usual treatment of these partial functions as a small > price for the benefits of working in a logic of (only) total functions. > > On Wed, 20 Feb 2019 at 12:00, Lawrence Paulson <l...@cam.ac.uk> wrote: > >> None of these attempts make any sense. In HOL and similar systems >> (including Isabelle/HOL), it’s *impossible* to arrange for x/0 to be >> undefined in any strong sense. Fortunately, it’s consistent and harmless to >> put x/0 = 0. >> >> Larry Paulson >> >> >> > On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourceforge.net wrote: >> > >> > I run some experiments so to check if it is violating any fundamental >> rule. >> > So far it went good. >> >> >> >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
