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

[Professor James Davenport]

On Sat, August 28, 2010 1:34 pm, Lars Hellström wrote:
> Paul Libbrecht
begin_of_the_skype_highlighting     end_of_the_skype_highlighting skrev:
>
>> - uniqueness is the holy grail to be reached, I don't think it can be
>> in any way *ensured*. I had the impression rewriting systems were on a
>> safer side
>
> Uniqueness is indeed not ensured by the definition, but something one
> strongly desires if the point of the exercise is to find the canonical
> form of some given expression. (Generative grammars may also be viewed
> as rewriting systems, in which case uniqueness would only hold for
> singleton languages.) Asking questions about arbitrary rewriting
> systems runs straight into the general word problem, but questions
> asked about specific rewriting systems may well be possible to address
> computationally.
>
> Normally, you first want to prove termination (e.g. that you avoid
> silly rewrite cycles and rewrites that will forever make the result
> longer); many tools and techniques for this are available (cf.
> http://www.floc-conference.org/WST-home.html). Then checking whether
> all critical pairs satisfy the diamond property will typically (it
> depends slightly on what kind of things you allow as rules) yield an
> *algorithm* that for any finite rewrite system either proves that it is
> complete (that normal forms with respect to it are unique) or gives an
> example of an expression that can be rewritten to two different normal
> forms.
I seem to have come slightly late to this discussion - apologies.
For me the key points are the following.
(a) it is not now the case, and probably never will be, that all the
properties of all OMS are captured by the FMPs.
(b) Nevertheless, it is the case for SOME OMS that the FMPs totally
capture their behaviour w.r.t. some, "more primitive" OMS.
(c) There is CURRENTLY no way to say what sort of OMS and what sort of FMP
we have. As a concrete example, sin is defined in terms of exp, which is
also DMLF 4.14.E1, but log is only defined by 4.2.E1 if you read the
cavest textually adjacent to the equation. Wp and Wm arn't really defined
at all.

I don't see how better automation of the FMPs, by themselves, will solve
the problem, since we do now know which ONS are full defined. There are
indeed questions of orientation, and maybe we need to be more explicit.

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