[Om] Adding DLMF links to CDs [Re: How to translate csymbol/@definitionURL]

[Professor James Davenport]

On Mon, July 19, 2010 4:31 pm, Bruce Miller wrote:
> I don't know that I intentionally suggested that, or followed
> someone elses suggestion, but if such a URL were to
> become valid in the near term, it would probably just
> be a restatement of the informal notion of
> 4.14.E1 "defining" sine.  That is,
> http://dlmf.nist.gov/#sin would (currently) redirect to
> http://dlmf.nist.gov/4.14.E1 which would redirect to
> http://dlmf.nist.gov/4.14#E1
>
> I would imagine that it is valid for the 1st and 2nd
> URI's in that list can reasonably be taken as
> _identifying_ distinct things (a definition of sine
> vs an equation, respectively).  The practicalities of
> a working web server could be confusing however.
>
> Whether DLMF should provide an explicit URL indicating
> "sine itself", or it's definition ... or whether we
> should even think of ourselves as defining sine...
> is something this discussion can help answer.
This is close to the old DeFMP discussion (why am I not surprised), To
summarise, some FMPs ARE definitions in the Principia Mathematica sense
that the definiendum can be replaced by the definiens. So 4.14.1 can be
read as a definition of sin, but 4.2.2 (by itself) cannot be a read as a
definition of log. The DeFMP debate was about stating this precisely, i.e.
this FMP is a definition, and it is legal to replace the definiendum by
the definiens. A use-case I had was an OM->Pascal translater, which would
replace cot by cos/sin [Pascal did not support cot etc.].

As with OpenMath, it would be nice if the DLMF made it clear in a
mahcine-parsable way (that's my, very small in the case of DLMF, objection
to the current system in both DLMF and OpenMath) which
equations/properties are definitions in this sense.

James Davenport
Lecturer on XX10190, CM30070, CM30078/50123, CM50209
Hebron & Medlock Professor of Information Technology, University of Bath
OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009
IMU Committee on Electronic Information and Communication
Council of the British Computer Society
Federal Council, International Foundation for Computational Logic