In my opinion, the best way of dealing with this is to use option types: None
denoting the undefined value. This makes function composition tedious but you
can use a monad to make this easier.
Now, it is not standard w.r.t. usual maths. But I'm not sure whether usual
maths are doing this the right way...
--
Vincent Aravantinos
PostDoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
Am 2013-04-04 um 18:11 schrieb Cris Perdue <c...@perdues.com>:
> 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) 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
