Hi Mike, >Taking definedness to the level Freek is discussing would, >I think, not let you prove that > > x DIV 0 = x DIV 0
Exactly. I think that what I want is much closer to PVS and B than to IMPS. I also don't want any change to the logic. I _hate_ partial logics. I want to be able to use all the tools that are available for the (standard) total logics! As I say, I _hate_ partial logics. You get multiple variants of equality. With one you can prove `1/0 = 1/0`, with one you can _dis_prove `1/0 = 1/0`, and maybe you even have other ones too? So I want a world in which writing `1/0 = 1/0` is _illegal_ (something akin to a type error). _And_ want that `!x. 1/x = 1/x` is illegal too (because x can take the value 0), but I _also_ want that `!x. ~(x = 0) ==> 1/x = 1/x` is fine (even although x _still_ can take the value 0). That's how things work in B. And this seems unlike IMPS to me. What I just want is to have some story + infrastructure that allows me to -- at the very very end -- prove that the result that I have established is "meaningful", in the sense that it doesn't depend on/refer to what functions do outside their domain. But that apart from that _everything_ is as it was before. Freek ------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
