Re: [Hol-info] Associativity of binary operators

[John H. <Joh...@cl...>]

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 Isabelle-HOL 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.)                                                       

  # `1 - 2 + 1`;;
  val it : term = `1 - 2 + 1`
  # dest_comb it;;
  val it : term * term = (`(+) (1 - 2)`, `1`)

Indeed, HOL Light does something quite close to what you are proposing:
"+" is right-associative and "-" is left-associative; the expression you
gave is parsed as it is because "-" also has a higher precedence than
"+". Generally I find this works quite well.

| It seems that both  HOL 4 and Isabelle-HOL use right-associative
| normal forms for arithmetic expressions, so that normalisation
| produces an expression containing a maximal number of brackets. Thus
| HOL 4 does:
|
| - numRingLib.NUM_NORM_CONV (Term `(x+y)*(x+y+z):num`);
| val it =
|     |- (x + y) * (x + y + z) =
|        x * x + (2 * (x * y) + (x * z + (y * y + y * z))) : thm

The analogous thing in HOL Light also uses a right-associative normal
form, but because "+" is right-associative this prints without any
bracketing.

  # NUM_NORMALIZE_CONV `(x+y)*(x+y+z):num`;;
  val it : thm =
    |- (x + y) * (x + y + z) = x EXP 2 + 2 * x * y + x * z + y EXP 2 + y * z

I tend to find right-association 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.

John.