Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
Given your recent post on G+ referencing Ivor the Engine, I thought for a moment you were talking about Larry the Lamb!
’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?
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.
I think my question is really a musing about what Symbolic Computation in Larry’s sense is and does.
1 to 9 of 9