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
