From: Rob Arthan <rda@le...>  20050216 21:23:28

John, On Tuesday 15 Feb 2005 11:47 pm, John Harrison wrote: > Hi Rob, > >  Having done a quick survey, I find that HOL Light follows the old way >  (with 1  2 + 1 equal to 2), while HOL 4 and IsabelleHOL follow typical >  programming language associativities to make 1  2 + 1 = 0. > > No, in HOL Light "1  2 + 1" means "(1  2) + 1", so it's 0 too. (Well, > if you're talking about cutoff subtraction over N it's 1, but that's > an orthogonal issue.) >... > > Indeed, HOL Light does something quite close to what you are proposing: > "+" is rightassociative and "" is leftassociative; the expression you > gave is parsed as it is because "" also has a higher precedence than > "+". Generally I find this works quite well. Apologies! I made a mistake in my test with HOL Light. I see now that it is just as you say  and this is exactly what I have been reinventing for ProofPowerHOL. So thanks for the recommendation! >... > > I tend to find rightassociation a more natural convention where it's > possible, perhaps because it reminds me of functional programming over > lists. I doubt if that holds for the average mathematician, though. I'd be interested in more views on that. If I were a mathematician teaching standard topics like polynomial division or gaussian elimination in systems of linear equations, I don't think I'd buy into the reading of + as a leftassociative binary operator either. Regards, Rob. 