This treatment of division by zero is fairly common in automated theorem proving. I have written a discussion of the issues near the end of section 4.1.2 of my paper on MetiTarski:
http://www.cl.cam.ac.uk/~lp15/papers/Arith/MetiTarski-jar.pdf The following paper is also relevant: http://portal.acm.org/citation.cfm?id=1219095 Larry Paulson On 3 Nov 2010, at 23:45, [email protected] wrote: > 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. ------------------------------------------------------------------------------ The Next 800 Companies to Lead America's Growth: New Video Whitepaper David G. Thomson, author of the best-selling book "Blueprint to a Billion" shares his insights and actions to help propel your business during the next growth cycle. Listen Now! http://p.sf.net/sfu/SAP-dev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
