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