RE: [Axiom-developer] B#

[Page, Bill]

Gaby, 

On Friday, March 24, 2006 2:26 PM you wrote:
> 
> Bill Page writes:
> | 
> | Can you give a couple of specific examples of the kind of
> | design issues where you think the authors are being too
> | vague and the problems might be difficult to solve?
> 
> Yes; take the example on page 39 under subsection "Types".
> What are the rules that the type inference uses to infer
> the type L_{&s • &n &bullet}?  The answer is I have
> to apply AXIOM's rules. Now, where are the AXIOM's rules
> defined.  I turned over the paper I mentioned earlier, but
> I can't find the real rules.
>

In "How to Make Axiom into a ScratchPad" on page 39

http://portal.axiom-developer.org/refs/articles/axiom-scratchpad.pdf/vie
w

Jenks and Trager write:

> Types
>
> (AXIOM). This style refers to that used in current AXIOM.
> The simplest way of accessing other AXIOM or A# types is
> via B# "constructors". For example, matrix [[a, b], [c, d]]
> builds a 2 by 2 matrix of elements of type User. To break
> out of type User, a user simply makes type declarations.
> For example, the following is a display of a B# definition
> for Laguerre polynomials L:

\begin{axiom}

n:NNI
a:Fraction Integer
L(n,a,x) == ( n=0 => 1; _
              n=1 => -x+1+a; _
              (2*n+a-1-x)/n*L(n-1,a,x)-(n+a-1)/n*L(n-2,n,x))

\end{axiom}

> By omitting the type of x in the above definition, type
> inferencing is used to determine the full signature of the
> function L when the user asks for a value with given
> arguments. This may result in multiple compilations of
> L if the function is called with different types of
> arguments.

\begin{axiom}

)set message selection on
L(2,1/2,1.1)
L(2,1/2,1/4)

\end{axiom}

> 
> Alternately, a user may declare the type of L: rather
> than that of its arguments n and a, e.g.
>

\begin{axiom}

RF ==> Fraction Polynomial Integer
L: (NNI, RF, RF) -> RF
L(2,1/2,1/4)

\end{axiom}

>
> where NNI and RF are used here to abbreviate the AXIOM
> types NonNegativeInteger and Fraction Polynomial
> Integer respectively.

-------

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 :(. 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. For example, we can simply run the commands
above in the Axiom interpreter. The interpreter will
provide information about the function selections and
coercions that it makes as it interprets each of these
commands. As Jenks and Trager observe, the results depend
on what and how much type information is provided by the
user.

This is really a question about the old Axiom Interpreter,
not about the design of B#. There is some information in
the Axiom book. See:

  2.9 Package Calling and Target Types
  2.10 Resolving Types

--------

I have been thinking about possible representations for
the User type.

Jenks and Trager wrote the following about the User type:

> All domains in AXIOM accessible from type User export
> a coercion to convert objects of the domain into objects
> of type User, and coercions the other way that may fail.
> This simplifies the task of the interpreter that often
> has to find a coercion path between two given types.
>
> 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. 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. 'InputForm' already almost satisfies the
requirement that "All domains in Axiom accessible from
type User export a coercion to convert objects of the
domain into objects of type User." This is true if you
substitute 'InputForm' for type User. E.g.

\begin{axiom}

E1:=sqrt(sin(x)^2+1)
e1:=E1::InputForm

\end{axiom}

An object of type 'InputForm' can be converted to
another type by the 'interpret' operation. The result
is of type 'Any' and may be coerced to other types,
however some conversion will fail.

\begin{axiom}

E2:=interpret(e1)
)di type E2
E2::Polynomial Integer

\end{axiom}

Expressions of type 'InputForm' can also be manipulated and
displayed in a fairly flexible manner

\begin{axiom}

)sh InputForm
e2:=e1=e1**2
map(expr,e2)

\end{axiom}

The internal representation of object of 'InputForm' are
of type SExpression - essentially a tree structure. So it
seems to me that 'InputForm' has almost everything we need
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.

-------

Regards,
Bill Page.