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 <c...@perdues.com> 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
> hol-info@lists.sourceforge.net
> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
