Re: [Hol-info] Associativity of binary operators

 Re: [Hol-info] Associativity of binary operators From: Rob Arthan - 2005-02-16 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 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.) >... > > 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. 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 ProofPower-HOL. So thanks for the recommendation! >... > > 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. 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 left-associative binary operator either. Regards, Rob. ```

 Re: [Hol-info] Associativity of binary operators From: John Harrison - 2005-02-15 23:47:33 ```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. ```
 Re: [Hol-info] Associativity of binary operators From: Rob Arthan - 2005-02-16 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 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.) >... > > 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. 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 ProofPower-HOL. So thanks for the recommendation! >... > > 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. 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 left-associative binary operator either. Regards, Rob. ```
 Re: [Hol-info] Bug in HOL Light? From: John Harrison - 2006-01-06 15:49:35 ```Hi Rob, | I can thoroughly recommend the way Kevin Blackburn implemented the subgoal | package in ProofPower based on ideas of Roger Jones. The logical state of | the proof is represented by a theorem whose conclusion represents the | original goal and whose assumptions represents the outstanding subgoals (a | sequent being essentially represented by a universally closed implication). I did consider this possibility when I was designing HOL Light. It certainly has some technical advantages, particularly in making metavariables almost trivial. I rejected it because of the interest I had at the time in the immediacy of the ultimate forward proofs. The encoding of multiple goals in a theorem adds an additional layer of cruft to the "expected" proof. Now that I don't care so much about the forward proofs, this would be something to look at again. But I'll probably just go back to the traditional LCF method, which I find generally works quite well. John. ```
 Re: [Hol-info] Rewriting bug in HOL Light? From: John Harrison - 2006-02-06 07:29:22 ```Hi Rob, | If you do it the frozen way as standard, the primitive inferences | involved in doing a typical rewrite don't need to look at the | assumptions of the rewrite theorems at all. Only the rarely needed | THAW does look at assumptions. I agree that in principle this could be more efficient, though whether it makes much of a difference to overall proof times in practice I don't know. Rewriting is certainly a fairly major component of HOL proof, but I don't know how much is taken by the actual matching inference, and how much just by the term traversal, congruences and initial term-net filtering. John. ```
 Re: [Hol-info] Alternative to ckpt? From: John Harrison - 2006-11-21 17:14:36 ```I sympathise with Christopher Conway's problems with "ckpt". It works fine on all my Linux machines, and on the Knoppix disc from ICMS 2006, which has HOL Light images on it: http://geom.math.metro-u.ac.jp/wiki/index.php?KNOPPIX/Math/ICMS2006/English But many people with sligtly different Linux versions have encountered serious problems getting "ckpt" to work. Even ignoring those issues, I haven't found any similarly suitable checkpointing program for Windows or Mac OS X, which makes using HOL Light on those platforms a bit tiresome. Overall, relying on OS-level facilities seems unfortunate. As Rob Arthan notes: | People writing interactive theorem provers seem to be driven to all sorts | of pain because the ML compiler-writing world appears to have forgotten | what ML is best at. A persistent object store for ML code and data provides | a universal solution to this problem, but it is becoming increasinly hard | to find an ML compiler which has a good persistent object store. Jason Hickey and others in the Mojave project did develop a way of saving and restoring the OCaml heap. I'm planning to investigate whether this is applicable to HOL Light sessions. John. ```