gmane.comp.mathematics.axiom.user

Re: A question about Axiom capabilities

Eugene Surowitz — 2013-04-08T14:49:41

Doing it by hand is highly prone to errors and more importantly omissions.

I've experimenting with some code on the Axiom interpreter code as a guinea pig,
before running through all the text of Axiom, to generate a full tokenary.
The text walker starts with output from the tar-ball and busts all text
into tokens, which can be tunable to sub-language.

Or putting it another way: Where is "integrate" everywhere?

Cheers, Gene


On 4/6/2013 4:52 PM, u1204 wrote:

Re: [open-axiom-devel] A question about Axiomcapabilities

Martin Baker — 2013-04-08T15:46:27

OK, As an experiment I created a diagram using a simple graphical editor 
(Inkscape) just to start thinking about layout and level-of-detail 
issues. This is a very tiny subset of the category structure but do you 
think it is enough to draw any conclusions about what would be useful?

The diagram is on this page:
http://www.euclideanspace.com/maths/standards/program/axiomsInAxiom/

Also, on this page, I have tried to gather together some of the 
interesting information that has come from this thread. Hopefully, if it 
were expanded and corrected it may find its way into more official 
documentation, tutorials and wikis.

Martin

Re: A question about Axiom capabilities

u1204 — 2013-04-06T21:45:54

AXIOM CATEGORY/DOMAIN GRAPH:

Axiom is working on creating a new web-based front end based on the
AXSERV domain. The static hyperdoc pages are being converted (Book
Volume 11: Axiom Browser). AJAX is used for the dynamic pages to
pass equations and display results. 

Eventually the Axiom graphics will be converted to work on an HTML
canvas. I've done some minimal experiments with the HTML canvas so
I have some clue about what we need to write to port Axiom's graphics.

I'd recommend that you consider either a graph that can be drawn on
an HTML canvas or creating SVG files which a browser can read. That 
way your work would fit into the long term goals and be easy to 
pick up.


AXIOM BROWSER:

Alternatively you could pick up the whole browser effort and maintain
volume 11 as well as the AXSERV domain. The short term goal is to 
replace hyperdoc yet preserve all of the current functionality.

You can run the pages standalone (without running Axiom). Suppose
your $AXIOM variable is set to /here/test/mnt/ubunt

Re: A question about Axiom capabilities

u1204 — 2013-04-06T20:52:56

The graph is very large. All of the information to create the graph
exists in static files (the algebra Makefile and the bookvol10* files).

It would be useful to be able to create portions of the graph
dynamically. Some of the functionality exists in the API domain
(ApplicationProgramInterface), such as getAncestors and getDomains.
Any other functionality is just as easy to add. I'd be happy to help.

In addition, it would be useful to be able to graph some information
related to functions. Where are all of the "integrate" functions and
how are they related? Or to know about a domain by showing the locally
defined functions and the tree of parents whose functions it inherits.

From a given domain it would be useful to create portions of the graph
of a given distance around the domain. So you could ask for a small
graph of categories and make the limit distance of 3. If the output
was in some standard format (e.g. dot files, html, etc.) it could be
used as input to graph drawing programs.

This is a reasona

Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

Martin Baker — 2013-04-05T10:11:04

I was thinking of something like CASL:
http://www.informatik.uni-bremen.de/cofi/wiki/index.php/CASL
I realise that its purpose is different to a category in Axiom but it 
does at least show how the semantics as well as the syntax of a category 
could be encoded in a well defined language.

Even if it were not possible to use this 'semantic' information for 
enforcing axioms or equation solvers it would be good to have it for 
documentation and automatically generating test scripts.


So are you saying that, for practical purposes, it is not even worth 
trying to write an equation solver for a given category/domain in SPAD, 
even for a very simple category?

I realise there is no general algorithm to do this, but I was hoping 
there might have been the possibility of a common 'toolkit' so at least 
every category/domain writer was not totally on their own.

Martin

Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

Ralf Hemmecke — 2013-04-05T09:20:37

Of course, AXIOM can deal with axioms, but the SPAD language does not
include any way to specify axiom (not even Aldor can do this).



For a term rewriting system you basically have to start with the
implementation of a term algebra. The signature would basically tell,
what symbols are allowed. Since LISP is so fitting for a representation
of such a term algebra, it is no surprise that quite a lot of computer
algebra systems were written in LISP.

Then you can add equations (axioms) and a mechanism to reduce a given
term modulo such equations. But there is no general algorithm to
transform a given term modulo such equation into a canonical form. A
"canonical form" does not even exist for every given term rewriting
system. The non-existence of the "eierlegende Wollmilchsau"
(http://de.wikipedia.org/wiki/Eierlegende_Wollmilchsau
http://en.wiktionary.org/wiki/eierlegende_Wollmilchsau) is the reason
why people work on specialized solvers and use special representations
of the respective term algebra to make th

Re: A question about Axiom capabilities

Martin Baker — 2013-04-05T16:05:46

 > Your probably know that OpenAxiom started putting the axioms in AXIOM.
 > See for example:
 >
 > 
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
 >
 > In fact, a couple of years ago, a student of mine did experiments on
 > exploiting these axioms to help code generation and automatic
 > parallelization.  The results were very encouraging (see the
 > yli-sandbox for example.)
 >
 > OpenAxiom is very much committed to get the axioms integrated to the
 > entire type checking and elaboration process.

Gaby,

Thanks, I find this stuff interesting, Its not that I expect it to 
appear in any flavour of Axiom soon (feel free to correct my 
assumptions), its just that I like to know how things work, what can and 
what can't be done.

AFSICS axioms are currently embedded in the inline documentation for the 
category like this:

snippet from:
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
++ Axioms:
++   \spad{associative("+":(%,%)

Re: Abstract Vector Algebra

u1204 — 2013-04-06T06:21:35

The idea of an "assume" facility seems antithetical to the design
of Axiom. It feels more natural to me to create categories and
domains which remain symbolic (e.g. symbolic matrices). If necessary
they could be coerced to definite values at the appropriate time.

I want

  t2:POLY(IndefinteInteger(x)) := x^2+2*x+3
  t3:POLY(IndefinitePositiveInteger(x)) := x^2+2*x+3
  t4:POLY(Complex(IndefiniteInteger(x))) := x^2+2*x+3

and I can choose the appropriate manipulation algorithms based on
the given types following the same rules we now use.

I'd like to be able to say something like:

  A:SymbolicMatrix := [[a b],[c,d]]
  B:SymbolicMatrix := [[e,f],[g,h]]
  t1 := (A*B)^T
                  B^T A^T
  Type:                       Expression(SymbolicMatrix)

and coerce B^T to a matrix domain if I need to see the entries.

Or I can subtype it to SymbolicMatrix(DoubleFloat), do the
manipulations symbolically and then coerce the final result
to Matrix(DoubleFloat).

Done this way, the indefinites (or symbolics) fit na

Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

u1204 — 2013-04-06T04:44:31

Actually, I wrote an NSF proposal to introduce "indeterminate integers".
This would be a first example of a special symbolic domain that would
create "arbitrary integers" rather than actual integers.

This is my approach to the Maple "assume" facility. I want to say that
the uderlying domain is an "indeterminate integer" rather than
"assume x is an integer". This idea seems more in-line with Axiom's
approach to computational mathematics.

I'm working on creating a sort-of "indeterminate matrix" domain based
on a prior question on this list so you can perform operations like

   (A B)^T => B^T A^T

where A and B are "indeterminate matrices".

I will note that the NSF will not fund open source projects.
Science can only occur if you are at a University. Sigh.

Tim Daly

Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

u1204 — 2013-04-06T04:34:20

There is the desire. Axiom has a long term goal of introducing
program-proof technology (either COQ or ACL2). ACL2 runs on the same
lisp as Axiom. The plan is to load it into the Axiom image and make it
support program proofs for spad code.

I do not have the resources to attack this problem yet. I am still
rewriting Axiom into literate form. However, I assure you that it
is in Axiom's long-term goals, somewhere in the "30 year horizon".

Look at http://axiom-developer.org (the Axiom home page) and see
item (f), that's the program-proof goal.

Tim Daly

Re: Abstract Vector Algebra

u1204 — 2013-04-06T06:01:40

Gaby, 


Thanks for the link. Quote from that page:

 "SI^2 envisions vibrant partnerships among academia, government
  laboratories and industry, including international entities, 
  for the development and stewardship of sustainable software
  ..."

Both Open-Axiom (you) and FriCAS (Waldek) are university related
and university supported efforts. Axiom is pure open source with
no affilations.

I'm saying what I said as an almost direct quote from the person
at NSF responsible for the relevant program. And from the person
before that. I tried for several years. I also tried at NIST in
relation to the Mathematical Handbook. I would like to see 
algorithms in the handbook and thought I could find funding there.

The issue seems to be that there needs to be someone who can handle the
receipts. At a University (e.g. CCNY where I used to work) the provost
did that.  Grants to your university fund students.  Open source
projects not associated with a university don't have the required
accounting setup.

I approac

Re: A question about Axiom capabilities

Gabriel Dos Reis — 2013-04-06T02:39:14

We did not get time to convert all the comments into code as is done
for some the new categories and domains in the trunk repository.
For example, from

http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet

you see:

SemiGroupOperatorCategory(T: BasicType): Category ==
  BinaryOperatorCategory T with
    assume associativity ==
      forall(f: %, x: T, y:T, z: T) . f(f(x,y),z) = f(x,f(y,z))

and

MonoidOperatorCategory(T: BasicType): Category ==
  SemiGroupOperatorCategory T with
    neutralValue: % -> T
      ++ \spad{neutralValue f} returns the neutral value of the
      ++ monoid operation \spad{f}.
    assume neutrality ==
      forall(f: %, x: T) .
         f(x, neutralValue f) = x
         f(neutralValue f, x) = x

The general idea is that most of the axioms and properties are
with the operations, not the carrier sets of structures (as currently
done for old domains.)  That entails some redesign of the
category and domain hierarchies.  We didn't get around to finis

Re: Abstract Vector Algebra

Gabriel Dos Reis — 2013-04-06T17:01:52

I do not know what that mean.  Could you clarify?


OpenAxiom uses domain for schematic expressions, e.g. expressions
with "indefinite" variables.  You can't coerce an indefinite variable
into define values.  That would creating values out of void.
The best you can do is to give values to indefinites.


I would find it poor design to have to duplicate domains that way.
Clearly there must be a notion of natural transformation (in the
categorical sense) that allows lifting of operations to the symbolic/indefinite
level -- see the past work with did on OpenAxiom; I seem to remember
I had a long discussion with Bill Page (or Ralf?) on this topic.

Rather, I would use the notion of schematic expressions -- expressions
from well defined arithmetic domains with indefinite variables.  These
expressions follow well typed and well defined arithmetic; they can be evaluated
to definite values if their schematic variables are given values.


In fact, if you do it properly you would notice that you are just
fixing some b

Re: Abstract Vector Algebra

Gabriel Dos Reis — 2013-04-06T16:48:19

NSF's mission

   http://www.nsf.gov/nsf/nsfpubs/straplan/mission.htm

is defined by law.  You would have to make a case that your proposal
fits its mission, e.g. strongly argue the research aspects of it. I do
not claim it is easy.  That also entails that you would have to be very
specific, and make convincing case of intellectual merits and broader
impacts that advance the mission of NSF.

If you go through the list of projects that made it through that
program, you will notice that the vast majority of them are open source.


Also, this is an aside, but I don't think one can convincingly
argue a notion of "pure open source."


I can't comment on that.  Each organization has its own policy
regarding dealing with funding agencies and contracts matters.


I understand.  Working on AXIOM is a full time job.

Re: A question about Axiom capabilities

Martin Baker — 2013-04-06T18:15:29

 > We did not get time to convert all the comments into code as is done
 > for some the new categories and domains in the trunk repository.
 > For example, from
 >
 > 
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet

Is there a way I could help in a pan-Axiom sort of way? For instance, 
would it be any help if I went through these categories and drew a 
diagram of their relationships? I realise diagrams like:
http://www.axiom-developer.org/axiom-website/bookvol10.2full.html
tend to quickly become unwieldy. But if the diagram was limited to pure 
algebras and split into operator and algebra categories, perhaps it 
might be more manageable?

Or, would it be more practical to model it in one of the formal methods 
tools around, such as?
* Formal specification program,
* Formal development program,
* Formal verification program,
* Theorem provers

I have no experience in using any of these programs but, when they came 
up in this thread I did some searches and they appea

Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

Martin Baker — 2013-04-05T08:51:46

Yes that's an interesting question. For an Axiom category to correspond 
to a 'category' in category theory or a 'theory' in universal algebra 
then it should define both the function signatures and the axioms. I get 
the impression that Axiom(the program) attempts to include axioms in 
categories to a limited extent by say: inheriting commutative but this 
would not be complete enough to drive a general equation solver? (and, 
of course, it cannot enforce commutative axiom in domain instances). It 
seems a sight irony that Axiom(the program) does not do much about axioms.

Given that there is no resources (or desire, as far as I can see) to 
change the structure of Axiom then I was wondering, just for specific 
domains where we want a specific equation solver, could we encode the 
axioms in a set of rules in a domain or package? I guess I'm looking for 
a compromise between building this into the Lisp code and writing a 
seperate equation solver in every domain.


Yes, but again I recognise that there are

Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

Ralf Hemmecke — 2013-04-05T00:07:37


I don't quite understand. If you assume myOp1 to be commutative, then
solving equations is quite a different task from when it is
non-commutative. Where would you store all these axioms?

If you mean "equations solver" then that includes also solving for (x,y)
in x + y = 0.

Or suppose your algebra is a ring. Do you want to write a solver for

  7*x^5+y^3*x^4+2 = 0

i.e. finding all pairs (x,y) that fulfil this equation?

Looks like you aim at a general term rewriting system.

Ralf

Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

martin — 2013-03-30T16:53:08

Agreed, but I was thinking more about doing it on a per-domain basis and 
building up gradually.

So we start with a very simple algebra that we want to create a equation 
solver for, for example we might want to create an algebra domain based 
on this category:

MyAlgebra() : Category with
   myOp1 : ($,$) -> $
   myOp2 : ($) -> $

Then create an expression holder that is specific to that algebra:

MyAlgebraExpression() : Exports == Implementation where
   Implementation == add
   Rep := Union(_
          literalTerm : MyAlgebra, _
          variableTerm : Symbol, _
          myOp1Term : Record(left: $, right: $), _
          myOp2Term : $_
          )
   bind : (Symbol,MyAlgebra,$) -> $
   canonicalForm : $ -> $
   decomposeMyOp1 : $ -> ($,$)
   decomposeMyOp2 : $ -> ($)

Then create an equation solver that is also specific to that algebra:

MyAlgebraEquation() : Exports == Implementation where
   Implementation == add
   Rep := Record(left: MyAlgebraExpression, right: MyAlgebraExpression)
   solveFor : (

Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

Martin Baker — 2013-03-30T17:25:45

 > Unless you specify what solver you intend to write, it's probably an
 > unsolvable task to write a general solver that works for all types of
 > algebras.
 >
 > Ralf

Agreed, but I was thinking more about doing it on a per-domain basis and 
building up gradually.

So we start with a very simple algebra that we want to create a equation 
solver for, for example we might want to create an algebra domain based 
on this category:

MyAlgebra() : Category with
   myOp1 : ($,$) -> $
   myOp2 : ($) -> $

Then create an expression holder that is specific to that algebra:

MyAlgebraExpression() : Exports == Implementation where
   Implementation == add
   Rep := Union(_
          literalTerm : MyAlgebra, _
          variableTerm : Symbol, _
          myOp1Term : Record(left: $, right: $), _
          myOp2Term : $_
          )
   bind : (Symbol,MyAlgebra,$) -> $
   canonicalForm : $ -> $
   decomposeMyOp1 : $ -> ($,$)
   decomposeMyOp2 : $ -> ($)

Then create an equation solver that is also specific to that algebra

Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

Ralf Hemmecke — 2013-03-30T12:01:47

Well, would be nice, but think about the following. An algebra, which is
a field. Depending on which equations you want to solve, there is need
for completely different algorithms. Solve (ax+by=c,dx+ey=f) for x and y
or ax^2+bx+c=0 for x.
Add a new operation (diferentiation) making the algebra into a
differential field, there are even more ways to come up with equations.

Unless you specify what solver you intend to write, it's probably an
unsolvable task to write a general solver that works for all types of
algebras.

Ralf

Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

Martin Baker — 2013-03-30T08:37:38

Would anyone object if I ask a slightly wider question on this topic?

It would be really nice if one could write an equation solver for a 
given algebra, I have often wanted to do that and I wonder if there is 
any general advise on this topic for Axiom?

I guess what I am looking for is a way to have variables that represent 
a given algebra element. If I understand correctly variables are built 
in to an Axiom Expression but they are hard coded to be some form of 
number only.

So I'm guessing that, to do this, one would not only need to define an 
algebra but a specific expression (coalgebra) domain to go with it and 
then some sort of rule solving logic?

Martin Baker