Home

Calculemus 2005

via OCaml

The Calculemus 2005 Symposium on July 18-19, 2005 will explore the mission of the Calculemus project:

The scientific and technological goal...is the design of a new generation of mathematical software systems and computer-aided verification tools based on the integration of the deduction and the computational power of Deduction Systems and Computer Algebra Systems respectively.

Both Deduction Systems and Computer Algebra Systems are receiving growing attention from industry and academia. On the one hand, Mathematical Software Systems have been commercially very successful in recent years....On the other hand, the use of formal methods in hardware and software development has made Deduction Systems indispensable not least because of the complexity and sheer size of the reasoning tasks involved.

In spite of these successes there is still need for improvement as many application domains still fall outside the scope of existing Deduction Systems and Computer Algebra Systems. For instance, the scope of Computer Algebra Systems (CASs) could be significantly enhanced by adding deductive reasoning power. In fact this lack of expressivity together with the unsolved problem of correctness prohibit large classes of applications. Deduction systems (DSs), which - on the other hand - provide such an expressivity, as well as the guarantee of correctness, still lack computational power as they are not suited to directly carry out algebraic or numerical calculations. This severely restricts their scope of application in mathematics and - more importantly - in engineering applications.

Earlier we discussed the Axiom CAS.

By Mark Evans at 2004-11-17 01:14 | DSL | other blogs | 8385 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Programming Language aspects of CASes

A part of my own interest in Calculemus has to do with the (programming) language semantics of computer algbebra systems. The interesting item to note (for this list anyways) is that all 'popular' CASes are dynamically typed. Axiom, linked above, and its underlying programming language, Aldor are exceptional, in that they are partly statically typed. But since Aldor has dependent types as well as first-class types, this means that there must be run-time representations of types, and that is rather against the grain of current statically typed languages. Even so, Axiom and Aldor were not able to do the one thing that users of the commercial packages want to do: analysis. I mean integrate, solve non-linear equations, deal with differential equations, manipulate expressions-as-functions, and so on. Somehow the type discipline allowed one to deal with algebra well enough (and only via dependent types, as the Automath people already knew, and the MetaPRL people seem to be re-learning), but completely failed on analysis. Theorems in analysis can be handled in type theory well-enough (ie the other half of Calculemus), but somehow computations in analysis have not yielded to the type-theoretic onslaught - yet.

In any case, CASes like Maple, Mathematica and MuPAD all have very interesting programming languages, all of which contain semantics that do not currently 'fit' the mold of any current theory of programming languages. I am actively working on writing some of this up. CASes are not alone in having these hard-to-explain semantics: LISP's various quotes (and what you can do with them) is still rather under-explained [MetaOCaml and Template Haskell only explain a small part]. If there is sufficient interest, I may try to post the simplest examples of unexplained semantics of CASes.

Be that as it may, as co-chair of Calculemus 2005, I would very much welcome any papers on the programming language aspects of CASes and theorem proving systems.

By Jacques Carette at Wed, 2004-11-17 03:35 | login or register to post comments

Axiom and mathematical analysis

I wonder what Jacques Carette meant by this comment?

Even so, Axiom and Aldor were not able to do the one
thing that users of the commercial packages want to do:
analysis. I mean integrate, solve non-linear equations,
deal with differential equations, manipulate
expressions-as-functions, and so on.

Axiom does very clearly provide facilities to "integrate, solve non-linear equations,deal with
differential equations, manipulate
expressions-as-functions".

Reference:
http://page.axiom-developer.org/zope/mathaction/AxiomDocumentationAndCommunity

By billpage at Wed, 2005-03-09 22:21 | login or register to post comments

On Axiom

First, the link you have given above seems broken.

Second, it appears my comment reflects my dated view of Axiom which did not use to have such facilities when I last looked at it. It is nice to see that this has changed.

By Jacques Carette at Thu, 2006-06-08 13:48 | login or register to post comments

I would be fascinated by anyt

I would be fascinated by anything you write -- the type-theoretic approach is so powerful that learning where there are difficulties would be very very interesting!

By neelk at Thu, 2004-11-18 21:38 | login or register to post comments

Ditto

That's why LtU is here. Feel free.

By Mark Evans at Wed, 2004-11-24 01:49 | login or register to post comments

CAS and type theory

OK, I will definitely get back to this, on LtU. This week I am completely swamped, but next week is looking much better.

One quick (cryptic) example: the same difficulties in being able to express partial evaluation in a typed setting occurs in a CAS. Of course I mean to have a partial evaluator written in a language X for language X, and have the partial evaluator 'never go wrong'. Cheating by encoding language X as an algebraic datastructure in X is counter-productive as it entails huge amounts of useless reflection/reification. One really wants to be able to deal with object-level terms simply and directly. But of course, that way lies the land of paradoxes (in set theory, type theory, logic)!

And while I am at it: consider symbolic differentiation. If I call that 'function' diff, and have things like diff(sin(x),x) == cos(x), what is the type of diff? More interestingly, what if I have
D(\x -> sin(x) ) == \x -> cos(x)
What is the type of D ? Is it implementable in Ocaml or Haskell? [Answer: as far as I know, it is not. But that is because as far as I can tell, D can't even exist in System F. You can't have something like D operating on opaque lambda terms.]. But both Maple and Mathematica can. And I can write that in LISP or Scheme too.

By Jacques Carette at Wed, 2004-11-24 04:01 | login or register to post comments

what is the type of diff?

In Axiom the function name 'differentiate' is
overloaded. In the case

differentiate(sin(x),x)

the type of 'differentiate' is

(Expression Integer,Symbol) -> Expression Integer

'Expression Integer' is the domain of general
expressions with Integer coefficients.
'differentiate' is defined in the Axion category
'FunctionSpace(Integer)' to
which 'Expression Integer' belongs.

In general the type associated with
'differentiate(...,x)' is given by the category
'PartialDifferentialRing(Symbol)' to which
'FunctionSpace(Integer)' belongs by the dependent
signature

(D,D1) -> D from D if D has PDRING D1 and D1 has SETCAT

where PDRING is an abbreviation for
PartialDifferentialRing and Symbol belongs to SETCAT.

I would like to invite you to discuss the Axiom
Language in more detail (complete with online code
examples) at:

http://page.axiom-developer.org/zope/mathaction/AxiomLanguage

By billpage at Thu, 2005-03-10 04:06 | login or register to post comments

Type 'Expression' is not a "type"!

The type constructor 'Expression' is a syntactic type - it represents trees with particular leaves. Unlike almost all other types in Axiom, it is not a semantic type.

Also, it surprises me that FunctionSpace(Integer) is a PDRING - this would imply that (all?) expressions that you can write down from Expression Integer are differentiable, which is clearly false. In fact, not all things that belong to Expression Integer are even meaningful! One simple example is 1/(1/(x-x)). If Axiom insists on normalizing that right away, then try 1/(1/((x+y)^2- (x^2+2*x*y+y^2)).

Note that this is exactly the same quagmire that other CASes (Maple, Mathematica, MuPAD, macsyma, etc) have gotten themselves into by defining everything syntactically. Axiom was doing better up until the point where Expression was created, since that type is isomorphic to the ``type'' of all objects in the other CASes.

Thanks for the link above - the corresponding page is a very nice read. While there, LtU members should really sign the Free Aldor petition.

By Jacques Carette at Thu, 2006-06-08 14:03 | login or register to post comments

Calculemus 2006

Some LtU members might be interested in some of the papers at this year's Calculemus.

By Jacques Carette at Thu, 2006-06-08 13:38 | login or register to post comments

Calculemus 2009

The call for papers for the next edition of this conference has just gone out. There are quite a number of PL issues that overlap significantly with what Calculemus is all about.

By Jacques Carette at Wed, 2009-01-07 18:19 | login or register to post comments