| When I read realTheory, I see the REAL_INV_0 theorem. Its content
| is inv 0 = 0, according to my understanding, it means that the
| reciprocal of real_0 is real_0. But it is contradictory to the
| knowledge of maths. The definition of inv in realaxTheory. How to
| understand inv 0 = 0? I want to know the advantages of such a
| definition.
This goes back to the construction of the reals in HOL88, as described in
my 1996 PhD thesis "Theorem Proving with the Real Numbers". Here is the
LaTeX for the passage where this decision is explained and to some extent
justified:
HOL's functions are all total, and it doesn't have a convenient means
of defining subtypes. This means that it's easiest to make the
multiplicative inverse a total function $\real \to \real$, giving us
an additional choice over the value of $0^{-1}$. In early versions of
the theory, we made $0^{-1}$ arbitrary, i.e. $\eps{x} \False$. However
this isn't the same as real undefinedness, which propagates through
expressions. In particular, since we take the standard definition of
division, $x / y = x y^{-1}$, this means that $0 / 0 = 0$, since $0$
times any real number is $0$. Because of this, the idea of making the
result arbitrary seemed artificial, so in the latest version, we have
boldly defined $0^{-1} = 0$. This achieves considerable formal
streamlining of theorems about inversion, allowing us to prove the
following equations without any awkward sideconditions:
\begin{eqnarray*}
\all{x} (x^{-1})^{-1} & = & x \\
\all{x} (-x)^{-1} & = & -x^{-1} \\
\all{x\;y} (x y)^{-1} & = & x^{-1} y^{-1} \\
\all{x} x^{-1} = 0 & \Iff & x = 0 \\
\all{x} x^{-1} > 0 & \Iff & x > 0
\end{eqnarray*}
For the reader who is disturbed by our choice, let us remark that we
will discuss the role of partial functions at greater length when we
have shown them in action in more complicated mathematical situations.
[....]
In any case, we think it is important that the reader or user of a
formal treatment should be aware of precisely what the situation is.
Our decision to set $0^{-1} = 0$ is simple and straightforward, in
contrast to some approaches to undefinedness that we consider later.
As \citeN{arthan-undefinedness} remarks `all but the most expert
readers will be ill-served by formal expositions which make use of
devious tricks'. (This is in the context of computer system
specification, but probably holds equal weight for pure mathematics.)
Note, by the way, that axiomatizing the reals in first order logic
gives rise to similar problems, since all function symbols are meant
to be interpreted as total functions.\footnote{\citeN{hodges-model}
points out that for various field-specific notions such as `subfield'
and `finitely generated' to be instantiations of their model-theoretic
generalizations, it's necessary to include the multiplicative inverse
in the signature of fields and to take $0^{-1} = 0$.}
I would say that the definition should be viewed as *extending* the
usual mathematical inverse function, rather than as being in
*contradiction* with it. If you like, think of our function as inv'
and the partial function as inv. Obviously there's nothing to stop us
defining inv'(0) = 0 if we want to, provided that we prove all the
theorems according to this definition. And since inv and inv' agree
except on the value zero, you only need to check the actual theorem
itself to see whether this distinction matters, and you can freely
exploit the convenient properties of inv' inside. (In logician's
parlance, it is a conservative extension.)
If you would prefer a different approach to partial functions, there
are several that are known and supported by various theorem-proving
systems. I'll take the liberty of quoting a later passage of my
PhD thesis:
One simple possibility is to use an untyped system like standard set
theory. Here, the lack of types gives more freedom to adopt special
values in the case of undefinedness. For example, many functions that
we want to be undefined in certain places have a natural `type' $X \to
Y$. (The inverse function $\real \to \real$, and the limit operation
$(\nat \to \real) \to \real$ are just two we have discussed here.) One
might adopt the convention of extending their ranges to $Y \Union
\{Y\}$ and giving the function the value $Y$ in the case of
undefinedness.\footnote{We are assuming here that $Y \not\in Y$, but
one could surely find counterparts to our convention in set theories
where this is not guaranteed \cite{holmes-naive}. Even there, $Y
\not\in Y$ is still guaranteed for `small' sets, which includes pretty
well all concrete sets used in mathematics.} This would seem to give
many of the benefits of a first-class notion of definedness without
complicating the foundational system.
A more radical approach is to adopt a logic in which certain terms can
be `undefined'. Then, on the understanding that $s = t$ means `$s$ and
$t$ are defined and equal', the statement $lim\;s = l$ would, assuming
that $l$ is defined, incorporate the information that $s$ does
actually converge. Such a logic is implemented by the IMPS system
\cite{farmer-imps}, which was expressly designed for the formalization
of mathematics, and otherwise has a type theory not dissimilar to
HOL's. However some dislike the idea of complicating the underlying
logic, either because of a desire for simplicity, or because of
concern that proofs are likely to become cluttered with definability
assumptions. The original LCF systems described by
\citeN{gordon-lcfbook} and \citeN{paulson-lcfbook} implemented a
similar logic (a special `bottom' element denoted undefinedness), as
did the first version of the LAMBDA hardware verification tool, and in
both cases, the clutter was considerable.
An alternative approach, long used by the Nuprl system and more
recently by PVS, is to make all functions total, but exploit a
facility for transparent subtypes. In such a scheme, $lim$ would have
not type $(\nat \to \real) \to \real$ but rather $\{ s \mid \ex{l} s
\to l \} \to \real$. Now the logic is still almost as simple (and
subtypes are desirable for other reasons too, as we have already
noted). Now if an assertion $lim\;s = l$ is well-typed, then $s$ must
converge. However there is still an additional load of proof
obligations involved in typechecking, which is no longer decidable as
in HOL. Moreover, it means that the underlying types can become
extremely complicated and counterintuitive. Finally, it is less
flexible than the IMPS approach, which, as it actually features a
definedness operator, can employ its own bespoke notions of equality.
For example in many informal contexts it seems that the equality $s =
t$ is interpreted as `quasi-equality' (using IMPS terminology), i.e.
`either $s$ and $t$ are both undefined, or they are both defined and
equal'. On such a reading, for example, the equation ${d \over dx}
(1/x) = - 1/x^2$ is strictly valid. Actually \citeN{freyd-allegories}
use a special asymmetric `Venturi tube' equality meaning `if the left
hand side is defined then so is the right and they are equal'. For
other contrasts between the approaches to undefinedness, consider the
following:
$$ \all{x \in \real} tan(x) = 0 \Imp \ex{n \in \num} x = n \pi $$
Assuming that $tan(x)$ is defined as $sin(x) / cos(x)$, this formula
distinguishes all the major approaches to undefinedness:
\begin{itemize}
\item In our formalization with $0^{-1} = 0$ it is false, since
$tan(x) = sin(x) / cos(x)$ is also $0$ at the values where $tan(x)$ is
conventionally regarded as `undefined', i.e. when $x = \pm {2 n + 1
\over 2} \pi$.
\item Had we just used an arbitrary value for $0^{-1}$ (say $\eps{x}
\False$) then the formula would be neither provable nor refutable,
since that would require settling whether the arbitrary value is in
fact $0$.
\item In the IMPS approach, the theorem is true, since $tan(x) = 0$
implies that $tan(x)$ is defined. (It makes no difference whether
equality is interpreted as strict or quasi-equality, since $0$ is
certainly defined.)
\item For approaches relying on total functions out of subtypes, the
truth of this formula depends on how typechecking and logic interact.
However in the usual scheme, as used for example by PVS, the above
formula is a typing error without a restriction on the quantified
variable. In typechecking $P[x] \Imp Q[x]$, the formula $P[x]$ is
assumed when typechecking $Q[x]$, but an assertion that $P[x]$ is
well-typed is not.
\end{itemize}
John.
------------------------------------------------------------------------------
Centralized Desktop Delivery: Dell and VMware Reference Architecture
Simplifying enterprise desktop deployment and management using
Dell EqualLogic storage and VMware View: A highly scalable, end-to-end
client virtualization framework. Read more!
http://p.sf.net/sfu/dell-eql-dev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
