1.1
At the Twelfth OpenMath Workshop (Eindhoven meeting 15/16.6.1999), there was a discussion about Formal Mathematical Properties. The minutes read as follows.
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
de nitions and consequences. Also, some objects do not have FMPs, e.g. subset. He suggested a new tag, DefMP, which would be like
would scare many potential users, and the other was that people might want di erent DefMPs. To the rst, 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 les, and maybe this would be appropriate for DefMPs.1
separate les was a move against the general trend towards databases.
for Reduce and Maple. Many agreed with him.
[Irrelevancies deleted.] MK proposed that, in the light of the
1See also section 6.
agreed. A few amendments to the DTD for CDs were noted. DPC pointed out that 5.4 (CD Signature les) and 5.5 (CD Groups) were probably not nal. MK suggested a DTD for defmp les, which would be inserted after 5.4, after it had been discussed by e-mail.
1.2 2003
This was part of JHD's presentation at Hagenberg 2007: http://staff.bath.
ac.uk/masjhd/Slides/MKM2007.pdf, though not the published version [
CSC [Claudio Sacerdoti Coen] distinguished three levels: notation (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 de nition, so the logic used should be irrelevant. 2
<OMS name="set" cd="set1"/>.
Math. These might not be primitive in mathematics, but OpenMath has decided not to de ne them. They may still have FMPs, but these FMPs are merely about them, rather than de ning the symbol. An example would be <OMS name="exp" cd="transc1"/>, whose only FMP is a representation of 8k 2 Z exp(z + 2k i) = exp(z) (which is equally true of 2 exp(z) and exp(2z) for example).
<OMS name="sin" cd="transc1"/>, whose FMP is a representation of sin(x) = exp(ix) exp( ix) , which means 2i that all occurrences of sin can be removed from an OpenMath object without changing the semantics. If the CD speci ed 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 de nition in integer1 is not of this form, but rather in terms of products), to de ne <OMS name="factorial" cd="integer1"/> (whose STS states that it is a function N ! N) with an FMP encoding the recursive de nition: <OMOBJ> <OMA> <OMS name="and" cd="logic1"/> <OMA> <OMS name="eq" cd="relation1"/> <OMA> <OMS name="factorial" cd="integer1"/> <OMS name="zero" cd="arith1"/> </OMA> <OMS name="one" cd="arith1"/> </OMA> <OMA> <OMS name="implies" cd="logic1"/> <OMA> <OMS name="gt" cd="relation1"/> <OMV name="n"/> <OMS name="zero" cd="arith1"/> 2If it is argued that this is arti cial, since this is not in fact the FMP, consider the example of Stirling1 in combinat1, whose FMP is the encoding of Stirling1(n; m) = Pkn=0m( 1)k binomial(n 1 + k; n m + k) binomial(2n m; n m k) Stirling2(n; m). </OMA> <OMA> <OMS name="eq" cd="relation1"/> <OMA> <OMS name="factorial" cd="integer1"/> <OMV name="n"/> </OMA> <OMA> <OMS name="times" cd="arith1"/> <OMV name="n"/> <OMA> <OMS name="factorial" cd="integer1"/> <OMA> <OMS name="minus" cd="arith1"/> <OMV name="n"/> <OMS name="one" cd="arith1"/> </OMA> </OMA> </OMA> </OMA> </OMA> </OMA> </OMOBJ>
3
The notation of mathematics is incredibly varied, and new notations and concepts are permanently being introduced. This poses problems for OpenMath's goal of encouraging interoperability between tools, and future-proo ng of data.
Equally, people have di erent views of mathematics, e.g. Real Analysis/Complex
4
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 \de ning", and should be treated di erently. 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. de ning A de ning FMP is one that can always be used as a de nition of a symbol. An example of this is the FMP for sin mentioned above.
The replacement value must not, either directly or indirectly by a chain of such FMPs, involve the symbol being de ned. evaluating An evaluating FMP is one that can be used as a de nition 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 nite number of applications of this, and any other evaluating or de ning FMPs, lead to an expression free of the symbol being de ned, whenever the symbol is applied to concrete instances of the correct type(s). 5
The requirements for uniqueness: 2008
The rst two are required, in JHD's opinion, to avoid any ambiguity: if there are two de nitions 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 de ning FMPs accompanied (and there is currently no mechanism for doing this) with a machine-checkable proof of consistency.
has come across a symbol which its base application does not know, but which has a de ning FMP, has no choice about what to do: it replaces it by the de nition (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 de nite value, and a de ning one otherwise. Hence for the moment this proposal does not rule that out, though this could clearly be debated.
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 di erent theories may each have their uses: for example Pascal would want \sin and cos ", but a CAD system would prefer \tan 2 " as not introducing 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. Speci cally, the FMP construct should also allow the attribute 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
Also, if such names (I think the HTML class is of type NMTOKENS) can be namespaced, then that would probably be a nice way of associating the status of FMPs with theories. E.g. there could be <FMP type="Euclid:definition Hilbert:axiom theorem"> to mean that \this FMP is known to be a de nition in The Elements, an axiom according to Hilbert, and a theorem in some (unspeci ed) other theory". And the point about namespaces is that one would elsewhere have gone <CD xmlns:Euclid="some-uri" xmlns:Hilbert="some-other-uri"> to provide a stable reference to \the theory", whatever that may be. I nd the idea appealing that the URI for the Euclid theory should be an URL for The
7
<FMP type="defining"> in the rst case, and <FMP type="evaluating">
3JHD needs some helphere. he had originally written "comma,delimited, but spacedelimited as in NMTOKENS might be better. 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 :".