Tim,
Thanks for your reply, lots to think about in this subject isn't there.
Like you I'm attempting the daunting (but interesting) path of trying to
understand this subject better.
Dependent types allow functions to exist in the type definition. The
functions can be executed "at run time".
Tim
In this series of videos Robert Harper gives an provocative take on
these subjects:
https://www.youtube.com/watch?v=LE0SSLizYUI
At about 37 min into this video he says: "what is true has unbounded
quantifier complexity whereas any formalism is always relentlessly
recursively
Tim,
Would this also be compatible with 'propositions as types' as in Idris
and various proof assistants? That is, could you have both Curry–Howard
and Carette-Farmer?
I ask this because types (and constructors for types) could also be
inherited by categories in the way you describe. So an
ppose that's all you need in order to write a program that
simplifies equations inside the type context?
-- Henri Tuhola
On Sat, 21 Sep 2019 at 11:50, Martin Baker wrote:
I'm a fan of both Axiom and Idris. I think my ideal would be Axiom
mathematics build on top of the Idris type system.
Th
On 21/09/2019 13:40, Henri Tuhola wrote:
The elaborator reflection also allows accessing the term rewriting. I
suppose that's all you need in order to write a program that
simplifies equations inside the type context?
I am trying to understand if these equations could be solved in this way?
I
I'm a fan of both Axiom and Idris. I think my ideal would be Axiom
mathematics build on top of the Idris type system.
The Axiom type system was incredibly advanced for its time but I suspect
the Idris type system has finally caught up and overtaken it? Correct me
if I'm wrong but I think the
Tim,
This all seems to be about the lisp layer, obviously thats what
interests you.
It seems to me that if SPAD code is complicated and not aligned to type
theory then, when SPAD is complied to Lisp, the List code will be
complicated and hard to work with. Your previous remarks, about not
evel. Think
of it as a PhD thesis project without the degree incentive :-)
Tim
On 6/25/19, Martin Baker wrote:
On 6/25/19, William Sit wrote:
> The expression x = x + 0, whether treated as a type or an equation,
> can only make sense when x, =, + and 0 are clearly typed and defined.
>
On 6/25/19, William Sit wrote:
> The expression x = x + 0, whether treated as a type or an equation,
> can only make sense when x, =, + and 0 are clearly typed and defined.
> It makes little sense to me that this, as an equation, can be "proved"
> to be valid universally (that is, without the
On 19/06/2019 12:18, Tim Daly wrote:
The effort to
Prove Axiom Sane involves merging computer algebra and proof
technology so Axiom's algorithms have associated proofs.
Tim,
Are there some fundamental compromises that have to be made when
combining computer algebra and proof technology?
Tim,
I've been experimenting with a language called 'Idris'. I've been
playing around with writing some of the Axiom SPAD library code in
Idris. My code so far is here:
https://github.com/martinbaker/Idris-dev/tree/algebra/libs/algebra
Nothing usable yet, I'm just experimenting with whats
On 04/11/17 00:42, Tim Daly wrote:
How would you model handling errors in Spad?
I do think that there might be an interesting research question of how to
handle classes of errors in computational mathematics. I had proposed
using Provisos to handle side-conditions on formulas. Hoon Hong and
On 04/11/17 16:18, Tim Daly wrote:
You're correct. My primary focus is on Spad code.
Tim,
Thanks for the explanation, interesting stuff, I'll be keen to read any
progress reports if you get time to write them.
Thanks, Martin B
___
On 04/11/17 00:42, Tim Daly wrote:
On the other hand, my current effort involves proving Axiom correct. That
should (in theory) eliminate whole classes of errors. This is at the expense
of proving new code correct which tends to get a negative reaction from
developers.
Tim,
I know little
On 02/11/17 21:10, Tim Daly wrote:
Another thought... While people don't seem to like lisp as a platform
it does have major advantages. I usually find myself using the lisp
debugging facilities (trace, break, and REPL evaluation) to find
out what failed and where.
If you go from Spad to
Tim,
Just a small documentation issue.
This line appears to be duplicated in the PDF:
"Permutation is a domain which can be used to compute permutations. It
is also an implementation of Group category."
In books/bookvol10.3.pamphlet its at line 145509.
I assume you would prefer me to let you
On 31/03/17 05:34, Tim Daly wrote:
Consider the Axiom Domain NonNegativeInteger. NNI roughly
corresponds to the Type theory "Nat" construction. They differ
in that Axiom uses Lisp Integers whereas Type theory uses
Peano arithmetic (a zero and a successor function) but for
our purposes this does
On 08/12/16 18:03, Tim Daly wrote:
So the real question might be "Can I formulate my physics in
matrix and tensors and shift between them". Which leads to the
question "Can I easily convert between matrices and tensors?"
From what I've seen so far this should be possible, provided it is
Tim,
You recently mentioned Clifford Algebra a couple of times so I thought I
would mention an idea that I had on the subject. The idea is still too
vague and hand-wavy to turn into code but I would be interested to know
if anyone thinks its viable?
The idea is to implement a 3-layer
On 27/07/15 11:22, d...@axiom-developer.org wrote:
3) Some categories could have exactly the same signatures but differ
only in their axioms.
Can you give me an idea of where this might happen?
This isn't an obvious case.
Well I was thinking of something like AbelianGroup vs. Group but
On 26/07/15 20:27, d...@axiom-developer.org wrote:
Martin,
I like the idea of specific mathematical axiom markup as a first
cut. I will try this idea.
There is a distinction to be made between mathematical AXIOMS for
the category (e.g. associative) and SIGNATURES for the functions
in a
On 25/07/15 12:38, d...@axiom-developer.org wrote:
Axiom has moved into a new phase. The goal is to prove Axiom correct.
Tim,
Why not do the easy bit first and just mark up the operators, in
domains, with the following common Axioms/Identities?
Only for functions with signature:
On 08/05/15 21:40, d...@axiom-developer.org wrote:
There exists a few mathematical axiom statements in the category book
(Volume 10.2), associated with each category (look at SemiGroup for
example). The intention is to decorate all of the categories and
domains with mathematical axioms which can
On 08/05/15 10:02, d...@axiom-developer.org wrote:
Axiom Volume 13 is the start of the pile. If you find any papers
or articles that might be of interest to the goal, please let me know.
Tim,
I am currently reading Nipkow/Klien [1] just to get a top level view of
the subject (I have not
On 06/03/15 11:32, d...@axiom-developer.org wrote:
Have you seen Visual Complex Analysis by Tristan Needham?
Yes, I agree that there are a lot of examples in there which show how
visualisation helps people get a better understanding of the
mathematics. Also I think this type of mathematics
It is vital that we make the strong connection between group theory
and Spad completely transparent. People need to have a presentation
that makes it easy to move between group theory and Spad.
There is a book, which I like, called 'Visual Group Theory' [Nathen
Carter, 2009]. This looks at the
Tim,
Thank you for the interesting post about Axiom design and use of lisp.
I wondered if you ever considered Clojure?
I have very little practical experience of Lisp, so please forgive my
ignorance but, I get the impression that Clojure has better type checking?
Also use of JVM means it
Tim,
Yes, I think it would be really good if Axiom could live up to its name
and include axioms.
It seems to me that categories in Axiom are mostly about function
signatures (I know I'm vastly oversimplifying here) but they would be
more like the mathematical concepts they represent if they
Tim,
The link you gave:
http://www.youtube.com/watch?v=D1cKI2jsidc
did not work on my computer, I think it should be:
http://www.youtube.com/watch?v=D1cKI2jsldc
Martin
___
Axiom-developer mailing list
Axiom-developer@nongnu.org
On 11/05/14 21:33, Tim Daly wrote:
Unless there is some overarching reason it is hard to see the need to
rewrite existing code. A new design that regularizes many domains
might make a good reason. A complete extension of the whole area, such
as a major matrix package might make DHMATRIX a
On 09/05/14 18:16, Tim Daly wrote:
With respect to documentation of open source software...
You keep using that word. I don't think it means what you think it
means. -- The Princess Bride
The notion that reading the code is the ultimate truth for
documentation is based on a misunderstanding at
On 17/11/13 18:28, d...@axiom-developer.org wrote:
This is interesting. I'm trying to incorporate it into the
new Axiom browser-based front end. However, anyone doing
literate programs in mathematics will find it useful.
http://latex2html5.com
Tim,
Yes it does look interesting. Looking at
Does the code have to be physically in the same document as the documentation
to achieve the aims of literate programming?
The analogy that I would make is with graphics in html, these are stored in
their own files so we can edit a .gif file or a .jpeg file or .png or .svg and
so on each with
On Friday 20 Jan 2012 11:59:52 Ralf Hemmecke wrote:
It all depends on your tools. If there were a tool that puts every code
chunk into a separate file but while editing shows you the chunks in the
order you want, you wouldn't care how your content is physically stored.
Its just that the method
On Friday 20 Jan 2012 15:59:15 you wrote:
How hard is this? It could hardly be easier. Send the single
pamphlet file to another user and they have everything.
Tim,
Perhaps I'm too set in my ways or perhaps I'm missing something but I think we
are going to have to agree to disagree on this
Tim,
One issue that occurred to me on this subject. It seems to me the point of
HTML and hypertext is that they are not a linear book. What I like about this
is that the reader can start at a high level with a small and concise page but
they can drill down to any level of detail they may need.
If you feel that interleaving videos, animations, navigation, and any
other tricks improves the independence test results then these
techniques should be used. If, however, you are just trying to
organize the material by some random criteria (e.g. alphabetical
or as trees of logically grouped
Documentation and comment systems are not like this. They make the
program organization fit the machine. They talk about the code, and
focus on line-by-line or file-by-file. They tend to work well with all
kinds of tools like Eclipse, Javadoc, or Doxygen.
I tend think of this as reference
Frustrated at the minimal documentation for the Kernel domain I have attempted
to start documenting it myself here:
https://github.com/martinbaker/fricas/blob/master/src/algebra/kl.spad.pamphlet
I have added lines: 216:272
I don't consider myself an expert on this subject but perhaps its
On Sunday 16 Oct 2011 21:27:41 Ralf Hemmecke wrote:
Better it is free and there is a little chance that some day someone
picks it up) than non-free and unmaintained.
I don't understand the technical issues and I agree that, in most cases,
choice is a good thing.
However, in the case of
On Wednesday 17 Aug 2011 05:24:41 d...@axiom-developer.org wrote:
It seems that the Category Theory discussion has come around again on the
great wheel of life. These talks might be helpful for those who are lost.
part 1: http://vimeo.com/17207564
part 2:
I have written an alternative geometry/graphics framework.
I have put links to the code and documentation at the bottom of this
page here:
http://www.euclideanspace.com/maths/standards/program/mycode/graph/
It is based on a scenegraph structure which allows
lines, surfaces and higher dimensional
passed the local build server checks.
Silver sources live on:
sourceforge.net/projects/axiom
savannah.nongnu.org/projects/axiom
axiom-developer.org
axiom-developer.com
axiom-developer.net
Axiom Gold version is at github. Gold is updated every 2 months.
Tim
Martin Baker wrote:
Tim
?p=1baseproject=ALLq=open-axiom
this automatically generates rpms not only for SuSE but also for Fedora,
Mandriva, etc.
Unfortunately I don't have any skills or knowledge in doing this otherwise I
would offer to help.
Martin Baker
___
Axiom
,
Martin Baker
___
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
structures in axiom to
implement Open Inventor (IVNodeCategory, RenderTools, IVSimpleInnerNode,
IVSeparator, IVGroup, IVCoordinate3, IVQuadMesh, IVIndexedLineSet,
IVUtilities). Would it be feasible to adapt this to support X3D?
Martin Baker
___
Axiom
to add it to the
codebase.
Martin Baker
___
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
into the formula
using buttons on the web page?
Martin Baker
___
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
they would
be implemented to operate on what determines that algebra.
Martin Baker
___
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
correction - the link in my last message should have been:
http://www.euclideanspace.com/maths/standards/program/clifford/
___
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
The GrassmannAlgebra domain has been added to Axiom. --Tim
Tim,
Thanks, do you have any views about how it should evolve from here? I think
the first stage is to fix the known issues and get the inverse function
working well enough to be able to implement transforms for any metric. At
that
Bertfried,
Thanks this looks very useful.
Can I ask about the definitions of the involutions:
gradeInvolution == reversion? sign=(-1)^(d(d-1)/2) symbol= ~
Cliplus clirev == ? symbol=multiply by pseudoscalar? symbol=
Clifford conjugation: scalar part minus non-scalar part? symbol=
I know these
(by the way, the link to st-andrews
website on Axiom documentation page is broken).
Since I have not found this I have been making some notes for my own benefit:
http://www.euclideanspace.com/maths/standards/program/spad/
Any corrections welcome.
Martin Baker
be preferred
wherever possible and explicit coding of algorithms be discouraged?
Martin Baker
___
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
Tim,
Thank you for these replies, I am learning a lot here.
I think it helps to get a wider perspective.
Part of what prompted my question is when I was thinking about how to
implement the exterior product I thought about possible options, for instance
rules:
e1, e2…en | ei/\ei=0, ei/\ej=
Bertfried,
Thank you for your reply.
I will correct the spelling of Grassmann (although without using ß).
I have been thinking about the naming of the domain. I think it would be
better to use the name 'Multivector', which seems to me to represent what it
is, then the names Grassmann and
On Monday 16 November 2009 04:35:00 Tim Daly wrote:
This is a request for design discussion for those who are interested.
Tim,
Can I ask a nieve question? If you were starting from scratch would you write
Axiom in lisp? I've no special axe to grind and no special technical
knowledge, I'm just
Bill,
Thanks very much for your reply, this gives me a clearer idea of the issues
involved.
In view of what you said and having looked at the Aldor site I think I will
stay with the Spad compiler.
I tried:
)show GrassmanAlgebra
and the output looked reasonable.
I thought that the problems
Bertfried,
In addition to the limitations of the current Clifford algebra implementation,
that you explained, there also seem (to my untrained eye) to be performance
issues. Also I wanted to get a feel for the general Axiom design methodology
by picking a specific issue.
The current
59 matches
Mail list logo
