> I presume that the same sort of thing could be done with reciprocal of
zero, and the definition without
> the side condition was chosen as being easier to work with.
Yes, I think I remember John Harrison discussing the issue in his thesis
and concluding that working
with an unconditional rewrite was sufficiently nice that the divergence
from mathematical practice was
justified.
Konrad.
On Fri, Apr 5, 2013 at 12:43 AM, Cris Perdue <[email protected]> wrote:
> Konrad,
>
> Yes, your example with MOD and DIV I think is just the right sort of
> thing. It's still annoying to
> know that the result of dividing by zero is some number, but not as bad as
> having a definite but unexpected result, and the issue is less obtrusive
> this way, too.
>
> I presume that the same sort of thing could be done with reciprocal of
> zero, and the definition without the side condition was chosen as being
> easier to work with.
>
> -Cris
>
>
> On Thu, Apr 4, 2013 at 4:00 PM, Konrad Slind <[email protected]>wrote:
>
>> Partial functions are annoying, no matter how you approach them.
>>
>> One way to introduce a partial operation in HOL is with
>> new_specification. In contrast with new_definition, this allows
>> you to introduce a constant with only its relevant properties.
>> Consider, for example, the so-called division algorithm
>> arithmeticTheory.DIVISION:
>>
>> |- !n. 0 < n ==>
>> !k. (k = k DIV n * n + k MOD n) /\ k MOD n < n
>>
>> Check the development in src/num/theories/arithmeticScript.sml
>> for details.
>>
>> Konrad.
>>
>>
>>
>>
>> On Thu, Apr 4, 2013 at 5:11 PM, Cris Perdue <[email protected]> wrote:
>>
>>> Dear HOL experts,
>>>
>>> I am hoping for wisdom and recommendations from you all related to a
>>> question I have. Let me start with a bit of background information, which
>>> is here largely to orient you to my understanding of the situation. I know
>>> the facts are elementary.
>>>
>>> Usually in mathematics some operations are considered to be undefined,
>>> such as division by zero. In HOL (Light - and I presume other HOL
>>> dialects), I see that the reciprocal of zero is defined to be zero, and I
>>> see operations on other types such as natural numbers are defined
>>> everywhere.
>>>
>>> Functions in type theory are total, a different point of view than
>>> definitions of functions as relations or sets of ordered pairs. It is not
>>> necessary however to specify what the value of a function is for all
>>> possible inputs. In that sense, a function specification in type theory may
>>> in fact define a family (set) of functions that all satisfy the
>>> specification.
>>>
>>> Considering division by (reciprocal of) zero, since for all real x, x
>>> * 0 = 0, there is no real x such that x * 0 = 1, so there is no reciprocal
>>> of 0. It could be some non-real value, and that is the source of my
>>> question.
>>>
>>> For some similar situations such as subtraction or division of natural
>>> numbers, the classic response is to extend the domain to the integers or
>>> the rational numbers, but normally division by zero is simply undefined in
>>> any field.
>>>
>>> The application I am working on (Prooftoys <http://prooftoys.org/>) is
>>> aimed mainly at people who want to extend their understanding of
>>> mathematics -- students in the broad sense; and I strenuously want to avoid
>>> introducing mathematical facts that vary from the norm, such as an unusual
>>> definition of reciprocal.
>>>
>>> For my own use I have no problem with introduction of a specific
>>> "undefined" value in addition to the reals to support cases like this, but
>>> the extra constant or constants are not the usual textbook mathematics.
>>>
>>> Taking another approach, the IMPS system has undefinedness built into
>>> the logic, which seems to me even more visible, and it makes the logic more
>>> complex, also seemingly undesirable in this kind of application.
>>>
>>> A relatively unobtrusive approach seems to be to define reals, natural
>>> numbers, etc. as subsets of "adequately large" types, and to leave
>>> unspecified the value of something like a division by zero. For example the
>>> reals might be taken as a subset of the set of sets of integers. If that
>>> seems one of the most attractive alternatives, would any of you like to
>>> suggest some existing formulation in the HOL setting?
>>>
>>> Can anyone offer suggestions for attractive ways of defining the real
>>> numbers (and/or other classic mathematical types) in higher-order logic in
>>> ways that are clean and otherwise attractive, and with the needs of
>>> non-expert users in mind?
>>>
>>> Are there some known approaches that might be considered more attractive
>>> than others?
>>>
>>> It seems to me the top priority in this kind of application is to make
>>> usage simple and classic in style, ideally also the theory behind it.
>>> Elegant constructions of the types would be nice to have, but secondary.
>>>
>>> Thanks in advance,
>>> Cris
>>>
>>>
>>>
>>> ------------------------------------------------------------------------------
>>> Minimize network downtime and maximize team effectiveness.
>>> Reduce network management and security costs.Learn how to hire
>>> the most talented Cisco Certified professionals. Visit the
>>> Employer Resources Portal
>>> http://www.cisco.com/web/learning/employer_resources/index.html
>>> _______________________________________________
>>> hol-info mailing list
>>> [email protected]
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>>
>>
>
------------------------------------------------------------------------------
Minimize network downtime and maximize team effectiveness.
Reduce network management and security costs.Learn how to hire
the most talented Cisco Certified professionals. Visit the
Employer Resources Portal
http://www.cisco.com/web/learning/employer_resources/index.html
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
