Hi Chris, Thanks for bringing up this topic, which is very interesting question to me. It's question III in my talk <http://www.cs.ru.nl/~freek/talks/lsfa.pdf>. I'm replying here because there is an approach that I've been wanting to develop for a while now (but haven't really started work on).
The idea is to _not_ change the HOL logic to address partiality, but instead to define an operation on the meta level that assigns to a HOL term f another term D(f) that states that the term f is "well defined". For instance if f is the term `1/0` then D(f) should be equivalent to `~(0 = 0)`. Exactly how this would work I don't know: probably each HOL constant c that you define would have another constant c_wd associated to it that corresponds to the "domain" of that HOL constant c. So `real_div` (division on the reals) would have a constant `real_div_wd` associated to it that corresponds to the predicate saying that the second argument should not be zero. Semantically, what would happen is that there would be a HOL model in which everything is partial, and then there would be a mapping into the traditional HOL model in which all those functions have been extended to make them total, while also there have been functions added that "remember" where in the original model the functions were partial. Something like that. Surprisingly, the very basic HOL function, equality, also would be a _partial_ function in such a setting! When comparing partial functions f and g the comparison `f = g` would be undefined if there was an x for which `f x` and `g x` are both undefined. So this operation "D" preferably would hvae nice properties. In particular you would like D(D(f)) to be provable for _any_ HOL term, so even if D(f) would not hold. Also, you would like to have the property that a HOL proposition is provable with all intermediate sequents "well defined" (the "D" probably would have to be extended to sequents for that) if and only if only the final sequent is well defined (so the proof has been done without paying any attention to well definedness of the intermediate steps.) If that would hold, then all you would need to do is first prove a theorem |- f in the traditional HOL way, and then at the very end show that |- D(f) also is provable, and still be very happy with it. A property like that for first order logic we proved in <http://www.cs.ru.nl/~freek/pubs/partial.pdf>. I have _no_ idea whether you could have something like that for the HOL logic too, but I would really like that. Of course this is all very much related to how systems like PVS and the B method deal with partiality, and ACL2 has something called "ACL2/gold" that is similar to this too, I think. So maybe what I'm asking for here already has been all worked out and is well known etc. If so, I'd like to hear about it. 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
