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
