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

[Lars Hellström]

Paul Libbrecht skrev:
> Well, let's continue the lesson... applying it to canonicalization for  
> search purposes.

Where of course canonisation of data may turn out to be a too expensive 
operation to be applied to the entire database being searched, and 
other methods must be used to sieve it first, but that's true 
regardless of how you decide equality.

> It's quite human and I have the impression we're  
> waiting on the invasion of rewriting systems:

They have been around for ages... A problem publicity-wise is that when 
it was new then computers were too small to fit much anything in 
memory. The special case that is Gröbner basis theory has enjoyed a 
period of being hot, however.

> - 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.

Lars Hellström