[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [fricasdevel] Re: [Axiommail] InputForm
From: 
Gabriel Dos Reis 
Subject: 
Re: [fricasdevel] Re: [Axiommail] InputForm 
Date: 
Thu, 04 Jun 2009 15:43:12 0500 
Tim Daly <address@hidden> writes:
 Gabriel Dos Reis wrote:
 > Tim Daly <address@hidden> writes:
 >
 >  I've been reading this thread. It seems to me that what people are seeking
 >  is a symbolic algebra rather than a computer algebra system. The
distinction
 >  is that a symbolic system manipulates input as parse trees in
 >  syntactic form.
 >  A computer algebra system manipulates input as semantic forms. It appears
 >  that you want to recover the syntax from the semantics, a very hard
problem.
 >
 > OpenAxiom has the Syntax domain for matters that are purely syntactic,
 >
 > OpenAxiom's intended of InputForm is that of expressions the semantics
 > of which yield computer representation of mathematical object. In
 > particular, you can think of Syntax objects are preInputForm objects 
 > syntactic objects that have not yet been type checked. So a Syntax object
 > is really a member of an initial algebra  unlike InputForm or
 > SExpression objects.
 >
 >  This discussion came up before. At the time I wrote the beginnings of a
 >  symbolic front end to Axiom based on Joel Cohen's work. Joel has given
 >  me permission to use his books as part of the effort.
 >
 > I'm familiar with his work (and his two books). I would think that
 > there already exist a domain constructor, Expression, that is most
 > suited for the work presented in the two volumes. The fundamental
 > building block is the Kernel domain constructor. I know some people
 > have expressed profound dislikes of the Expression domain constructor.
 > But, I suspect that they would have a deeper appreciation of it after
 > reading Cohen's work.
 >
 > The need for InputForm is not just for 'symbolic mathematics'. A proper
 > support for the compilation model of the Spad language requires that any
 > constructor argument be coercible to InputForm. A fact that is not 
 > at the moment  enforced, but that is deeply relied upon. See what the
 > devaluate functions do and the unspolem assumptions behind.
 >
 > It is on my TODO list that OpenAxiom1.3.x and up will enforce those
 > assumptions.
 >
 >  Gaby
 >
 >
 So you propose that there are two reasons for this discussion of InputForm,
 one of which is to support a computational model of the spad language
 and the other is to support symbolic manipulation?
No  I did not mean to give an exhaustive list of reasons to have
InputForm or not. However, I do recognize instances of situations
where the notion of InputForm os relevant and that is what I was trying
to say. Futhermore, I do not think the world has to be divided in terms
of algebraic computation versus symbolic computation. Rather, my belief
is that symbolic mathematics (cross of algebraic computation and
symbolic computation) are going to be more and more prevalent.
 It is unclear what to expect from InputForm.
I think an operational definition of InputForm may be that of syntactic
normal forms of mathematical objects. This is required for handling
categories and domains properly (or any form of dependent types).
 Under the assumption of a computational model it seems that x+y^2 == y^2+x
Note that the linear display of the InputForm x + y^2 as y^2 + x
reflects the semantics of the polynomial object denoted by that form.
As such, I do not think this is a mater of algebraic versus symbolic
computation.
 Under the assumption of a cohen symbolic model they are not equivalent.
 (assuming that plus is associative in both cases)
Cohen assumes that + is associative  because he primarily works with
polynomials over commutative rings.
 Given that there was a comment that the input form was not properly
 reproduced
 I assumed the discussion involved symbolic issues. Perhaps I misread it.

 I do not see how InputForm can be made to support both models.
Indeed. I would reserve the use of InputForm for syntatic canonical
forms of mathematical objects.
 Gaby
 Re: [fricasdevel] Re: [Axiommail] InputForm, (continued)
 Re: [fricasdevel] Re: [Axiommail] InputForm, Gabriel Dos Reis, 2009/06/03
 Re: [fricasdevel] Re: [Axiommail] InputForm, Ralf Hemmecke, 2009/06/03
 Re: [fricasdevel] Re: [Axiommail] InputForm, Bill Page, 2009/06/03
 Re: [fricasdevel] Re: [Axiommail] InputForm, Gabriel Dos Reis, 2009/06/03
 Re: [fricasdevel] Re: [Axiommail] InputForm, Ralf Hemmecke, 2009/06/03
 Re: [fricasdevel] Re: [Axiommail] InputForm, Gabriel Dos Reis, 2009/06/03
 Re: [fricasdevel] Re: [Axiommail] InputForm, Tim Daly, 2009/06/04
 Re: [fricasdevel] Re: [Axiommail] InputForm, Gabriel Dos Reis, 2009/06/04
 Re: [fricasdevel] Re: [Axiommail] InputForm, Tim Daly, 2009/06/04
 Re: [fricasdevel] Re: [Axiommail] InputForm,
Gabriel Dos Reis <=
 Re: [fricasdevel] Re: [Axiommail] InputForm, Bill Page, 2009/06/04
 Re: [fricasdevel] Re: [Axiommail] InputForm, Gabriel Dos Reis, 2009/06/04
 Re: [fricasdevel] Re: [Axiommail] InputForm, Bill Page, 2009/06/04
 Re: [fricasdevel] Re: [Axiommail] InputForm, Gabriel Dos Reis, 2009/06/04
 Re: [fricasdevel] Re: [Axiommail] InputForm, Bill Page, 2009/06/04
 [Axiommail] mapleok, Tim Daly, 2009/06/05