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.
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.
Joel describes a symbolic, expression tree based system for doing
computational mathematics. I call this a "Cohen Algebra". Using these
expression trees allows us to carefully craft and manipulate the expressions
in ways that Axiom would not normally permit because they are not
semantically valid. As long as the forms are never coerced to Axiom
domains until they are semantically valid, it is possible to do many
"badly formed" intermediate manipulations, some of which are very
useful for teaching purposes.
We can get the Cohen algebra into Axiom using categories, domains, and
packages that support expression tree I/O and coercions to and from
Axiom domains, e.g.
cohenPolynomial(cohenInteger) <-> Polynomial(Integer)
This enables us to address several issues that have been outstanding
in the field for a while, including those mentioned at the last conference:
*) It would be possible to do "step-by-step" output (Watt?)
That is, you could show the steps of solving 3*x=6
by showing the step of dividing both sides by 3
3 6
- x = -
3 3
and preserve the 3 on both sides
*) It would be possible to do "step-by-step* explanations (Watt?)
Algorithms in the Cohen domains could easily have
explanations attached to the operations so that it could
automatically print:
"divide each side by 3"
*) It would be possible to modify the output if the result
turned into "wallpaper" (as mentioned by Davenport).
So you could simply print the condensed output of a
groebner basis computation.
*) It would be much easier to input and output forms for
other systems (e.g. supporting OpenMath output)
(Davenport)
I plan to do more work on Cohen domains because all of the
above features would be useful. My simple test example domains
are attached.
In my opinion, the idea of using InputForm beyond its intended
interpreter connections is not a viable effort. It would be much
easier and more profitable to construct something like the Cohen
domains to support the goal.
Tim
============================================
)abbrev category CCAT CohenCategory
+++ Author: Timothy Daly
+++ Date Created: 7 April 2007
+++ Description: Joel Cohen's Computer Algebra and Symbolic Computation
CohenCategory(): Category == SetCategory with
kind:(CExpr)->Boolean
++ kind(CExpr)
operand:(CExpr,Integer)->CExpr
++ operand:(CExpr,Integer)
numberOfOperand:(CExpr)->Integer
++ numberOfOperand:(CExpr)->Integer
construct:(CExpr,CExpr)->CExpr
++ construct:(CExpr,CExpr)->CExpr
-------------------------------------------------------------------
)abbrev domain CTERM CohenTerm
+++ Author: Timothy Daly
+++ Date Created: 7 April 2007
+++ Description: Joel Cohen's Computer Algebra and Symbolic Computation
CohenTerm(): Exports == Implementation where
OUT ==> OutputForm
ATTRIBS ==> Record(attrib: String, value: String)
UNION ==> Union(Symbol,String,Integer)
TAGS ==> Record(name:UNION, tags:List ATTRIBS)
Exports ==> CohenCategory with
term: () -> %
term: Symbol -> %
term: String -> %
term: Integer -> %
name: % -> String
tags: % -> List ATTRIBS
coerce: Symbol -> %
coerce: String -> %
coerce: Integer -> %
coerce: % -> OUT
_=: (%,%) -> Boolean
Implementation ==> add
Rep := TAGS
tagPair(atype:String,thetype:String):ATTRIBS ==
attr:ATTRIBS:=[atype,thetype]
name(t0:%):String ==
t1:=t0.name
t1 case Symbol => string t1
t1 case String => t1
t1 case Integer => string t1
"failed"
tags(t0:%):List ATTRIBS == t0.tags
term():% ==
attr:List ATTRIBS:= list tagPair("type","String")
aname:=""::UNION
result:TAGS:=[aname,attr]
result
term(s:Symbol):% == [s,[tagPair("type","Symbol")]]
coerce(s:Symbol):% == [s,[tagPair("type","Symbol")]]
term(s:String):% == [s,[tagPair("type","String")]]
coerce(s:String):% == [s,[tagPair("type","String")]]
term(s:Integer):% == [s,[tagPair("type","Integer")]]
coerce(s:Integer):% == [s,[tagPair("type","Integer")]]
coerce(arg:%):OUT ==
t0:=arg.name
t1:=arg.tags
t2:=
t0 case Symbol => outputForm t0
t0 case String => outputForm t0
t0 case Integer => outputForm t0
"failed"
--bracket [ t2, t1.1 ]
t2
a = b ==
a.name = b.name
-------------------------------------------------------------------
)abbrev domain CTREE CohenTree
+++ Author: Timothy Daly
+++ Date Created: 7 April 2007
+++ Description: Joel Cohen's Computer Algebra and Symbolic Computation
CohenTree(S: CohenCategory): Exports == Implementation where
Exports == BinaryTreeCategory(S) with
cohenTree: S -> %
++ cohenTree(v) is an non-empty cohen tree
++ with value v, and left and right empty.
++
++X t1:=cohenTree([1,2,3])
cohenTree: (%,S,%) -> %
++ cohenTree(l,v,r) creates a cohen tree with
++ value v with left subtree l and right subtree r.
++
++X t1:=cohenTree([1,2,3])
++X t2:=cohenTree([4,5,6])
++X cohenTree(t1,[7,8,9],t2)
cohenTree: (%,S) -> %
++ cohenTree(v,r) creates a cohen tree with
++ value v with right subtree r.
cohenTree: (S,%) -> %
++ cohenTree(l,v) creates a cohen tree with
++ value v with left subtree l
empty: () -> %
++ empty()
empty?: % -> Boolean
++ empty?(a)
leaf?: % -> Boolean
++ leaf?(a)
left: % -> %
++ left(a)
node: (%,S,%) -> %
++ node(a,b,c)
right: % -> %
++ right(a)
setleft_!: (%,%) -> %
++ setleft!(a,b)
setright_!: (%,%) -> %
++ setright!(a,b)
setvalue_!: (%,S) -> S
++ setvalue!(a,b)
value: % -> S
++ value(a)
Implementation == add
Rep := List Tree S
cohenTree(v:S) == node(empty(),v,empty())
cohenTree(l:%,v:S,r:%):% == node(l,v,r)
cohenTree(l:%,v:S):% == node(l,v,empty())
cohenTree(v:S,r:%):% == node(empty(),v,r)
empty()== [] pretend %
empty? t == empty?(t)$Rep
leaf? t == empty? t or empty? left t and empty? right t
left t ==
empty? t => error "cohenTree:no left"
children first t
node(l,v,r) == cons(tree(v,l:Rep),r:Rep)
right t ==
empty? t => error "cohenTree:no right"
rest t
setleft_!(t1,t2) ==
empty? t1 => error "cohenTree:no left to set"
setchildren_!(first(t1:Rep),t2:Rep)
t1
setright_!(t1,t2) ==
empty? t1 => error "cohenTree:no right to set"
setrest_!(t1:List Tree S,t2)
setvalue_!(t,nd) ==
empty? t => error "cohenTree:no value to set"
setvalue_!(first(t:Rep),nd)
nd
value t ==
empty? t => error "cohenTree:no value"
value first t
t1 = t2 == (t1::Rep) =$Rep (t2::Rep)
-------------------------------------------------------------------
-- a:=a::CTERM
-- b:=b::CTERM
-- c:=a+b
-- left(c)
-- right(c)
-- d:=3::CTERM
-- e:=d*c
-- left(e)
-- right(e)
--
-- -- Figure 3.4 p88
-- )clear all
--
-- c:=c::CTERM
-- d:=d::CTERM
-- x:=x::CTERM
-- two:=2::CTERM
-- e:=c+d*x^2
--
-- -- Figure 3.5a p89
-- )clear all
-- a:=a::CTERM
-- b:=b::CTERM
-- c:=c::CTERM
-- d:=a*b+c
-- e:=-d
-------------------------------------------------------------------
)abbrev package CMATH CohenMath
+++ Author: Timothy Daly
+++ Date Created: 7 April 2007
+++ Description: Joel Cohen's Computer Algebra and Symbolic Computation
CohenMath: Exports == Implementation where
TERM ==> CohenTerm
TREE ==> CohenTree(TERM)
Exports ==> with
_-: (TERM) -> TREE
++ -a
_-: (TREE) -> TREE
++ -a
-- "!": (TERM) -> TREE
-- ++ a!
-- "!": (TREE) -> TREE
-- ++ a!
_-: (TERM,TERM) -> TREE
++ a-b
_-: (TERM,TREE) -> TREE
++ a-b
_-: (TREE,TERM) -> TREE
++ a-b
_-: (TREE,TREE) -> TREE
++ a-b
_+: (TERM,TERM) -> TREE
++ a+b
_+: (TERM,TREE) -> TREE
++ a+b
_+: (TREE,TERM) -> TREE
++ a+b
_+: (TREE,TREE) -> TREE
++ a+b
_*: (TERM,TERM) -> TREE
++ a*b
_*: (TERM,TREE) -> TREE
++ a*b
_*: (TREE,TERM) -> TREE
++ a*b
_*: (TREE,TREE) -> TREE
++ a*b
_^: (TERM,TERM) -> TREE
++ a*b
_^: (TERM,TREE) -> TREE
++ a*b
_^: (TREE,TERM) -> TREE
++ a*b
_^: (TREE,TREE) -> TREE
++ a*b
Implementation ==> add
--- handle unary prefix terms
prefixTerm(op:TERM,b:TERM):TREE == cohenTree(op,cohenTree(b))
prefixTree(op:TERM,b:TREE):TREE == cohenTree(op,b)
--- handle unary postfix terms
postfixTerm(a:TERM,op:TERM):TREE == cohenTree(cohenTree(a),op)
postfixTree(a:TREE,op:TERM):TREE == cohenTree(a,op)
--- handle binary terms
termOpTerm(a:TERM,op:TERM,b:TERM):TREE ==
cohenTree(cohenTree(a),op,cohenTree(b))
termOpTree(a:TERM,op:TERM,b:TREE):TREE ==
cohenTree(cohenTree(a),op,b)
treeOpTerm(a:TREE,op:TERM,b:TERM):TREE ==
cohenTree(a,op,cohenTree(b))
treeOpTree(a:TREE,op:TERM,b:TREE):TREE ==
cohenTree(a,op,b)
_-(b:TERM):TREE == prefixTerm(term("-")$TERM,b)
_-(c:TREE):TREE == prefixTree(term("-")$TERM,c)
-- "!"(a:TERM):TREE == postfixTerm(a,term("!")$TERM)
-- "!"(a:TREE):TREE == postfixTree(a,term("!")$TERM)
_-(a:TERM, b:TERM):TREE == termOpTerm(a,term("-")$TERM,b)
_-(a:TERM, b:TREE):TREE == termOpTree(a,term("-")$TERM,b)
_-(a:TREE, b:TERM):TREE == treeOpTerm(a,term("-")$TERM,b)
_-(a:TREE, b:TREE):TREE == treeOpTree(a,term("-")$TERM,b)
_+(a:TERM, b:TERM):TREE == termOpTerm(a,term("+")$TERM,b)
_+(a:TERM, b:TREE):TREE == termOpTree(a,term("+")$TERM,b)
_+(a:TREE, b:TERM):TREE == treeOpTerm(a,term("+")$TERM,b)
_+(a:TREE, b:TREE):TREE == treeOpTree(a,term("+")$TERM,b)
_*(a:TERM, b:TERM):TREE == termOpTerm(a,term("*")$TERM,b)
_*(a:TERM, b:TREE):TREE == termOpTree(a,term("*")$TERM,b)
_*(a:TREE, b:TERM):TREE == treeOpTerm(a,term("*")$TERM,b)
_*(a:TREE, b:TREE):TREE == treeOpTree(a,term("*")$TERM,b)
_^(a:TERM, b:TERM):TREE == termOpTerm(a,term("^")$TERM,b)
_^(a:TERM, b:TREE):TREE == termOpTree(a,term("^")$TERM,b)
_^(a:TREE, b:TERM):TREE == treeOpTerm(a,term("^")$TERM,b)
_^(a:TREE, b:TREE):TREE == treeOpTree(a,term("^")$TERM,b)
-------------------------------------------------------------------
)abbrev domain COHEN CohenAlgebra
+++ Author: Timothy Daly (based on Joel Cohen's books)
+++ Date Created: 7 April 2007
+++ Description:
+++ This type represents symbolic algebra as detailed in Joel Cohen's
+++ books "Computer Algebra and Symbolic Computation"
+++ A.K. Peters, Ltd. ISBN 1-56881-159-4
+++
+++ Elements of this domain are purely symbolic expressions represented
+++ in a tree structure.
CohenAlgebra(X : CohenCategory) : CohenCategory with
_+: (X,X) -> %
++ x + y is the formal sum of the input arguments
_/: (X,X) -> %
++ x / y is the formal fraction of the input arguments
numer : % -> X
++ numer(x) is the numerator of the formal fraction
denom : % -> X
++ denom(x) is the denominator of the formal fraction
if X has IntegralDomain then
coerce : % -> Fraction(X)
++ coerce(x) from here to Fraction(there)
coerce : Fraction(X) -> %
++ coerce(x) from Fraction(there) to here
if X has Field then
coerce : % -> X
++ coerce from here to Field(there)
== add
import Record(num : X, den : X)
Rep := Record(num : X, den : X) -- representation
-- (a::CTERM + b::CTERM)$COHEN(CTERM)
-- c:CTERM:=d
-- e:CTERM:=f
-- (c+e)$COHEN(CTERM)
(n:X + d:X):% == [n,d]
-- (a::CTERM / b::CTERM)$COHEN(CTERM)
-- c:CTERM:=d
-- e:CTERM:=f
-- (c/e)$COHEN(CTERM)
(n:X / d:X):% == [n,d]
-- g:=(c/e)$COHEN(CTERM)
-- h:=(c/e)$COHEN(CTERM)
-- (g=h)
-- (g=h)::Boolean
-- i:=(a::CTERM / b::CTERM)$COHEN(CTERM)
-- j:=(a::CTERM / b::CTERM)$COHEN(CTERM)
-- (i=j)::Boolean
-- (g=i)
-- (g=i)::Boolean
_=(x:%, y:%):Boolean == (x.num = y.num) and (x.den = y.den)
-- numer g
-- numer i
numer(r:%):X == r.num
--denom g
--denom i
denom(r:%):X == r.den
coerce(r:%):OutputForm == (r.num :: OutputForm) / (r.den :: OutputForm)
-- COMPLEX(INT) has FIELD
-- COMPLEX(INT) has IntegralDomain
-- p:COMPLEX(INT):=2
-- p::FRAC(COMPLEX(INT))::COHEN(COMPLEX(INT))
if X has IntegralDomain then
coerce(r : %) : Fraction(X)
== (r.num / r.den) @ Fraction(X)
coerce(x : Fraction(X)) : % == x pretend %
-- FRAC(POLY(INT)) has FIELD
-- m:=(x^2)@FRAC(POLY(INT))
-- m::COHEN(POLY(INT))
if X has Field then
coerce(r : %) : X
== (r.num / r.den) @ X
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
