Vincent,
Thanks for your input on this. Are there some examples in HOL or HOL Light
where the approach you suggest with option types is used? (Preferably some
elementary theory where I won't get too lost as a non-mathematician.) This
is unfamiliar to me except of course in the programming language.
Regards,
Cris
On Thu, Apr 4, 2013 at 4:28 PM, Vincent Aravantinos <
[email protected]> wrote:
> 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 <[email protected]>:
>
> 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
