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

[Paul Libbrecht]

Le 25 août 2010 à 12:26, Lars Hellström a écrit :
>> (applying a definition such as the binomial coefficient's  
>> factorial  expression certainly shouldn't go backwards for a normal  
>> search  comparison, coming from 1 to sin^2 x + cos^2 x would be  
>> horribly  surprising).
>> I am not sure what is the criterion, except length shortening,
>
> The choice of criterion for orienting one's given identities into  
> rewrite rules can be a Very Hard Problem (not unlike the problem of  
> "proving theorem X"). Length shortening can be a good principle to  
> start with, but it is not unusual that one has to make slight  
> deviations from it.
> Since you seem to be unfamiliar with rewriting, I should perhaps  
> also point out that you often need to add to your system derived  
> rules that no sane person would pick as axioms, just to ensure that  
> the normal (canonical) forms with respect to it are unique.

Well, let's continue the lesson... applying it to canonicalization for  
search purposes. It's quite human and I have the impression we're  
waiting on the invasion of rewriting systems:

- 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
- the choice of axioms is based on the reasoning of mathematicians  
but, more importantly, partially on the knowledge of the users. E.g.  
that it knows commutativity or that it knows that a/b * c/d is (a*c)/ 
(b/d), an assumption that is probably usual but should never be done  
if teaching fraction calculus!


paul