Re: [Axiom-developer] B#

[Gabriel Dos Reis]

"Page, Bill" <address@hidden> writes:

[...]

| In this context I would not call it vague or hand waving.
| They are simply referring to the behavior of the Axiom
| interpreter as it is now defined. Unfortunately I am not
| able to point you to any clear and complete system-level
| documentation of the actual algorithms used :(.

yes, that is what I have been saying :-).  I read the codes in
src/interp/i-*.spad.pamphlet; although I don't understand all of it,
it still is not a specification of the AXIOM type system rules.

| But in the
| final analysis we do have the full source code for the
| interpreter plus we can do some experiments to test our
| understanding.

yes; however that assumes the existing code base is correct AND we do
understand it sufficiently well.  I'm far from meeting those criteria
now.  I'm trying to being overly critical of the paper.  I find it
quite very useful and delightful by moment.  However, the formal type
system rules are not there, not in any other paper I can have access
to through ACM.  I hope Tim would be able to make some of the
technical reports available to us.

[...]

| > Type User has exported operations that allow the user to
| > do general formula manipulation, to transform parse forms
| > and results as symbolic formulae under rather complete user
| > control. Transformations can be done by pattern-matching
| > or direct manipulation. Expression trees provide a simple
| > and intuitive model of a formula.
| 
| To me this sounds very much like the 'InputForm' domain that
| is already part of the Axiom Interpreter.

and not SExpression? 

| I have a feeling
| that the Axiom developers were already incrementally moving
| toward a B# implementation by a series of smaller steps
| involving extensions to the Axiom library and to the Axiom
| interpreter.

My general feeling after reading the paper several times is that they 
beleive in two-level systems: one for library writer where the full
rigor or strongly typed language is there to assist the library
writer; and one level (top level?) to introduce novices to the
system.  This is to be contrasted (as they said in the paper) with the
approach taken by Maple (it is interesting to note their comparison
with the GAUSS system).  I believe they wanted to make the system more
accesible, but I don't think they wanted to move away from A#.

[...]

| as a representation for the type User. In principle it
| would not be a difficult job to implement parser for B#
| in SPAD or Aldor that would generate InputForm expressions
| directly from B# input and perform the type of coercions
| that are now down by the Axiom interpreter.

Implementing the parser is indeed not difficult at all.  The
interesting bit is connecting to the rest of the system.

-- Gaby