[Axiom-math] Re: musings on notation

[root]

Paul,

Paul Graham wrote:
>The thing to do would be to show how you can make some
>existing e.g. Lisp program shorter by using functors.

Actually Axiom and its programming language do make programs much
shorter. It closely mirrors the mathematics and uses a unification
of the idea of categories from math with the idea of type hierarchy
from comp sci to get very expressive, short programs. Most functions
are less than 10 lines long and on average are below that length. The
resulting algorithms are extremely readable (provided you know the
theory, of course).

It's not the length of the program that I'm trying to optimize but
the length of the thought process. Imagine having to say "take the
limit of this function as x tends toward zero such that given any
epsilon we can always find a delta... We don't do this. We just say
integrate and we just write the \int symbol.

The problem that needs to be attacked, however, is that there doesn't
appear to be a notation that I could write by hand for a "thing" that
has the properties of a program (including the notion of process) as
well as the properties of a mathematical object. (Or the "thing" that
has the properties of a closure as well as a mathematical object).



Let me try an example. Consider the simple case of trying to raise a
square matrix to an integer power:
 
 P = 3
 M:SquareMatrix(2) = matrix([[1,2],[3,4]])
 M^P

which we know how to do. 



The harder case is to assume we don't know the actual value of P but
we know its Category. So if an IndefiniteInteger which have the
property of integers but we don't say which one. IndefiniteInteger is
a type we understand so we can say:

 P = IndefiniteInteger()
 M = SquareMatrix(2)
 M^P

which implies that we have to compute a symbolic object (M^P) but know
that P is of some well-defined type with certain properties but with
unspecified value. We can't compute it's actual value until P takes on
a particular integer value.



The notational case is even harder. So I'd like to be able
to say:

 P = Program(foo)
 M:SquareMatrix(2) = matrix([[1,2],[3,4]])
 M^P

but first I need to define categorical properties of the "Program"
type. So it might be a functor of the form:

 Program(C:Code) -> Integer()

that is, a Program type is Categorically defined to accept things
of type Code and is guaranteed to produce an Integer(). Notice
what happened here. I'm trying to raise a square matrix to an
unspecified power and all I can guarantee is that the operation
WOULD be defined if I were to compute it. I want a name for this
concept "the operation would be defined if we run it". 

Now mathematically this is hard because we haven't defined the
Category structure for Code. Do we require all Code functions to be
total (a definite valid value for every input?). Do we require the
Category of Stateless so that the function always returns the same
result? If so, we could functionally compose Program types, define
operators, and be able to compute:

  Q = P*P

where the '*' function is
 
  *(Program,Program) -> Program

However, Program objects could include the notion of "running" over
time (unless you subscribe to Dijkstra's view). There is some previous
work in this area in lisp (scheme has continuations, lisp has closure, 
delay and force). I'd like to distinguish these "special property" 
objects with a new mathematical notation so they become apparent.

Thus, a polynomial that uses P above is not obviously "runnable" if
we just create a program variable and use it in the polynomial:

 p = Program(knarlyfunction)
 poly = p^2 + 2*p + 1

'poly' has a value that  now depends on {running, forcing, continuing} p.




I'm suggesting that we need to have a "run, force, continue" notation
similar to integration, with integration we normally write:

 integrate(poly,p)

to integrate poly with respect to p. With programs we could say

 force(poly)

where 'force' is a fancy looking kanji character on input and output.
The reason for choosing a fancy character is to "lift" the idea of
forcing functions into the notation so we can start defining the 
difference between

  force( integrate(poly,p) )

and 

  integrate( force(poly) , p)

or even

 force( force(poly) )

where 'force' means "the operation would be defined if we run it".



This raising the question of how this new notational idea composes with
other notations. What does kanji-F (force) mean and what are its
properties?
 



Indeed, some mathematical problems lend themselves well to such a
notation. Consider a function that, when integrated, returns multiple
branches. This could be handled by continuations. So in the computatation

                                | x<0 => sin(x)
                                |
  integrate(knarlyfunction,x) =>| x=0 => 0
                                |
                                | x>0 => cos(x)

consider what could happen. Somewhere in the integration it 
becomes apparent that, say, the result is discontinuous at 0.
The code breaks the computation into 3 delayed branches (or
continuations, or closures, or whatever) and returns these
continuations unforced.

  kanji-C1 = Program(knarlyfunction, proviso(x<0))
  kanji-C2 = Program(knarlyfunction, proviso(x=0))
  kanji-C3 = Program(knarlyfunction, proviso(x>0))

so kanji-C1 is a closure objects that can return a result. 
and then does 

  force(kanji-C1)
  force(kanji-C2)
  force(kanji-C3)


Consider what happens if we think about this notationally rather
than computationally. We could state that 

  integrate(knarlyfunction,x) => {kanji-C1, kanji-C2, kanji-C3}

and leave the results as symbolic values rather than forcing them.
Since we are building symbolic mathematical software this is a 
ideally what we'd like to be able to do. Then we could evaluate
a polynomial thus:

  poly = x^2 + 2*x + 3
  eval(poly, x==kanji-C1) 

and get the result

  kanji-C4

and force(kanji-C4) => sin(x)&2 + 2*sin(x) + 3



The overall thought is that if we have a notation that will allow
us to write results using pencil-and-paper then we can begin to
express what these things mean in a computational mathematics system.

Currently we're using the ideas but we haven't reified them.




CY had set me to thinking about this earlier today with his email:
==================================================================


> C Y Student wrote:
> I don't have any profound insights as far as notation, but I would
> suggest a particular documentation approach to this type of work.
> 
> Mathematical notation is implimented (or at least based on) standard
> mathematical ideas because they are intuitive to the normal mathematics
> user.  Unique notation, however useful or powerful it might be, will be
> rejected by all but a few unless two things happen:
> 
> 1)  The notation becomes a standard way of doing something useful in a
> computer algebra system
> 2)  End users are compelled to learn the notation because they can't
> live without the extra expressiveness/features/etc. it provides.
> 
> 1) is wrapped up in 2), in my opinion.  And the only way to get a foot
> in the door with 2) is to a) document the new notation comprehensively,
> clearly, and usably and b) provide non-trivial useful examples where
> the new notation solves a problem where old notation would have had
> great difficulties.  We have to sell the new notation, not just develop
> it.  We have to make people want it.
> 
> The tool that comes to mind as an effectively marketed tool is Sun's
> new system tool dtrace.  Their strategy was simple but very effective -
> they showed useful examples where subtle system problems were
> identified by dtrace quickly where no other system tools could have
> done it nearly as well.  I think any new notation Axiom is going to
> introduce will have to do the same - not just propose it and show it is
> elegant, but have cases of it effectively addressing real world (or at
> least math world) problems.  Show people that it is worth the time and
> pain to learn new concepts and tools.  Then, if people like the new
> abilities well enough, perhaps a standard can be created.
> 
> I would also suggest this be the figure of merit for proposed new
> notation - not only that it be powerful in theory, but shown to be
> powerful in interesting examples.  Just my 2c.