mailing-list for TeXmacs Users

[Jeremy Henty <address@hidden>]

On Thu, Jun 07, 2007 at 01:34:47AM -0600, Karl Hegbloom wrote:

> Sure, but to software that is reading the markup you've typed, perhaps
> so that it can hand it on to a CAS or so that some nifty new TeXmacs
> extension (probably yet to be written) can do some simple algebraic
> operations on it 

... which is indeed my cunning plan, if I can ever get my head around
the software.  But I want to do more than simple algebraic operations;
I want to create complete proofs.  I want to publish documents that
include actual proofs, *not* just typeset representations of them.

Currently I do mathematics with pencil and paper because there isn't
anything better.  (I use software to typeset the results, but that's
not the same thing.)  Mathematics is harder than algebra.

In other words, I *demand* a pony and I'm going to hold my breath
until I get it.  (OK, I plan to write the code too.)

> ... how is "w<space><tab>h" to be parsed?  

As the product of w and h , the same way I (and every other
mathematician I know) parse it.

> Since you can think of a variable as something like a zero argument
> function that returns the variable's current value ...

No.  A zero-argument function is a constant symbol, not a variable.
Variables are something else: if you deny that you have to define the
meaning of such rubbish as "forall 0 , it is true that ..."  and
"there exists sin(x) such that ...".  Look at the BNF for any formal
mathematics language and you'll see that <Variable> is a separate
syntactic category for precisely this reason - at some places (namely
quantifiers such as "for all", "there exist", "d/dx" and "integral
... dx") only a variable makes sense.  (In case you were wondering, I
have been employed to develop such formal tools so I am not just
making this up.)

> It's name alone signifies it's meaning uniquely enough, both to the
> human reader and to the CAS parser.

No.  The fact that the "d" in "dy/dx" is part of a differential
operator (rather than a variable called "d") is clear only from the
context.  The correct parsing of "dy/dx" is "(the operator d/dx)
applied to (the expression y)".  No context-insensitive parser will
get that right unless it parses an internal representation that has
extra invisible information.

> ... you would probably want to wrap it in a macro to get both
> special typeset appearance AND distinct semantics for the CAS
> parser.

I suspect that will be necessary to interface TeXmacs to a full proof
system including calculus, logical quantifiers etc. rather than just
algebra.  Has anyone already done this?  The documentation only
mentions algebra systems.

/me dives into the TeXmacs style package documentation.

Regards, 

Jeremy Henty