Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorTim_Porter
   • CommentTimeJan 24th 2013
   • (edited Jan 24th 2013)
   • PermaLink
   Author: Tim_Porter
   Format: MarkdownItexI created an entry on [[Larry Lambe]]. I included a link to some (on line) notes of his on Symbolic Computation which includes discussion of the perturbation lemma from homological perturbation theory.

   I created an entry on Larry Lambe. I included a link to some (on line) notes of his on Symbolic Computation which includes discussion of the perturbation lemma from homological perturbation theory.

2. • CommentRowNumber2.
   • CommentAuthorAndrew Stacey
   • CommentTimeJan 24th 2013
   • PermaLink
   Author: Andrew Stacey
   Format: MarkdownItexGiven your recent post on G+ referencing Ivor the Engine, I thought for a moment you were talking about [Larry the Lamb](http://en.wikipedia.org/wiki/Toytown)!

   Given your recent post on G+ referencing Ivor the Engine, I thought for a moment you were talking about Larry the Lamb!

3. • CommentRowNumber3.
   • CommentAuthorTim_Porter
   • CommentTimeJan 24th 2013
   • (edited Jan 24th 2013)
   • PermaLink
   Author: Tim_Porter
   Format: MarkdownItex'I'm only a little mathematician, sir!' (I cannot convey the voice in text. Ah, memories of my childhood.......... Apologies to those of you who did not have the `benefit' of the BBC Radio Children's Hour... I will not give the dates out of respect for my age!) Larry Lambe, the mathematician this time, did some excellent work on Symbolic Computation for IBM some years ago and developed ways of doing calculations using the perturbation lemma in the system Axiom. I wonder if some of that symbolic computation stuff may not be distantly linked with the efforts to do homotopy theory in Coq. Can anyone say if the idea is silly or not?

   ’I’m only a little mathematician, sir!’ (I cannot convey the voice in text. Ah, memories of my childhood………. Apologies to those of you who did not have the ‘benefit’ of the BBC Radio Children’s Hour… I will not give the dates out of respect for my age!)

   Larry Lambe, the mathematician this time, did some excellent work on Symbolic Computation for IBM some years ago and developed ways of doing calculations using the perturbation lemma in the system Axiom. I wonder if some of that symbolic computation stuff may not be distantly linked with the efforts to do homotopy theory in Coq. Can anyone say if the idea is silly or not?

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJan 24th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIn general, it's nontrivial to relate computer calculations with formal proofs. A proof assistant like Coq is also a programming language, so you can "do computations" in it in a verified way; but conversely it can take a lot of work to formalize a proof of correctness of a computer calculation. E.g. the computer calculations involved in the proof of the 4-color theorem were done in 1976, but the proof was only formalized in 2005.

   In general, it’s nontrivial to relate computer calculations with formal proofs. A proof assistant like Coq is also a programming language, so you can “do computations” in it in a verified way; but conversely it can take a lot of work to formalize a proof of correctness of a computer calculation. E.g. the computer calculations involved in the proof of the 4-color theorem were done in 1976, but the proof was only formalized in 2005.

5. • CommentRowNumber5.
   • CommentAuthorTim_Porter
   • CommentTimeJan 24th 2013
   • PermaLink
   Author: Tim_Porter
   Format: MarkdownItexI think my question is really a musing about what Symbolic Computation in Larry's sense is and does.

   I think my question is really a musing about what Symbolic Computation in Larry’s sense is and does.

6. • CommentRowNumber6.
   • CommentAuthorronniegpd
   • CommentTimeJan 25th 2013
   • PermaLink
   Author: ronniegpd
   Format: TextJust to add my 2 bits to the discussion on computation, since I discussed this a lot with Larry, with regard to the system AXIOM. This developed from the system SCRATCHPAD, a 25 year development by IBM, but the version marketed by NAG had all sorts of flaws, and users dropped away. It is now freely available, and I have heard strong expressions of support for it. AXIOM does not verify any axioms. However it uses axioms to give favourable expressions. For example, a normal form for a free abelian group is simpler than that for a free group. AXIOM is strongly typed. So for the symbol "1" you have to say in what mathematical type it is, a positive integer, an integer, rational number, square nxn matrix over a ring, etc. This corresponds to standard informal mathematical usage. Tne type system allows for inheritance, types as first class variables, and coercion. Thus a square matrix of integer polynomials in x may be coerced into a polynomial in x over the ring of square integral matrices. Inheritance implies that you need can implement one algorithm for multiplication in a semigroup, and that can be used for addition and multiplication in rings, say. Types as variables implies you can formulate the type of a monoid ring using the types of monoid and ring, and then use that for polynomials, and Laurent polynomials. A very appealing part of the AXIOM book (to me) was the back and front inside covers, describing the datastructures for the system (e.g. for lists, ...) and for the mathematics. So the value for mathematics was its expressive power. The problem was the cumbersome system, with internal compilers from its own nice SPAD language into LISP and then C, and the fact that NAG when they bought it seem somehow to have mucked up the system, with two compilers; previous users of SCRATCHPAD fell away, but some form of the system has been rescued. Larry Lambe has constructed his own system which he uses in his current work, and which incorporates the values pioneered in SCRATCHPAD. Code from this was used by Gareth Evans, the last PhD student at Bangor, for a thesis under Chris Wensley on noncommutative involutive bases (a variation on Grobner bases). Thus AXIOM does not verify that an algorithm works. However it is intended to supply a language and system in which the algorithm could in principle be expressed, even if that involved say bicategories of divided powers of L-infinity algebras (to make something up). The aim is to model normal and best mathematical practice, and aim for fast and robust computation.

   Just to add my 2 bits to the discussion on computation, since I discussed this a lot with Larry, with regard to the system AXIOM. This developed from the system SCRATCHPAD, a 25 year development by IBM, but the version marketed by NAG had all sorts of flaws, and users dropped away. It is now freely available, and I have heard strong expressions of support for it.
   
   AXIOM does not verify any axioms. However it uses axioms to give favourable expressions. For example, a normal form for a free abelian group is simpler than that for a free group.
   
   AXIOM is strongly typed. So for the symbol "1" you have to say in what mathematical type it is, a positive integer, an integer, rational number, square nxn matrix over a ring, etc. This corresponds to standard informal mathematical usage.
   
   Tne type system allows for inheritance, types as first class variables, and coercion. Thus a square matrix of integer polynomials in x may be coerced into a polynomial in x over the ring of square integral matrices.
   
   Inheritance implies that you need can implement one algorithm for multiplication in a semigroup, and that can be used for addition and multiplication in rings, say.
   
   Types as variables implies you can formulate the type of a monoid ring using the types of monoid and ring, and then use that for polynomials, and Laurent polynomials.
   
   A very appealing part of the AXIOM book (to me) was the back and front inside covers, describing the datastructures for the system (e.g. for lists, ...) and for the mathematics.
   
   So the value for mathematics was its expressive power. The problem was the cumbersome system, with internal compilers from its own nice SPAD language into LISP and then C, and the fact that NAG when they bought it seem somehow to have mucked up the system, with two compilers; previous users of SCRATCHPAD fell away, but some form of the system has been rescued.
   
   Larry Lambe has constructed his own system which he uses in his current work, and which incorporates the values pioneered in SCRATCHPAD. Code from this was used by Gareth Evans, the last PhD student at Bangor, for a thesis under Chris Wensley on noncommutative involutive bases (a variation on Grobner bases).
   
   Thus AXIOM does not verify that an algorithm works. However it is intended to supply a language and system in which the algorithm could in principle be expressed, even if that involved say bicategories of divided powers of L-infinity algebras (to make something up). The aim is to model normal and best mathematical practice, and aim for fast and robust computation.
7. • CommentRowNumber7.
   • CommentAuthorronniegpd
   • CommentTimeJan 25th 2013
   • PermaLink
   Author: ronniegpd
   Format: TextI should add that the THEORY of the type system was not well expressed in the AXIOM book or the additional handouts. There was in mind doubt the "equality" type, especially for functions. Was "type" a "type"? etc. But I did come across a paper claiming to prove coherence of coercion. On the other hand, the aim was not an overarching system for all mathematics, now and in the future, but to build a system which could cope with and express current work, maybe in an old fashioned view of universal algebra (Gratzer rather than Lawvere, or Ehresmann sketches); which could be expanded step by step, and tested at that level; and was fast and robust. (Except that the compiler for AXIOM was slow with the machines we had then, in the mid 1990s!)

   I should add that the THEORY of the type system was not well expressed in the AXIOM book or the additional handouts. There was in mind doubt the "equality" type, especially for functions. Was "type" a "type"? etc. But I did come across a paper claiming to prove coherence of coercion.
   
   On the other hand, the aim was not an overarching system for all mathematics, now and in the future, but to build a system which could cope with and express current work, maybe in an old fashioned view of universal algebra (Gratzer rather than Lawvere, or Ehresmann sketches); which could be expanded step by step, and tested at that level; and was fast and robust. (Except that the compiler for AXIOM was slow with the machines we had then, in the mid 1990s!)
8. • CommentRowNumber8.
   • CommentAuthorronniegpd
   • CommentTimeJan 25th 2013
   • PermaLink
   Author: ronniegpd
   Format: TextLarry tells me the distro he likes is FreCAS http://fricas.sourceforge.net/ , but there are still problems from the old days to overcome. The way I like to see proofs is in terms of landscapes: so when you describe the way to the station you don't give all the cracks in the pavements, though you will warn of men at work! So the way to more certainty is in terms of relevant structure, so that you know it is correct because of the way it all fits together. This is analogous to the way error correction works, by fitting the code to an elaborate and tight structure. It fits with the comment on Grothendieck, that he was prepared to work very hard to make things tautological. Again if we want proof searching, we want the landscape well proscribed. Machines are very good at finding routes through mazes, but the maze must be set at the right "landscape", i.e. structural level, or it will be inefficient, and maybe also non robust. How to do this in a way modelling general mathematical practice, and making it usable for people like me, is a major problem.

   Larry tells me the distro he likes is FreCAS http://fricas.sourceforge.net/ , but there are still problems from the old days to overcome.
   
   The way I like to see proofs is in terms of landscapes: so when you describe the way to the station you don't give all the cracks in the pavements, though you will warn of men at work! So the way to more certainty is in terms of relevant structure, so that you know it is correct because of the way it all fits together. This is analogous to the way error correction works, by fitting the code to an elaborate and tight structure. It fits with the comment on Grothendieck, that he was prepared to work very hard to make things tautological.
   
   Again if we want proof searching, we want the landscape well proscribed. Machines are very good at finding routes through mazes, but the maze must be set at the right "landscape", i.e. structural level, or it will be inefficient, and maybe also non robust. How to do this in a way modelling general mathematical practice, and making it usable for people like me, is a major problem.
9. • CommentRowNumber9.
   • CommentAuthorjim_stasheff
   • CommentTimeJan 25th 2013
   • PermaLink
   Author: jim_stasheff
   Format: Text@ronnie The way I like to see proofs is in terms of landscapes: so when you describe the way to the station you don't give all the cracks in the pavements, though you will warn of men at work! spot on indeeed!

   @ronnie
   The way I like to see proofs is in terms of landscapes: so when you describe the way to the station you don't give all the cracks in the pavements, though you will warn of men at work!
   
   spot on indeeed!