=Paper=
{{Paper
|id=Vol-1186/paper-10
|storemode=property
|title=Another Look at Formal Mathematical Properties
|pdfUrl=https://ceur-ws.org/Vol-1186/paper-10.pdf
|volume=Vol-1186
|dblpUrl=https://dblp.org/rec/conf/mkm/Davenport14
}}
==Another Look at Formal Mathematical Properties==
https://ceur-ws.org/Vol-1186/paper-10.pdf
Another Look at Formal Mathematical Properties
James Davenport
(J.H.Davenport@bath.ac.uk).
September 2008: Bug fix 31/5/2014
1 History
1.1 Prior to the 2003 document
At the Twelfth OpenMath Workshop (Eindhoven meeting 15/16.6.1999), there
was a discussion about Formal Mathematical Properties. The minutes read as
follows.
AMC introduced a paper by himself and MK on “Defining Math-
ematical Properties”. He said that CDs did not necessarily introduce
the logical meaning of mathematical symbols. OpenMath should
involve the logic community more. While OpenMath has Formal
Mathematical Properties (FMPs), there is no differentiation between
definitions and consequences. Also, some objects do not have FMPs,
e.g. subset. He suggested a new tag, DefMP, which would be like
FMPs, but the DefMPs would have to define the mathematical ob-
ject uniquely. At least in theory, the FMPs would then be formally
proved as consequences of the DefMPs.
In the Esprit group, there were two objections: one that they
would scare many potential users, and the other was that people
might want different DefMPs. To the first, he answered that there
were many features of OpenMath that not everyone used. For the
second, he noted that signatures had been moved to separate files,
and maybe this would be appropriate for DefMPs.1
This led to a lively debate. GHG said that placing the DefMPs in
separate files was a move against the general trend towards databases.
MK in particular called for genuinely usable OpenMath tools, e.g.
for Reduce and Maple. Many agreed with him.
[Irrelevancies deleted.] MK proposed that, in the light of the
DefMP discussion above, which seemed to conclude that the DefMPs
should be in auxiliary files, FMPs should be moved to a different
kind of file. AMC agreed, but DPC did not. SB proposed, and
1 See also section 6.
1
JHD seconded, that FMPs should stay where they were. This was
agreed. A few amendments to the DTD for CDs were noted. DPC
pointed out that 5.4 (CD Signature files) and 5.5 (CD Groups) were
probably not final. MK suggested a DTD for defmp files, which
would be inserted after 5.4, after it had been discussed by e-mail.
AS suggested that some tags like CDVersion should also be present
in signature files.
1.2 2003
The 2003 document said the following,
In the last few years, JHD has come to understand more of the
motivation behind the DefMP proposal, and wishes to resurrect a
variant of it, in which FMPs would be qualified with some description
of their rôle.
This was part of JHD’s presentation at Hagenberg 2007: http://staff.bath.
ac.uk/masjhd/Slides/MKM2007.pdf, though not the published version [2]. JHD’s
notes of the Hagenberg meeting read as follows.
CSC [Claudio Sacerdoti Coen] distinguished three levels: nota-
tion (or presentation), content and logic. OpenMath, he thought,
does well at distinguishing content from notation. He then asked
whether DefMP wasn’t mixing the last two — how can I interpret
your DefMP if I don’t know your logic. JHD admitted that this
might be a problem for type 4 symbols. Type 3 symbols have a
purely extensional definition, so the logic used should be irrelevant.
2 Kinds of symbols
It seems to JHD that there are various kinds of symbol.
1. Those that are fundamentally primitive, and not defined at all. They may
still have FMPs, but these FMPs are merely about them, rather than
defining the symbol. An example would be
.
2. Those that OpenMath treats as primitive, and not defined at all in Open-
Math. These might not be primitive in mathematics, but OpenMath has
decided not to define them. They may still have FMPs, but these FMPs
are merely about them, rather than defining the symbol. An example
would be
,
2
whose only FMP is a representation of ∀k ∈ Z exp(z + 2kπi) = exp(z)
(which is equally true of 2 exp(z) and exp(2z) for example).
3. At the other end of the spectrum, there are those objects that Open-
Math defines (because mathematicians use them) but which are logically
redundant. An example of this is
,
whose FMP is a representation of sin(x) = exp(ix)−exp(−ix)
2i , which means
that all occurrences of sin can be removed from an OpenMath object
without changing the semantics. If the CD specified this, a system which
encountered a symbol like this could rewrite it knowing that there was no
semantic loss.
If it felt that sin is still “important”, and complex exponentials are not the
right response to a real function, how about csc, which can be perfectly
encapsulated via csc(x) = sin1 x ?
4. It would be possible2 (in fact the definition in integer1 is not of this
form, but rather in terms of products), to define
(whose STS states that it is a function N → N) with an FMP encoding
the recursive definition:
2 If it is argued that this is artificial, since this is not in fact the FMP, consider the example
Pn−m
of Stirling1 in combinat1, whose FMP is the encoding of Stirling1(n, m) = k=0
(−1)k ∗
binomial(n − 1 + k, n − m + k) ∗ binomial(2n − m, n − m − k) ∗ Stirling2(n, m).
3
In this case, it is possible to replace any particular numerical factorial by
a computation, but it is impossible to replace, say n! with a definition not
involving factorials (unless one extracts some kind of Y -expression from
that recursive definition, which is mere semantic trickery).
3 The OpenMath dilemma
The notation of mathematics is incredibly varied, and new notations and con-
cepts are permanently being introduced. This poses problems for OpenMath’s
goal of encouraging interoperability between tools, and future-proofing of data.
Equally, people have different views of mathematics, e.g. Real Analysis/Complex
Analysis, and this colours people’s views of what is “fundamental”
4 Kinds of FMP: 2008 Proposal
At the moment, the distinction we have made above is purely informal, and there
are no clues in the CD as to the meaning of any FMP. The DefMP proposal
mentioned above suggested that some FMPs were “defining”, and should be
treated differently. We propose a slightly weaker form: that some FMPs should
be marked, and therefore could be treated specially. More concretely, we propose
two special marks.
4
defining A defining FMP is one that can always be used as a definition of
a symbol. An example of this is the FMP for sin mentioned above.
In all contexts, it is legitimate to replace an occurrence of sin by the
corresponding right-hand side. Such FMPs will generally begin with an eq
operator, though this is not necessarily required. The following guarantees
must be met by such an FMP.
• A symbol can have at most one of them.
• The replacement value must not, either directly or indirectly by a
chain of such FMPs, involve the symbol being defined.
evaluating An evaluating FMP is one that can be used as a definition of how
to evaluate a symbol on a concrete instance of its input argument(s). The
following guarantees must be met by such an FMP.
♠ A symbol can have at most one of them.
♠ The replacement value must, after a finite number of applications of
this, and any other evaluating or defining FMPs, lead to an expression
free of the symbol being defined, whenever the symbol is applied to
concrete instances of the correct type(s).
5 The requirements for uniqueness: 2008
These requirements could be seen as posing the following questions.
1. Why restrict to one defining FMP?
2. Why restrict to one evaluating FMP?
3. Can one have one defining and one evaluating?
The first two are required, in JHD’s opinion, to avoid any ambiguity: if there
are two definitions of a symbol, are they proven to be consistent? Note that, in
the quote above, AMC called for greater interactions with the logic community.
It may be that, in the fullness of time, we will be able to allow two defining
FMPs accompanied (and there is currently no mechanism for doing this) with
a machine-checkable proof of consistency.
The other reason for insisting on uniqueness is that a CD-reading tool, which
has come across a symbol which its base application does not know, but which
has a defining FMP, has no choice about what to do: it replaces it by the
definition (and recurses if necessary). Otherwise the tool has to be far more
complicated.
The third question also raises the question of consistency. However, it does
not raise quite the same question of ambiguity, since such a tool would probably
use an evaluating FMP if it (knew that it) had a definite value, and a defining
one otherwise. Hence for the moment this proposal does not rule that out,
though this could clearly be debated.
5
6 Varieties of Theory
Acknowledgement: This section owes much to Lars Hellström.
As has been said before, there are multiple views of mathematics, e.g. Real
Analysis/Complex Analysis. In Complex Analysis, it is natural to reduce all
elementary transcendental functions in terms of exp/log, but for Real Analysis
this is not a good idea, as it introduces complex numbers where “they aren’t
needed”. Furthermore, for Real Analysis, there are two competing “natural”
theories, one in terms of sin θ and cos θ and the other in terms of tan θ2 .
These different theories may each have their uses: for example Pascal would
want “sin θ and cos θ”, but a CAD system would prefer “tan θ2 ” as not intro-
ducing algebraic dependencies. Neither would want “exp/log”. We therefore
propose, as a development of the 2008 proposal to allow a forest of DefMPs,
rather than a tree. Specifically, the FMP construct should also allow the at-
tribute theories=, with value a string which is a delimited3 list of theory names
(same syntax as operation names). No attribute would be the equivalent of
theories="default".
The uniqueness requirements ♠ above would then be interpreted per theory.
6.1 Further Suggestions by Lars
Also, if such names (I think the HTML class is of type NMTOKENS) can be names-
paced, then that would probably be a nice way of associating the status of FMPs
with theories. E.g. there could be
to mean that “this FMP is known to be a definition in The Elements, an axiom
according to Hilbert, and a theorem in some (unspecified) other theory”. And
the point about namespaces is that one would elsewhere have gone
to provide a stable reference to “the theory”, whatever that may be. I find the
idea appealing that the URI for the Euclid theory should be an URL for The
Elements, but that’s probably a matter for DML/MKM to hash out. :-)
7 Concrete changes
We propose that be allowed an attribute type, so that one could write
in the first case, and
3 JHD needs some helphere. he had originally written ”comma,delimited, but space-
delimited as in NMTOKENS might be better.
6
in the second.
There would be an optional additional attribute theories=, interpreted as
in section 6, with the uniqueness requirements ♠ above being interpreted per
theory, which, if we adopted section 6.1, would be “per the name before the :”.
Existing systems could ignore these, but new systems might interpret them
on the lines suggested above.
References
[1] Corless,R.M., Davenport,J.H., Jeffrey,D.J. & Watt,S.M., “According to
Abramowitz and Stegun”. SIGSAM Bulletin 34 (2000) 2, pp. 58–65.
[2] Davenport,J.H. & Libbrecht,P., The Freedom to Extend OpenMath and
its Utility. Mathematics in Computer Science 2(2008/9) pp. 379–398. (Full
Version: http://hdl.handle.net/10247/468, 2008.)
7