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/ubuntu. In your
browser you can open the page:
file:///here/test/mnt/ubuntu/doc/hypertex/rootpage.xhtml
and see the current state of the world. Visit

Reference -> Topics -> Numbers -> Integers 

and you will see a page from hyperdoc. If Axiom is connected and running
in the background the equations can be clicked on and the results
returned to the browser.

I am currently rewriting the "basic commands" code for hyperdoc
which is in lisp. It implements an html-like language with extensions
for inline latex (Scott Morrison is a very clever fellow and was WAY
ahead of his time.) I'm documenting it as I rewrite it so I know 
what to change for the browser functionality. This rewrite will
be the next patch released.

The longer term goal is to make an Axiom "appliance server" which
will be completely browser-driven so it can be used in a classroom
or network setting.

Tim Daly

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 reasonably straightforward problem and would get you more
familiar with Axiom's hierarchy as well as writing code.

Some of this functionality can be embedded into latex documents which
would make them much more useful. Currently the big graph contains
links to the source code in the books. There are mini-graphs in the
books but the links are not (yet) part of the graphs. It would be
useful to click on the pictures in the book and move to, say, a
parent category's source code.

Tim Daly

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 things fast.

Ralf

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("+":(%,%)->%)}\tab{30}\spad{ (x+y)+z = x+(y+z) }
++   \spad{commutative("+":(%,%)->%)}\tab{30}\spad{ x+y = y+x }
AbelianSemiGroup(): Category == SetCategory with

I had a rummage about in the sandbox you mentioned (written by Yueli 
about 3 years ago) and I did not come across any overall tutorial file 
(what I would think of as top level documentation) I may have missed it. 
Did Yueli write any thesis or anything like that?

At first glance it does look encouraging as the code to analyse the code 
does seems to be written in SPAD, which hopefully shows that it can be 
done. When I look at the code (such as snippet below) it looks like the 
axioms are coded differently, that is on a per operator basis?

snippet from:
http://sourceforge.net/apps/trac/open-axiom/browser/yli-sandbox/contrib/redec/operatorcats.spad?rev=2776
)abbrev category ASSOCOP AssociativeOperator
   ++ Axiom: associativity: rule op(a, op(b, c)) == op(op(a,b), c)
   AssociativeOperator(T: SetCategory, op: Mapping(T, T, T)):Category
     == MagmaOperator(T, op)

Any further clues for understanding the code appreciated, thanks,

Martin

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 naturally into
the mathematical structure of Axiom. There is probably even some
category theory support for lifting operations (arrows) to 
symbolic form.

Tim Daly

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 approached IBM (where I used to work) with the suggestion that they
set up a very small (e.g. 2 person) "open source support" organization,
not specifically related to Axiom, which had the job of receiving the
NSF grant money and handling receipts. The accountants would be paid out
of the grant money, similar to the way the provost took over 50% of my
grant for "overhead". I also approached Texas Instruments and Hewlett
Packard. I suppose I should have approached Google but my frustration
level just got too high.

This isn't money for programming. It would be grant money to have
conferences, travel expenses, website support, and code sprints. 
The only direct cash payments would go to summer-of-code-like projects.

It is much more costly but way less frustrating to just fund it myself.

Tim Daly

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 finish
the conversion; plus Yue  is no longer working in this area.


unfortunately, no.  What I have are internal reports we didn't to put
in shape that is publishable, even as technical reports.


Yes, most of the code was written in Spad; some hooks into the parser was
needed, but the elaboration, and the whole static analysis is written in Spad.

(By the way, I used OpenAxiom in 2006 and 2008 for static analysis and
compiler courses so, there was precedent for writing the "compiler stuff" in
Spad.  Some improvements were needed to make the whole experience palatable
though -- for example, that is why we have a Syntax domain, some form of
pattern matching, user-defined case operator, existential type, etc.)


Yes, I explained above many properties are with the operators, not the
carrier set -- Integer can be the carrier set for many monoidal structures.


The main trunk has the axioms integrated in codes.  One of the reasons why
Yue used the old commentary style to write some of the axioms is that he
needed to analyse the entire algebra set (which he did), but he did
not have the time
to redesign the entire algebra hierarchy.  After the positive
preliminary reports,
we headed for getting some results out (see the ISSAC 2011 paper); and
after that
he changed fields of studies.

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 bugs in the Expression domain and you do not need
Symbolic anything :-)   At least, that was my final conclusion when
I worked on this for many years.


Yes, but I don't see where that contradicts the notion of "assume".

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 appear to be very 
powerful (I guess their limitations only become clear with experience)?
At first glance CASL appears very powerful for axioms.

quote from wiki page here.
http://en.wikipedia.org/wiki/Specification_language
"In the property-oriented approach to specification (taken e.g. by 
CASL), specifications of programs consist mainly of logical axioms, 
usually in a logical system in which equality has a prominent role, 
describing the properties that the functions are required to satisfy - 
often just by their interrelationship. This is in contrast to so-called 
model-oriented specification in frameworks like VDM and Z, which consist 
of a simple realization of the required behaviour."

So, if I understand correctly:
CASL is good at theories (axiom categories).
ACL2 is good at models of those theories (axiom domains).
(or by Curry–Howard: proofs)

I have not yet seen a program that is good at both.

I get the impression that ACL2, after a very quick search on the web (so 
I may be wrong), does term rewriting and proofs but its input is not 
axioms but some sort of state machine defined in LISP? (I have not seen 
the light regarding LISP, but let not have that debate!).

So I just wondered if anyone has had experience with any of these 
'formal methods tools' and would there be any benefit in my attempting 
to learn one? (to experiment with specifying axioms or to experiment 
with term rewriting systems).

Or would it be best to wait (hopefully not for the full 30 years) until 
you guys implement more of this stuff?

Martin

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 no resources, so I was 
wondering if it would be possible to start with a very simple domain 
(not a field, something really simple, which is what I was trying to 
indicate in the psudocode in my last message). Then abstract out a rule 
engine. Then gradually build it up over time so that it could cope with 
more complex domains.

This is probably not very practical, but I was just trying to do a 
thought experiment to investigate what would be required to have 
variables that range over domains that are not numbers.

Martin

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 : (Symbol,$) -> MyAlgebraExpression

This would require 3 domains for every algebra that we wanted to be able 
to solve but why not have some separate common rule interpreter code. So 
MyAlgebraEquation domain would consist mostly of a set of substitution 
rules for that particular algebra?

Martin

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:

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

This would require 3 domains for every algebra that we wanted to be able 
to solve but why not have some separate common rule interpreter code. So 
MyAlgebraEquation domain would consist mostly of a set of substitution 
rules for that particular algebra?

Martin

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