On Tue, Apr 9, 2013 at 2:22 AM, Freek Wiedijk <[email protected]> wrote:
> 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).
>
Questions about the notion of definition always strike me as wonderful
opportunities to connect high school-level math with actual ideas of
mathematics. I think most people on this mailing list would agree that the
typical math curriculum (for sure in the U.S.) focuses far too much on
following rules to get answers and too little on mathematical ideas. And
the notion of a definition seems like a really basic math concept. So for
me as well this is a very interesting question, not just a practical one or
a minor curiosity.
>
> 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.
>
In a classic HOL system such as HOL Light suppose f is defined using a
description operator that maps from singleton sets to the single member.
(Let's call it "the" rather than "iota".) as "f x = the {y | <formula>}".
Then there is another function F with values that are sets, definable as F
x = {y | <formula>}. Then the domain where f x is well-defined is the set
of x'es where there is a unique y such that y is in F x, so we could say
f_domain_of_definition = {x | ?!y. <formula>}. So your proposal seems
totally doable (and I think a fine idea).
I think this systematizes the approach that leads to using x != 0 ==> recip
x * x = 1 as a specification for reciprocal, or Konrad's example with DIV
and MOD. Hopefully I am not missing something here.
>
> 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.
>
I think of equality of partial functions as something that is explicitly or
implicitly relative to their domains of definition, in fact the
intersection of their domains of definition. Perhaps we might say f and g
are similar if they produce equal values over the intersection of their
domains of definition.
For what it's worth, this looks a lot like some of the issues that the
Lutins logic of IMPS has to deal with, and as I recall, William Farmer
makes a comment in a paper, relating the Lutins approach to definedness
with the use of set-valued functions.
>
> 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.
>
D sure looks to me like the Lutins/IMPS definedness operator. I prefer to
stick with the simpler HOL-style foundations, but of course the issue is
genuine. My impression is that the authors of Lutins know how to
systematically translate Lutins statements into statements in a regular HOL
logic that has no special handling of definedness.
> 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
