Bill Page

Project Euler

The statement at the Project Euler website includes: "Although mathematics will help you arrive at elegant and efficient methods, the use of a computer and programming skills will be required to solve most problems.". So I think the intention is quite clear: mathematical insight mixed with actual computation. Since computers are enormously more powerful now than when this project was first conceived, I suppose you might dispute whether the particular problem set presented actually achieves this goal or not. In any case it seems quite reasonable to assume that at least some of the algebra built-in to Axiom and Aldor libraries is relevant to at least some of these problems.

I think it is interesting to take a look at the "statistics" section of the project web site:

http://projecteuler.net/index.php?sec...

26345 users have submitted 468838 correct solutions ...

In solving these problems a computer algebra system (Magma, Maple, Mathematica, Matlab or Pari/GP) was used by 493 users.

In all 42 different programming languages were used with C/C++ (3322) being the most popular, followed by Python (2482) and Java (1574).

In spite of the difference, I think 493 users of computer algebra systems is actually quite high given the probable number of programmers who are familiar with these systems compared to conventional programming languages. I think it would be great of one day Aldor and Axiom showed up on this list of languages.

	Bill Page

"Pervasive support for dependent types"

In his post: "Should 3+4 = 7?" on
http://lambda-the-ultimate.org/node/2...
Stephen Watt explained the rational for why Vector(3+4) is not equivalent to Vector(7) in Aldor (I agree the same applies to Axiom):

"The other stance that would allow all types to be treated completely uniformly would be to have all type expressions fully evaluate at compile time. I believe this would lead to worse problems however in the Aldor setting. With the heavy use of mutually recursive and dependent types in the library, we could not have separate compilation with static type checking."

So this is not so much a limitation of static type checking as such but rather the way the compiler interacts with the library. The relationship to the definition of equality between types is simply this: that in comparing Vector(3+4) to Vector(7), 3+4 is not evaluated. Syntactically speaking they are not identical and Aldor does not make any attempt to look deeper. So this is a "weaker" sense of equality of types than if the compiler treated '3' and '4' as integers and computed there sum before making the comparison.

Treating an type expression "Vector(n+1)" as a constructor with n a parameter is certainly possible.

	Bill Page

@David Casperson: David,

I would like to recall something that you wrote on Thu, Apr 3, 2008 at 1:33 PM (in part):

I think that a far more fundamental question is "what is the relationship between the object- and the meta-language?" In this
case the meta-language is Aldor in which we express ideas and
algorithms about mathematics of interest.

As category theory is very expressive it is tempting to view all mathematics as applied category theory and say that the objects that we want to talk about: rings, Lie algebras, etc., are categories. That would make category theory the object
language. This doesn't necessarily imply anything about the meta-language, except that it ought to be able to manipulate the things of the object language easily.
...
Translated back into Aldor, the category theoretic constructions
that we want to talk about need not necessarily be the category
theoretic constructs that we want to use to talk about category theory.

------

I think you are absolutely correct to raise this issue. Why indeed should we attempt to design a language like Aldor at all? Afterall, in the final analysis all programming languages are essentially equally expressive - they all are (in principle) Turing-complete. So there is nothing we can do in one that we cannot (in principle) do in another.

I think the answer has to do with the expressiveness of the language. That is, how efficiently can we express the ideas (programs) that we need to express? It seems very likely to me that the most efficient language for this purpose is the metalanguage itself (otherwise it seems likely that if a more expressive language existed, mathematics would quickly adopt it).

So the closer our object language is to our metalanguage, the more "expressive" it is. It seems that the only thing that might prevent us from achieving this optimum is that the meta-language is not in general be entirely computable (or else it is in some essential respect inconsistent).

But category theory itself appears to have some kind of universal applicability. So I wonder if you would agree that in spite of having "translated back into Aldor" as you said above, that we can (and should) remain in category in so much as the formal semantics of Aldor can be specified in categorical terms?

I wonder however exactly what cateogory theory is most appropriate to describe such a programming language? One possible answer I think is topos theory - or by another name: algebraic set theory. Choosing this as the basis for the underlying semantics of the Aldor language would have numerous implications.

Bill.

	William Sit

blog on Axiom

Thanks. I was more interested in the tesseract, and I left some comments there. http://amca01.wordpress.com/2008/05/1...

Also the wordpress.com site seems notorious for poor security:
http://en.wikipedia.org/wiki/WordPres...

For example (second item with Google search on "silent h article Safire" (no quotes). The third last item from this second link:
http://209.85.215.104/search?q=cache:HvGMLkQBlasJ:es.wordpress.com/tag/william-safire/+silent+h+article+Safire&hl=en&ct=clnk&cd=2&gl=us&client=firefox-a
click on "more" of that item.

The page says, in a big header, "Yes, We Can"

William

	Bill Page

Rig

My main motivation for looking at this is a possible re-design of the Axiom library. Many times when I think about the mathematical taxonomy implemented there, I worry that it is too ad hoc. In a computer algebra system it seems to make sense to start with somewhat more mathematical structure than might be typical in pure mathematics.

In Axiom for example we get positive integers as a subdomain of the Integers. And Integers come from God (well, actually Lisp ... :-).

I agree with your comment about the desirability of putting all this in a categorical setting. I rather liked Baez's description of the NNO as the "free rig on one generator", but I do not know how useful this is in a computer algebra system. Although we certainly do want to do this at a higher level, it seems inconvenient to try to build everything in such a pure manner.

In Axiom we already have:

(1) -> )sh AbelianSemiGroup
AbelianSemiGroup is a category constructor
Abbreviation for AbelianSemiGroup is ABELSG

-------------------- Operations ----------------------------
?*? : (PositiveInteger,%) -> %
?+? : (%,%) -> %
?=? : (%,%) -> Boolean
?~=? : (%,%) -> Boolean

-------

AbelianSemiGroup(): Category == SetCategory with
--operations
"+": (%,%) -> %
++ x+y computes the sum of x and y.
"*": (PositiveInteger,%) -> %
++ n*x computes the left-multiplication of x by the positive integer n.
++ This is equivalent to adding x to itself n times.
add
import RepeatedDoubling(%)
if not (% has Ring) then
n:PositiveInteger * x:% == double(n,x)

-------

Perhaps PositiveInteger is (or should be) Axiom's NNO? Is this "repeated doubling" that kind of thing to which you are referring? Of course in the Axiom programming language (SPAD) we do already have iteration (and much more!).

I also think your reference to Topi is right on. Maybe what we need is some formal mathematical structure (such as topos theory) that we can relate quite directly and formally to Axiom at the level of SPAD. Then when we talk (formally) about introducing seemingly simpler structures into the Axiom library (such as rig and ring), we can do so in reference to something like topi. Then perhaps, it would not seem so embarrassing to see PositiveInteger in AbelianSemiGroup...

Regards,
Bill Page.

	Bill Wood

@Bill Page: Sorry not to get back to you sooner; it's been a busy month. My "strategy" for finding out what Aldor is good for is to ask you guys! For example, if you are familiar with the ProjectEuler site, would Aldor be a good language for solving their usual math-intensive programming problems? I've used lisp for most of the problems I've worked, along with the ECLiPSe Prolog+Constraint Logic Programming system and Python for a couple of problems. I gather from recent postings here that some view Aldor as a language to program abstract algebra computations in. What about semi-numeric computation, such as solving congruences or computing with continued fractions? I saw your reference to category theory; has anyone mentioned using Aldor to support some of the reasoning about programs that Haskellers talk about?

Well there's a start. Thanks for giving me the opportunity to ask questions.

-- Bill Wood

	Bill Page

@Oziewicz Zbigniew: Zbigniew, I am very happy now there are at least two people here who claim to know something about category theory! :-) We might wish that Aldor (and computer algebra systems in general) had more direct support for doing categorical computations by at least there is already the beginning of this subject by Saul Youssef:

http://axiom-wiki.newsynthesis.org/SandBoxAldorCategoryTheory

Concerning Frobenius algebra in relativity, I think we must consider first non-commutative algebras. I am not so sure about the Aldor libraries in this regard, but at least Axiom has non-commutative polynomials. There are some simple example calculations here:

http://axiom-wiki.newsynthesis.org/SandBoxNoncommutativePolynomials

Cheers,
Bill Page.

	Bill Page

Registering the Algebraist blog

We are now indexed in Technorati Profile.
(0 comments)

	Bill Page

@Bill Wood: Hello Bill,

Welcome to the Algebraist!

My main motivation for posting this message is the goal of "finding out what Aldor is good for" that you listed as one of your projects. I think that is a very good question. :-) When you have a moment it would be great if you could jot down some notes here (write a blog entry?) about how you intend to find an answer to that question... seriously. It seems to me that developers often do not spend enough time (re-)thinking basic questions like this, so sometimes even to us it seems difficult to answer the question. And it is not so easy to suggest to someone new what path they should follow to find out more about Aldor.

Regards,
Bill Page.

	Bill Page

Re: What Axiom can do for Aldor

---------- Forwarded message ---------- From: Bill Page Date: Fri, Mar 21, 2008 at 5:07 PM Subject: Re: What Axiom can do for Aldor To: William Sit William, With your permission, I would also like to post this entire email to...
(0 comments)

	Bill Page

@William Sit: Hello William,

Thanks for joining in! :-)

One thing that I would really like to discuss here is the relationship between Axiom and Aldor. In particular: What can Axiom do for Aldor? As opposed to the perhaps more obvious question of: What Aldor can offer Axiom users...

What do you think?

[Repeated for the record ... ]

	Bill Page

Please join the network!

I hope you will consider becoming part of an active community to support the development of the Aldor programming language.
(0 comments)