Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTim_Porter
    • CommentTimeJan 24th 2013
    • (edited Jan 24th 2013)

    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.

    • CommentRowNumber2.
    • CommentAuthorAndrew Stacey
    • CommentTimeJan 24th 2013

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

    • CommentRowNumber3.
    • CommentAuthorTim_Porter
    • CommentTimeJan 24th 2013
    • (edited Jan 24th 2013)

    ’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?

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJan 24th 2013

    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.

    • CommentRowNumber5.
    • CommentAuthorTim_Porter
    • CommentTimeJan 24th 2013

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

    • CommentRowNumber6.
    • CommentAuthorronniegpd
    • CommentTimeJan 25th 2013
    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.
    • CommentRowNumber7.
    • CommentAuthorronniegpd
    • CommentTimeJan 25th 2013
    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!)
    • CommentRowNumber8.
    • CommentAuthorronniegpd
    • CommentTimeJan 25th 2013
    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.
    • CommentRowNumber9.
    • CommentAuthorjim_stasheff
    • CommentTimeJan 25th 2013
    @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!