This is a good question, and I am not best placed to fully answer it, but
hopefully can help.
It's first necessary to realise that all functions (i.e. things of type
`:A->B` for some A and B) in HOL are total, and so any value in the domain
type maps to some value. This differs from conventional mathematics, where
certain functions such as reciprocal do not include all values in their
domain. So given that `inv 0` maps to some value, there is a choice of
whether to specifically tie down what that value is, or to leave it
"unspecified" (i.e. it is some real number value, but impossible to
determine which one).
Not that even if it is unspecified, then, given that it takes some value, it
is still possible to prove some results that may (or may not) seem
surprising, e.g.
|- !x y. x * inv 0 + y * inv 0 = inv 0 * (x + y)
What they have done in HOL4 (and HOL Light) is chosen to pin it down to a
specific value. It is considered that this is harmless in terms of
soundness. I understand that the value is chosen so that it conveniently
fits with various algebraic properties, such as:
|- !x y. inv x = inv y <=> x = y [ HOL4's REAL_INV_INJ ]
|- !x. inv (inv x) = x [ HOL4's REAL_INV_INV ]
This means it's possible to prove certain property theorems without non-zero
side conditions, and so apply these theorems in a proiof without having to
prove side conditions, making interactive and automated theorem proving
easier and quicker.
I'm not sure why other properties, such as 'REAL_INV_MUL' keep side
conditions when they don't need them. For example:
|- !x y. x <> 0 /\ y <> 0 ==> inv x * inv y = inv (x * y) [ HOL4's
REAL_INV_MUL ]
|- !x y. inv x * inv y = inv (x * y) [ HOL Light 's REAL_INV_MUL ]
This is perhaps for historical reasons - I think HOL did not previously tie
down the value, but then HOL Light did and influenced HOL4 (I may be wrong
about this). Perhaps some theorems in HOL4 have not yet been updated.
Personally I'm not sure whether I'm comfortable with the idea of tying down
the value (but am willing to be convinced), and so am not its greatest
advocate! I'm not exactly sure what makes me feel more uncomfortable with
this compared to not tying it down to a specific value (which still makes me
feel a little uncomfortable!), but I think it's related to the increased
risk of users writing formal specifications with unintentional meaning.
Mark Adams
on 28/10/10 2:10 PM, liliminga <[email protected]> wrote:
> Hello,
>
> When I read realTheory, I see the REAL_INV_0 theorem. Its content is inv 0
= 0,
> according to my understanding, it means that the reciprocal of real_0
> is real_0. But it is contradictory to the knowledge of maths. The
definition
> of inv in realaxTheory. How to understand inv 0 = 0? I want to know the
> advantages of such a definition.
>
>
>
> ----------------------------------------
>
>
----------------------------------------------------------------------------
> --
> Nokia and AT&T present the 2010 Calling All Innovators-North America
contest
> Create new apps & games for the Nokia N8 for consumers in U.S. and Canada
> $10 million total in prizes - $4M cash, 500 devices, nearly $6M in
marketing
> Develop with Nokia Qt SDK, Web Runtime, or Java and Publish to Ovi Store
> http://p.sf.net/sfu/nokia-dev2dev
>
>
> ----------------------------------------
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
------------------------------------------------------------------------------
Nokia and AT&T present the 2010 Calling All Innovators-North America contest
Create new apps & games for the Nokia N8 for consumers in U.S. and Canada
$10 million total in prizes - $4M cash, 500 devices, nearly $6M in marketing
Develop with Nokia Qt SDK, Web Runtime, or Java and Publish to Ovi Store
http://p.sf.net/sfu/nokia-dev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
